Self provers and Σ1 sentences

Logic Journal of the IGPL 20 (1):1-21 (2012)

Joost Joosten
Universitat de Barcelona
This paper is the second in a series of three papers. All three papers deal with interpretability logics and related matters. In the first paper a construction method was exposed to obtain models of these logics. Using this method, we obtained some completeness results, some already known, and some new. In this paper, we will set the construction method to work to obtain more results. First, the modal completeness of the logic ILM is proved using the construction method. This is not a new result, but by using our new proof we can obtain new results. Among these new results are some admissible rules for ILM and GL. Moreover, the new proof will be used to classify all the essentially Δ1 and also all the essentially Σ1 formulas of ILM. Closely related to essentially Σ1 sentences are the so-called self provers. A self-prover is a formula φ which implies its own provability, that is φ → □φ. Each formula φ will generate a self prover φ ^ □φ. We will use the construction method to characterize those sentences of GL that generate a self prover that is trivial in the sense that it is Σ1
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1093/jigpal/jzp096
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 42,156
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Cuts, Consistency Statements and Interpretations.Pavel Pudlák - 1985 - Journal of Symbolic Logic 50 (2):423-441.
The Interpretability Logic of Peano Arithmetic.Alessandro Berarducci - 1990 - Journal of Symbolic Logic 55 (3):1059-1089.
The Formalization of Interpretability.Albert Visser - 1991 - Studia Logica 50 (1):81 - 105.
A Course on Bimodal Provability Logic.Albert Visser - 1995 - Annals of Pure and Applied Logic 73 (1):109-142.

View all 18 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Modal Matters for Interpretability Logics.Evan Goris & Joost Joosten - 2008 - Logic Journal of the IGPL 16 (4):371-412.
Finite Models Constructed From Canonical Formulas.Lawrence S. Moss - 2007 - Journal of Philosophical Logic 36 (6):605 - 640.
Propositional Proof Systems and Fast Consistency Provers.Joost J. Joosten - 2007 - Notre Dame Journal of Formal Logic 48 (3):381-398.
Proofs and Countermodels in Non-Classical Logics.Sara Negri - 2014 - Logica Universalis 8 (1):25-60.
An Empirical Analysis of Modal Theorem Provers.Ullrich Hustadt & Renate A. Schmidt - 1999 - Journal of Applied Non-Classical Logics 9 (4):479-522.
On Me Number of Steps in Proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
On the Number of Steps in Proofs.Jan Kraj\mIček - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
On the Set of Atoms.M. Crabbé - 2000 - Logic Journal of the IGPL 8 (6):751-759.
Arithmetic Proof and Open Sentences.Neil Thompson - 2012 - Philosophy Study 2 (1):43-50.


Added to PP index

Total views
5 ( #995,455 of 2,253,631 )

Recent downloads (6 months)
4 ( #484,966 of 2,253,631 )

How can I increase my downloads?


My notes

Sign in to use this feature