Witnessing functions in bounded arithmetic and search problems

Journal of Symbolic Logic 63 (3):1095-1115 (1998)
  Copy   BIBTEX

Abstract

We investigate the possibility to characterize (multi) functions that are Σ b i -definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T 2 in terms of natural search problems defined over polynomial-time structures. We obtain the following results: (1) A reformulation of known characterizations of (multi)functions that are Σ b 1 - and Σ b 2 -definable in the theories S 1 2 and T 1 2 . (2) New characterizations of (multi)functions that are Σ b 2 - and Σ b 3 -definable in the theory T 2 2 . (3) A new non-conservation result: the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α). To prove that the theory T 2 2 (α) is not ∀Σ b 1 (α)-conservative over the theory S 2 2 (α), we present two examples of a Σ b 1 (α)-principle separating the two theories: (a) the weak pigeonhole principle WPHP (a 2 , f, g) formalizing that no function f is a bijection between a 2 and a with the inverse g, (b) the iteration principle Iter (a, R, f) formalizing that no function f defined on a strict partial order ( $\{0,\dots,a\}$ , R) can have increasing iterates

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,127

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

Multifunction algebras and the provability of PH↓.Chris Pollett - 2000 - Annals of Pure and Applied Logic 104 (1-3):279-303.
Exponentiation and second-order bounded arithmetic.Jan Krajíček - 1990 - Annals of Pure and Applied Logic 48 (3):261-276.
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.
The Σ 2 1 theory of axioms of symmetry.Galen Weitkamp - 1989 - Journal of Symbolic Logic 54 (3):727-734.
Monotone reducibility and the family of infinite sets.Douglas Cenzer - 1984 - Journal of Symbolic Logic 49 (3):774-782.
What are the ∀∑1 b-consequences of T 2 1 and T 2 2?Fernando Ferreira - 1995 - Annals of Pure and Applied Logic 75 (1):79-88.

Analytics

Added to PP
2009-01-28

Downloads
20 (#793,209)

6 months
70 (#75,308)

Historical graph of downloads
How can I increase my downloads?

References found in this work

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.
Theory of Formal Systems.Raymond M. Smullyan - 1965 - Journal of Symbolic Logic 30 (1):88-90.
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.
¹1-formulae on finite structures.M. Ajtai - 1983 - Annals of Pure and Applied Logic 24 (1):1.
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.

View all 6 references / Add more references