Examining fragments of the quantified propositional calculus

Journal of Symbolic Logic 73 (3):1051-1080 (2008)
  Copy   BIBTEX

Abstract

When restricted to proving $\Sigma _{i}^{q}$ formulas, the quantified propositional proof system $G_{i}^{\ast}$ is closely related to the $\Sigma _{i}^{b}$ theorems of Buss's theory $S_{2}^{i}$ . Namely, $G_{i}^{\ast}$ has polynomial-size proofs of the translations of theorems of $S_{2}^{i}$ , and $S_{2}^{i}$ proves that $G_{i}^{\ast}$ is sound. However, little is known about $G_{i}^{\ast}$ when proving more complex formulas. In this paper, we prove a witnessing theorem for $G_{i}^{\ast}$ similar in style to the KPT witnessing theorem for $T_{2}^{i}$ . This witnessing theorem is then used to show that $S_{2}^{i}$ proves $G_{i}^{\ast}$ is sound with respect to $\Sigma _{i+1}^{q}$ formulas. Note that unless the polynomial-time hierarchy collapses $S_{2}^{i}$ is the weakest theory in the s₂ hierarchy for which this is true. The witnessing theorem is also used to show that $G_{i}^{\ast}$ is p-equivalent to a quantified version of extended-Frege for prenex formulas. This is followed by a proof that Gi p-simulates $G_{i+1}^{\ast}$ with respect to all quantified propositional formulas. We finish by proving that S₂ can be axiomatized by $S_{2}^{1}$ plus axioms stating that the cut-free version of $G_{0}^{\ast}$ is sound. All together this shows that connection between $G_{i}^{\ast}$ and $S_{2}^{i}$ does not extend to more complex formulas

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Fragments of the propositional calculus.Leon Henkin - 1949 - Journal of Symbolic Logic 14 (1):42-48.
Simplified formalizations of fragments of the propositional calculus.Alan Rose - 1977 - Notre Dame Journal of Formal Logic 18 (2):255-261.
Tables for the propositional calculus (logico-mathematical brain).René Calvache - 1966 - Miami, Fla.: Miami, Fla.. Edited by Sanabria, E. F. & [From Old Catalog].
Theorem counting.M. G. Beavers - 1994 - Topoi 13 (1):61-65.
Sequential Dynamic Logic.Alexander Bochman & Dov M. Gabbay - 2012 - Journal of Logic, Language and Information 21 (3):279-298.
Quantum logical calculi and lattice structures.E. -W. Stachow - 1978 - Journal of Philosophical Logic 7 (1):347 - 386.

Analytics

Added to PP
2010-09-12

Downloads
31 (#443,123)

6 months
1 (#1,028,709)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Bounded arithmetic and the polynomial hierarchy.Jan Krajíček, Pavel Pudlák & Gaisi Takeuti - 1991 - Annals of Pure and Applied Logic 52 (1-2):143-153.
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.
Quantified propositional calculi and fragments of bounded arithmetic.Jan Krajíček & Pavel Pudlák - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (1):29-46.

Add more references