Quantified propositional calculi and fragments of bounded arithmetic
Quantified propositional calculi and fragments of bounded arithmetic
复制标题
量化命题演算和有界算术片段
DOI：
10.1002/malq.19900360106
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
P. Pudlák
中科院分区：
文献类型：
--
作者：
J. Krajícek;P. Pudlák
本文的动机来自一个著名的，可能是非常困难的问题，是否有界算术是完全可公理化。迄今为止，试图用逻辑机器来解决这个问题的努力都失败了。将逻辑与组合逻辑相结合，有可能解决这一问题.这就需要转换成一个更具组合性的问题。有界算术的有限可公理化性似乎与多项式族是否坍缩为某个Ci\ level 1的问题密切相关：f，B~t.这两个问题之间没有任何关系被证明. 1）本文提出了一个不同的组合性质的问题，并证明了这个问题与有界算术的有限可公理化性问题之间的关系. COOK [4]介绍了多项式时间可计算函数的方程理论PV，并给出了PV与命题证明系统ER（ExtendedResolution）之间的有趣关系。他证明了（1）PV证明了ER的可靠性;（2）在PV中可证明的等式到命题演算的转换在ER中有多项式长度的证明。Bus [1]证明了S~（有界算术S2的一个片段）在PV上是保守的，从而将这个关系转移到S~上。S ~ 2的有限公理化等价于族S~，i = 1，2，. . .,正在增加。我们将构造命题证明系统G，它对i ~ 1与S~+l有类似的关系，就像ER与S~有类似的关系一样。然后我们讨论了关于S~（i = 1，2，.）. .,可以归结为证明系统G”i = 1，2，. ..系统G，是命题逻辑的Gentzen系统到至多有i个量词替换的量化命题公式的自然推广。关于G的问题将需要证明超多项式下界，在这些系统中证明的长度。这似乎太困难了，目前，指数下界已被证明只有相当弱的系统分辨率系统（未扩展）到目前为止，比照。哈肯[8]。然而，我们将证明，从这个关系可以导出关于S~ 2及其片段的非平凡陈述，特别是：（1）对于i > j ~ 2，如果S~ 2是可公理化的，则V ~ 1：J-推论（推论7.1），.
The motivation for this paper comes from a well-known and probably very difficult problem whether Bounded Arithmetic is fiIiitely axiomatizable. Attempts tosolve this problem using the machinery of mathematicallogic have failed so far. It is possible that, the problem can be solved by combining logic with combinatl;>rics. This would require a transformation onto a more combinatorial problem. Thefinite axiomatizability of Bounded Arithmetic seems to be tightly connected with the problem whether Polynomial Hierarchy collapses to somCi\ level 1:f, b~t no implication relating these two problems has been proved.l) Here we present a different problem of a combinatorial character and prove a relation between this problem and the problem of the finite axiomatizability of Bounded Arithmetic. COOK [4] introduced an equational theory PV of pólynomial time computablé flinctions and showed an interesting relation between PV and propositional proof system ER (ExtendedResolution).. He showed that (1) PV proves soundness ofER and (2) the translati~n of the equalities provable in PV into propositional calculus have polynomial1y long proofs in ER. Bus~ [1] showed that S~ (a fragment of the bounded arithmetic S2) is conservative over PV; thus this relation is transferred to S~. The finite axiomatizability of S2 is equivalent to the question whether the hierarchy S~, i = 1,2, . . ., is increasing. We shall construct propositional proof systems G, which have similar relation to S~+l for i ~ 1 as ER has to S~. Then we show tttat the problem about ,the hierarchy S~, i = 1,2, . . ., can be reduced to a problem about the length of proofs in proof systems G" i = 1, 2, ... .. The systems G, are natural extensions of a Gentzen system for the propositional logic to quantified propositional formulas with at most i quantifier alternations. The problem about G,'s would require proving superpolynomial lower bounds, to the length of proofs in these systems. This seems too difficult at present, as exponential lower bounds have been proved only for quite a weak system Resolution System (not extended) so far, cf. HAKEN [8]. However we shall show that nontrivial statements about S2 and its fragments can be derived from this relation, in particular: (1) For i > j ~ 2 the V1:J-consequences if S~ are finitely axiomatizable (Corollary 7.1), .