Reference [12] introduced a novel formula to formula translation tool that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations. In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.18778/0138-0680.45.1.02
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 69,078
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

The Modal Logic of Provability. The Sequential Approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
On Modal Systems Having Arithmetical Interpretations.Arnon Avron - 1984 - Journal of Symbolic Logic 49 (3):935-942.
The Predicate Modal Logic of Provability.Franco Montagna - 1984 - Notre Dame Journal of Formal Logic 25 (2):179-189.

View all 6 references / Add more references

Citations of this work BETA

An Arithmetically Complete Predicate Modal Logic.Yunge Hao & George Tourlakis - 2021 - Bulletin of the Section of Logic 50 (4):513-541.

Add more citations

Similar books and articles

Extension Without Cut.Lutz Straßburger - 2012 - Annals of Pure and Applied Logic 163 (12):1995-2007.
Uniform Short Proofs for Classical Theorems.Kees Doets - 2001 - Notre Dame Journal of Formal Logic 42 (2):121-127.
Boolos-Style Proofs of Limitative Theorems.György Serény - 2004 - Mathematical Logic Quarterly 50 (2):211.
Why Do Mathematicians Re-Prove Theorems?John W. Dawson Jr - 2006 - Philosophia Mathematica 14 (3):269-286.
Proof-Theoretical Analysis of Order Relations.Sara Negri, Jan von Plato & Thierry Coquand - 2004 - Archive for Mathematical Logic 43 (3):297-309.
Interpolation and the Interpretability Logic of PA.Evan Goris - 2006 - Notre Dame Journal of Formal Logic 47 (2):179-195.
Probabilistic Proofs and Transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
A Formalization Of Sambins's Normalization For Gl.Edward Hauesler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.


Added to PP index

Total views
7 ( #1,063,755 of 2,498,790 )

Recent downloads (6 months)
1 ( #421,542 of 2,498,790 )

How can I increase my downloads?


My notes