Truth definitions without exponentiation and the Σ₁ collection scheme

Journal of Symbolic Logic 77 (2):649-655 (2012)
  Copy   BIBTEX


We prove that: • if there is a model of I∆₀ + ¬ exp with cofinal Σ₁-definable elements and a Σ₁ truth definition for Σ₁ sentences, then I∆₀ + ¬ exp +¬BΣ₁ is consistent, • there is a model of I∆₀ Ω₁ + ¬ exp with cofinal Σ₁-definable elements, both a Σ₂ and a ∏₂ truth definition for Σ₁ sentences, and for each n > 2, a Σ n truth definition for Σ n sentences. The latter result is obtained by constructing a model with a recursive truth-preserving translation of Σ₁ sentences into boolean combinations of $\exists \sum {\begin{array}{*{20}{c}} h \\ 0 \\ \end{array} } $ sentences. We also present an old but previously unpublished proof of the consistency of I∆₀ + ¬ exp + ¬BΣ₁ under the assumption that the size parameter in Lessan's ∆₀ universal formula is optimal. We then discuss a possible reason why proving the consistency of I∆₀ + ¬ exp + ¬BΣ₁ unconditionally has turned out to be so difficult



    Upload a copy of this work     Papers currently archived: 79,857

External links

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

Through your library


Added to PP

34 (#357,863)

6 months
1 (#479,585)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jeffrey Paris
University of Manchester

References found in this work

Relating the bounded arithmetic and polynomial time hierarchies.Samuel R. Buss - 1995 - Annals of Pure and Applied Logic 75 (1-2):67-77.
End extensions of models of linearly bounded arithmetic.Domenico Zambella - 1997 - Annals of Pure and Applied Logic 88 (2-3):263-277.

Add more references