We introduce a first order extension of GL, called ML 3 , and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML 3 , as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove (...) that ML 3 is sound with respect to arithmetical interpretations and that it is also sound and complete with respect to converse well-founded and transitive finite Kripke models. This leads us to expect that a Solovay-like proof of arithmetical completeness of ML 3 is possible. (shrink)

We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.

In this paper, we introduce provability multilattice logic PMLn and multilattice arithmetic MPAn which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that PMLn has the provability interpretation with respect to MPAn and prove the arithmetic completeness theorem for it. We formulate PMLn in the form of a nested sequent calculus and show that cut is admissible in it. We introduce the notion of a provability multilattice and develop algebraic semantics for PMLn on its (...) basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for PMLn and establish the Kripke completeness theorem via syntactical and semantic embeddings from PMLn into GL and vice versa. Last but not least, the decidability of PMLn is shown. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

This paper is the first of a series of three articles that present the syntactic proof of the PA-completeness of the modal system G, by introducing suitable proof-theoretic objects, which also have an independent interest. We start from the syntactic PA-completeness of modal system GL-LIN, previously obtained in [7], [8], and so we assume to be working on modal sequents S which are GL-LIN-theorems. If S is not a G-theorem we define here a notion of syntactic metric d(S, G): we (...) calculate a canonical characteristic fomula H of S (char(S)) so that ⊢G ∼ H → (∼S) and ⊢GL-LIN ∼ H, and the complexity σ of ∼ H gives the distance d(S, G) of S from G. Then, in order to produce the whole completeness proof as an induction on this d(S, G), we introduce the tree-interpretation of a modal sequent Q into PA, that sends the letters of Q into PA-formulas describing the properties of a GL-LIN-proof P of Q: It is also a d(*, G)-metric linked interpretation, since it will be applied to a proof-tree T of ∼ H with H = char(S) and σ(∼ H) = d(S, G). (shrink)

We present sequent calculi for normal modal logics where modal and propositional behaviours are separated, and we prove a cut elimination theorem for the basic system K, so as completeness theorems both for K itself and for its most popular enrichments. MSC: 03B45, 03F05.

This paper deals with the system of modal logicGL, in particular with a formulation of it in terms of sequents. We prove some proof theoretical properties ofGL that allow to get the cut-elimination theorem according to Gentzen's procedure, that is, by double induction on grade and rank.

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.