Geodesic
A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
Bulletin of the Section of Logic, Tome 45 (2016) no. 1.

Voir la notice de l'article provenant de la source Library of Science

Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) 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 (provably, [2]) 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 (compare with the more complexproofs in [2,8]).
Keywords: Modal logic, GL, first-order logic, proof theory, cut elimination, reflection property, disjunction property, quantified modal logic, QGL, arithmetical completeness 
@article{BSL_2016_45_1_a0,
     author = {Tourlakis, George},
     title = {A {New} {Arithmetically} {Incomplete} {First-Order} {Extension} of {Gl} {All} {Theorems} of {Which} {Have} {Cut} {Free} {Proofs}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {45},
     number = {1},
     year = {2016},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a0/}
}
TY  - JOUR
AU  - Tourlakis, George
TI  - A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
JO  - Bulletin of the Section of Logic
PY  - 2016
VL  - 45
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a0/
LA  - en
ID  - BSL_2016_45_1_a0
ER  - 
%0 Journal Article
%A Tourlakis, George
%T A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
%J Bulletin of the Section of Logic
%D 2016
%V 45
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a0/
%G en
%F BSL_2016_45_1_a0
Tourlakis, George. A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs. Bulletin of the Section of Logic, Tome 45 (2016) no. 1. http://geodesic.mathdoc.fr/item/BSL_2016_45_1_a0/