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-definable with smalli(i= 1, 2, 3) in fragments of bounded arithmeticT2in 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 areand-definable in the theoriesand.(2) New characterizations of (multi)functions that areand-definable in the theory.(3) A new non-conservation result: the theoryis not-conservative over the theory.To prove that the theoryis not-conservative over the theory, we present two examples of a-principle separating the two theories:(a) the weak pigeonhole principle WPHP(a2,f, g) formalizing that no functionfis a bijection betweena2andawith the inverseg,(b) the iteration principle Iter(a, R, f) formalizing that no functionfdefined on a strict partial order ({0,…, a},R) can have increasing iterates.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,202

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

Admissible closures of polynomial time computable arithmetic.Dieter Probst & Thomas Strahm - 2011 - Archive for Mathematical Logic 50 (5):643-660.
Lifting independence results in bounded arithmetic.Mario Chiari & Jan Krajíček - 1999 - Archive for Mathematical Logic 38 (2):123-138.
Nested PLS.Toshiyasu Arai - 2011 - Archive for Mathematical Logic 50 (3-4):395-409.
Herbrandizing search problems in Bounded Arithmetic.Jiří Hanika - 2004 - Mathematical Logic Quarterly 50 (6):577-586.
On Almost Orthogonality in Simple Theories.Itay Ben-Yaacov & Frank O. Wagner - 2004 - Journal of Symbolic Logic 69 (2):398 - 408.
Structures interpretable in models of bounded arithmetic.Neil Thapen - 2005 - Annals of Pure and Applied Logic 136 (3):247-266.
Bounded arithmetic for NC, ALogTIME, L and NL.P. Clote & G. Takeuti - 1992 - Annals of Pure and Applied Logic 56 (1-3):73-117.
$Sigma^1_2$-Sets of Reals.Jaime I. Ihoda - 1988 - Journal of Symbolic Logic 53 (2):636-642.

Analytics

Added to PP
2017-02-21

Downloads
5 (#1,469,565)

6 months
1 (#1,459,555)

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.

View all 6 references / Add more references