The provability logic for Σ1-interpolability

Annals of Pure and Applied Logic 64 (1):1-25 (1993)
  Copy   BIBTEX


We say that two arithmetical formulas A, B have the Σ1-interpolation property if they have an ‘interpolant’ σ, i.e., a Σ1 formula such that the formulas A→σ and σ→B are provable in Peano Arithmetic PA. The Σ1-interpolability predicate is just a formalization of this property in the language of arithmetic.Using a standard idea of Gödel, we can associate with this predicate its provability logic, which is the set of all formulas that express arithmetically valid principles in the modal language with two modal operators, □ for provability in PA and for Σ1-interpolability. In this paper we determine this provability logic .It turns out that this problem appears to be quite similar to the problem of such modal description of relative interpretability, a problem, solved by Berarducci and Shavrukov. However, the present case is sometimes easier. In particular, we prove in this paper the fixed point property and the Craig interpolation property for our modal system ELH



    Upload a copy of this work     Papers currently archived: 74,389

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

The Provability Logic for Σ< Sub> 1-Interpolability.Konstantin N. Ignatiev - 1993 - Annals of Pure and Applied Logic 64 (1):1-25.
On the Provability Logic of Bounded Arithmetic.Rineke Verbrugge & Alessandro Berarducci - 1991 - Annals of Pure and Applied Logic 61 (1-2):75-93.
The Decision Problem of Provability Logic with Only One Atom.Vítězslav Švejdar - 2003 - Archive for Mathematical Logic 42 (8):763-768.
Closed Fragments of Provability Logics of Constructive Theories.Albert Visser - 2008 - Journal of Symbolic Logic 73 (3):1081-1096.
Explicit Provability and Constructive Semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
Realization of Intuitionistic Logic by Proof Polynomials.Sergei N. Artemov - 1999 - Journal of Applied Non-Classical Logics 9 (2-3):285-301.


Added to PP

4 (#1,230,858)

6 months
1 (#415,900)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Modal Matters for Interpretability Logics.Evan Goris & Joost Joosten - 2008 - Logic Journal of the IGPL 16 (4):371-412.
Self Provers and Σ1 Sentences.Evan Goris & Joost Joosten - 2012 - Logic Journal of the IGPL 20 (1):1-21.
Interpolation and the Interpretability Logic of PA.Evan Goris - 2006 - Notre Dame Journal of Formal Logic 47 (2):179-195.

Add more citations

References found in this work

The Interpretability Logic of Peano Arithmetic.Alessandro Berarducci - 1990 - Journal of Symbolic Logic 55 (3):1059-1089.
Characters and Fixed-Points in Provability Logic.Zachary Gleit & Warren Goldfarb - 1989 - Notre Dame Journal of Formal Logic 31 (1):26-36.

Add more references