Proving consistency of equational theories in bounded arithmetic

Journal of Symbolic Logic 67 (1):279-296 (2002)
  Copy   BIBTEX

Abstract

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.])

Categories

Keywords

Reprint years

DOI

10.2178/jsl/1190150044

Links

PhilArchive



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

External links

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

Through your library

My notes

Similar books and articles

On the equational class of diagonalizable algebras.Glaudio Bernardi - 1975 - Studia Logica 34 (4):321 - 331.
Theories with equational forking.Markus Junker & Ingo Kraus - 2002 - Journal of Symbolic Logic 67 (1):326-340.
A consistency proof for elementary algebra and geometry.Harvey Friedman - manuscript
For everyn, then-freely generated algebra is not functionally free in the equational class of diagonalizable algebras.Franco Montagna - 1975 - Studia Logica 34 (4):315 - 319.
Weak theories of nonstandard arithmetic and analysis.Jeremy Avigad - manuscript
On interpretations of bounded arithmetic and bounded set theory.Richard Pettigrew - 2009 - Notre Dame Journal of Formal Logic 50 (2):141-152.
"True" arithmetic can prove its own consistency.Andrew Boucher -
The consistency of arithmetic.Storrs McCall - manuscript
Equivalence of F with a sub-theory of peano arithmetic.Andrew Boucher - manuscript
On the Herbrand Notion of Consistency for Finitely Axiomatizable Fragments of Bounded Arithmetic Theories.Leszek Aleksander Kołodziejczyk - 2006 - Journal of Symbolic Logic 71 (2):624 - 638.

Analytics

Added to PP
2009-01-28

Downloads
60 (#253,024)

6 months
14 (#139,944)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

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.
Term rewriting theory for the primitive recursive functions.E. A. Cichon & Andreas Weiermann - 1997 - Annals of Pure and Applied Logic 83 (3):199-223.

Add more references