Wyniki wyszukiwania

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

An Arithmetically Complete Predicate Modal Logic

63%

Hao Y., Tourlakis G.

Bulletin of the Section of Logic

2021

tom 50

nr 4

513-541

This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness (with respect to finite reverse well-founded Kripke models) is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.

Ograniczanie wyników

2 Bulletin of the Section of Logic

2 Tourlakis G.

1 Hao Y.

1 2021

1 2016

Wyniki wyszukiwania

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

An Arithmetically Complete Predicate Modal Logic