Premium
Quantified propositional calculi and fragments of bounded arithmetic
Author(s) -
Krajíček Jan,
Pudlák Pavel
Publication year - 1990
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19900360106
Subject(s) - constructive , mathematical proof , bounded function , propositional calculus , citation , mathematics , computer science , arithmetic , calculus (dental) , algebra over a field , discrete mathematics , library science , pure mathematics , programming language , medicine , mathematical analysis , geometry , dentistry , process (computing)
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), .