A small reflection principle for bounded arithmetic

Journal of Symbolic Logic 59 (3):785-812 (1994)
  Copy   BIBTEX

Abstract

We investigate the theory IΔ 0 + Ω 1 and strengthen [Bu86. Theorem 8.6] to the following: if NP ≠ co-NP. then Σ-completeness for witness comparison formulas is not provable in bounded arithmetic. i.e. $I\delta_0 + \Omega_1 + \nvdash \forall b \forall c (\exists a(\operatorname{Prf}(a.c) \wedge \forall = \leq a \neg \operatorname{Prf} (z.b))\\ \rightarrow \operatorname{Prov} (\ulcorner \exists a(\operatorname{Prf}(a. \bar{c}) \wedge \forall z \leq a \neg \operatorname{Prf}(z.\bar{b})) \urcorner)).$ Next we study a "small reflection principle" in bounded arithmetic. We prove that for all sentences φ $I\Delta_0 + \Omega_1 \vdash \forall x \operatorname{Prov}(\ulcorner \forall y \leq \bar{x} (\operatorname{Prf} (y. \overline{\ulcorner \varphi \urcorner}) \rightarrow \varphi)\urcorner).$ The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlak in [Pu86]. Finally, we give some applications of the small reflection principle, showing that the principle can sometimes be invoked in order to circumvent the use of provable Σ-completeness for witness comparison formulas

Similar books and articles

Consequences of arithmetic for set theory.Lorenz Halbeisen & Saharon Shelah - 1994 - Journal of Symbolic Logic 59 (1):30-40.
Frege's unofficial arithmetic.Agustín Rayo - 2002 - Journal of Symbolic Logic 67 (4):1623-1638.
Stretchings.O. Finkel & J. P. Ressayre - 1996 - Journal of Symbolic Logic 61 (2):563-585.
Classification and interpretation.Andreas Baudisch - 1989 - Journal of Symbolic Logic 54 (1):138-159.

Analytics

Added to PP
2009-01-28

Downloads
151 (#121,584)

6 months
83 (#51,164)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Citations of this work

Faith & falsity.Albert Visser - 2004 - Annals of Pure and Applied Logic 131 (1-3):103-131.
Uniform Density in Lindenbaum Algebras.V. Yu Shavrukov & Albert Visser - 2014 - Notre Dame Journal of Formal Logic 55 (4):569-582.
No Escape from Vardanyan's theorem.Albert Visser & Maartje de Jonge - 2006 - Archive for Mathematical Logic 45 (5):539-554.

View all 6 citations / Add more citations

References found in this work

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
Arithmetization of Metamathematics in a General Setting.Solomon Feferman - 1960 - Journal of Symbolic Logic 31 (2):269-270.
On the scheme of induction for bounded arithmetic formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (C):261-302.
The formalization of interpretability.Albert Visser - 1991 - Studia Logica 50 (1):81 - 105.

View all 20 references / Add more references