1,721,020 research outputs found
Subintuitionistic logics and their modal companions: a nested approach
Full text linkIn the present paper we deal with subintuitionistic logics and their modal companions. In particular, we introduce nested calculi for subintuitionistic systems and for modal logics in the S5 modal cube ranging from K to S4. The latter calculi differ from standard nested systems, as there are multiple rules handling the modal operator. As an upshot, we get a purely syntactic proof of the Gödel-McKinsey-Tarski embedding which preserves the structure and the height of the derivations. Finally, we obtain a conservativity result for classical logic over a weak subintuitionistic system
Infinitary logic with infinite sequents: syntactic investigations
Full text linkThe present paper deals with a purely syntactic analysis of infinitary logic with infinite sequents. In particular, we discuss sequent calculi for classical and intuitionistic infinitary logic with good structural properties based on sequents possibly containing infinitely many formulas. A cut admissibility proof is proposed which employs a new strategy and a new inductive parameter. We conclude the paper by discussing related issues and possible themes for future research
Constructive theories through a modal lens
Full text linkWe present a uniform proof-theoretic proof of the Gödel–McKinsey–Tarski embedding for a class of first-order intuitionistic theories. This is achieved by adapting to the case of modal logic the methods of proof analysis in order to convert axioms into rules of inference of a suitable sequent calculus. The soundness and the faithfulness of the embedding are proved by induction on the height of the derivations in the augmented calculi. Finally, we define an extension of the modal system for which the result holds with respect to geometric intuitionistic
Labelled sequent calculi for Lewis’ non-normal propositional modal logics
No full textC. I. Lewis’ systems were the first axiomatisations of modal logics. However some of those systems are non-normal modal logics, since they do not admit a full rule of necessitation, but only a restricted version thereof. We provide G3-style labelled sequent calculi for Lewis’ non-normal propositional systems. The calculi enjoy good structural properties, namely admissibility of structural rules and admissibility of cut. Furthermore they allow for straightforward proofs of admissibility of the restricted versions of the necessitation rule. We establish completeness of the calculi and we discuss also related systems
On the proof theory of infinitary modal logic
Full text linkThe article deals with infinitary modal logic. We first discuss the difficulties related to the development of a satisfactory proof theory and then we show how to overcome these problems by introducing a labelled sequent calculus which is sound and complete with respect to Kripke semantics. We establish the structural properties of the system, namely admissibility of the structural rules and of the cut rule. Finally, we show how to embed common knowledge in the infinitary calculus and we discuss first-order extensions of infinitary modal logic
Through and beyond classicality: analyticity, embeddings, infinity
Full text linkStructural proof theory deals with formal representation of proofs and with the investigation of their properties. This thesis provides an analysis of various non-classical logical systems using proof-theoretic methods. The approach consists in the formulation of analytic calculi for these logics which are then used in order to study their metalogical properties. A specific attention is devoted to studying the connections between classical and non-classical reasoning. In particular, the use of analytic sequent calculi allows one to regain desirable structural properties which are lost in non-classical contexts. In this sense, proof-theoretic versions of embeddings between non-classical logics - both finitary and infinitary - prove to be a useful tool insofar as they build a bridge between different logical regions
Analyticity with extra-logical information
Full text linkIn this paper, a new approach to the issue of extra-logical information within analytic (i.e. obeying the sub-formula property) sequent systems is introduced. We prove that incorporating extra-logical axioms into a purely logical system can preserve analyticity, provided these axioms belong to a suitable class of formulas that can be decomposed into a set of equivalent initial sequents and are permutable over the cut rule. Our approach is applicable not only to first-order classical and intuitionistic logics, but also to substructural logics. Furthermore, we establish a limit for the augmented systems under analysis: exceeding the boundaries of their respective classes of extra-logical axioms leads to either a loss of analyticity or a loss of structural properties
A Syntactic Proof of the Decidability of First-Order Monadic Logic
Full text linkDecidability of monadic first-order classical logic was established by L ̈owenheimin 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T
Inside Classical Logic: Truth, Contradictions, Fractionality
Full text linkFractional semantics provides a multi-valued interpretation of a variety of logics, governed by purely proof-theoretic principles. This approach employs a method of systematic decomposition of formulas through a well-disciplined sequent calculus, assigning a fractional value that measures the “quantity of identity” (intuitively, “quantity of truth”) within a sequent. A key consequence of this framework is the breakdown of the traditional symmetry between truth and contradiction. In this paper, we explore the ramifications of this novel perspective on classical logic. Specifically, we (i) introduce an alternative paraconsistent consequence relation, and (ii) show how the gradual character of contradictions induces a corresponding characterization of tautologies, thereby obtaining a full-fledged informational refinement of classical logic
Labelled sequent calculi for logics of strict implication
Full text linkn this paper we study the proof theory of C.I. Lewis’ logics of strict conditional S1-
S5 and we propose the first modular and uniform presentation of C.I. Lewis’ systems.
In particular, for each logic Sn we present a labelled sequent calculus G3Sn and we
discuss its structural properties: every rule is height-preserving invertible and the
structural rules of weakening, contraction and cut are admissible. Completeness of
G3Sn is established both indirectly via the embedding in the axiomatic system Sn
and directly via the extraction of a countermodel out of a failed proof search. Finally,
the sequent calculus G3S1 is employed to obtain a syntactic proof of decidability of
S1
- …
