Skip Navigation

Journal of Logic and Computation 2009 19(1):123-143; doi:10.1093/logcom/exn030
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Cordón-Franco, A.
Right arrow Articles by Lara-Martín, F. F.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

This article appears in the following Journal of Logic and Computation issue: Special Issue: Logic and Computation in the Real World: CiE 2007 [View the issue table of contents]

Original Articles

Existentially Closed Models and Conservation Results in Bounded Arithmetic

A. Cordón-Franco, A. Fernández-Margarit and F. F. Lara-Martín

Facultad de Matemáticas. Universidad de Sevilla, C/ Tarfia s/n, 41012 Sevilla (Spain).

E-mail: acordon{at}us.es,afmargarit{at}us.es,fflara{at}us.es

Received 28 September 2007.

We develop model-theoretic techniques to obtain conservation results for first order Bounded Arithmetic theories, based on a hierarchical version of the well-known notion of an existentially closed model. We focus on the classical Buss' theories SFormula and TFormula and prove that they are {forall}{Sigma}Formula conservative over their inference rule counterparts, and exist{forall}{Sigma}Formula conservative over their parameter-free versions. A similar analysis of the {Sigma}Formula-replacement scheme is also developed. The proof method is essentially the same for all the schemes we deal with and shows that these conservation results between schemes and inference rules do not depend on the specific combinatorial or arithmetical content of those schemes. We show that similar conservation results can be derived, in a very general setting, for every scheme enjoying some syntactical (or logical) properties common to both the induction and replacement schemes. Hence, previous conservation results for induction and replacement can be also obtained as corollaries of these more general results.

Keywords: Bounded arithmetic; existentially closed models; conservation results; parameter-free schemes



References

  1. Adamowicz Z, Bigorajska T. Existentially closed structures and Gödel's second incomplenteness theorem. The Journal of Symbolic Logic (2001) 66:349–356.[CrossRef]
  2. Avigad J. Saturated models of universal theories. Annals of Pure and Applied Logic (2002) 118:219–234.[CrossRef][Web of Science]
  3. Bloch S. Divide and Conquer in Parallel Complexity and Proof Theory. (1992) PhD Thesis, University of California, San Diego.
  4. Buss S. Bounded Arithmetic. (1986) Bibliopolis, Napoli.
  5. Clote P, Takeuti G. First order bounded arithmetic and small boolean circuit complexity classes. In: Feasible Mathematics II.—Clote P, Remmel J, eds. (1995) Birkhäuser, Boston. 154–218.
  6. Hirschfeld J, Wheeler WA. Forcing, Arithmetic, Division Rings. (1975) Berlin, Heidelberg: Springer Verlag. Lecture Notes in Mathematics, vol. 454.
  7. Johannsen J. A Bounded Arithmetic Theory for Constant Depth Threshold Circuits. Gödel'96. (1996) Berlin, Heidelberg: Springer. 224–234. Lecture Notes in Logic, vol. 6.
  8. Johannsen J, Pollett C. On proofs about threshold circuits and counting hierarchies. In: Proceedings of the 13th IEEE Symposium on Logic in Computer Science. (1998) Los Alamitos, CA, USA: IEEE Computer Society. 444–453.
  9. Johannsen J, Pollett C. On the {Delta}Formula–bit–comprehension rule. Logic Colloquium'98. (2000) 13. Natick, Massachusetts: ASL/A.K. Peters. 262–279. Lecture Notes in Logic.
  10. Krajícek J, Pudlák P, Takeuti G. Bounded arithmetic and the polynomial herarchy. Annals of Pure and Applied Logic (1991) 52:143–153.[CrossRef][Web of Science]
  11. Krajícek J. Bounded Arithmetic,Propositional Logic, and Complexity Theory. (1995) Cambridge, New York, Melbourne: Cambridge University Press.
  12. Nguyen P, Cook S. Theories for TC0 and other small complexity classes. Logical Methods in Computer Science (2006) 2:1–40.[Medline]
  13. Pollett C. Structure and definability in general bounded arithmetic theories. Annals of Pure and Applied Logic (1999) 100:189–245.[CrossRef][Web of Science]
  14. Sieg W. Herbrand analyses. Archive for Mathematical Logic (1991) 30:409–441.[CrossRef]

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Cordón-Franco, A.
Right arrow Articles by Lara-Martín, F. F.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?