A Proof Theory for the Logic of Provability in True Arithmetic

Studia Logica 108 (4):857-875 (2020)
  Copy   BIBTEX

Abstract

In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. However, it might sound somewhat strange that no proof theory for GLS was ever developed nor even suggested thus far, except for the axiomatic system offered by Solovay. In this paper, we develop a proof theory for GLS based on the sequent calculus method. We provide a sequent calculus for GLS and prove the cut-elimination and some standard consequences of it: the interpolation and definability theorems. As another consequence of cut-elimination, we also prove the equivalence of GL and GLS with respect to a special form of formulas which we call Gödel sentences, using a purely proof-theoretical method.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

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

Provability logics with quantifiers on proofs.Rostislav E. Yavorsky - 2001 - Annals of Pure and Applied Logic 113 (1-3):373-387.
Arithmetic Proof and Open Sentences.Neil Thompson - 2012 - Philosophy Study 2 (1):43-50.
Provability logic.Rineke Verbrugge - 2008 - Stanford Encyclopedia of Philosophy.
Realization of Intuitionistic Logic by Proof Polynomials.Sergei N. Artemov - 1999 - Journal of Applied Non-Classical Logics 9 (2-3):285-301.
The provability logic for Σ1-interpolability.Konstantin N. Ignatiev - 1993 - Annals of Pure and Applied Logic 64 (1):1-25.

Analytics

Added to PP
2019-12-19

Downloads
27 (#506,960)

6 months
4 (#320,252)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Proof theory.Gaisi Takeuti - 1975 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
Provability Interpretations of Modal Logic.Robert M. Solovay - 1981 - Journal of Symbolic Logic 46 (3):661-662.

View all 14 references / Add more references