Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: GL

Sortuj według:

Ogranicz wyniki do:

Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik

A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

100%

Tourlakis G.

Bulletin of the Section of Logic

2016

tom 45

nr 1

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]).

A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics

100%

Gao F., Tourlakis G.

Bulletin of the Section of Logic

2015

tom 44

nr 3-4

A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as primitive; or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules.

Ograniczanie wyników

2 Bulletin of the Section of Logic

2 Tourlakis G.

1 Gao F.

1 2016

1 2015

Wyniki wyszukiwania

A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics