1,720,979 research outputs found
Labelled calculi for quantified modal logics with definite descriptions
Get PDFWe introduce labelled sequent calculi for quantified modal logics with definite descriptions. We prove that these calculi have the good structural properties of G3-style calculi. In particular, all rules are height-preserving invertible, weakening and contraction are height-preserving admissible and cut is syntactically admissible. Finally, we show that each calculus gives a proof-theoretic characterization of validity in the corresponding class of models
A Syntactic Proof of the Decidability of First-Order Monadic Logic
Get PDFDecidability 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
Labelled sequent calculi for logics of strict implication
Get PDFn 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
Proof-theoretic pluralism
Get PDFStarting from a proof-theoretic perspective, wheremeaning is determined by the inference rules governing logical operators, in this paper we primarily aim at developing a proof-theoretic alternative to the model-theoretic meaning-invariant logical pluralism discussed in Beall and Restall (Logical pluralism, Oxford University Press, Oxford, 2006). We will also outline how this framework can be easily extended to include a form of meaning-variant logical pluralism. In this respect, the framework developed in this paper—which we label two-level proof-theoretic pluralism—is much broader in scope than the one discussed in Beall and Restall’s book
Non-Normal Super-Strict Implications
Get PDFThis paper introduces the logics of super-strict implications that are based on C.I. Lewis’ non-normal modal logics S2 and S3. The semantics of these logics is based on Kripke’s semantics for non-normal modal logics. This solves a question we left open in a previous paper by showing that these logics are weakly connexive
Proof theory for quantified monotone modal logics
Get PDFThis paper provides a proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone non-normal modal logics, and studies the role of the Barcan Formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction, and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut
sequent calculi for indexed epistemic logics
No full textIndexed epistemic logics constitute a well-structured class of quantified epistemic logics with great expressive power and a well-behaved semantics based on the notion of epistemic transition model. It follows that they generalize term-modal logics. As to proof theory, the only axiomatic system for which we have a completeness theorem is the minimal system Q.Ke, whether with classical or with free quantification. This paper proposes a different approach by introducing labelled sequent calculi. This approach turns out to be very flexible and modular: for each class of epistemic transition structures C* considered in the literature, we introduce a G3-style labelled calculus GE.*. We show that these calculi have very good structural properties insofar as all rules are height-preserving invertible (hp-invertible), weakening and contraction are height-preserving admissible (hp-admissible) and cut is admissible. We will also prove that each calculus GE.* characterizes the class C* of indexed epistemic structures
Proof Analysis in Deontic Logics
No full textSequent calculi for normal and non-normal deontic logics are introduced. For these calculi we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This yields that the subformula property holds for them and that they are decidable. Then we show that our calculi are equivalent to the axiomatic ones, and therefore that they are sound and complete w.r.t. neighborhood semantics. This is a major step in the development of the proof theory of deontic logics since our calculi allow for a systematic root-first proof search of formal derivations
Logicality, Double-line Rules, and Harmony
No full textThe inversion principle, and the related notion of harmony, has been extensively discussed in
proof-theoretic semantics at least since (Prawitz, 1965). In our paper we make use of multi-
conclusion sequent-style calculi to provide a harmonious proof-theoretic analysis of modal logics,
and we concentrate on Standard Deontic Logic (SDL) as a running example. Our approach is
based on combining display calculi (DSDL) with Dosen's characterization of logicality in purely
structural terms. We present a genuinely new double-line version of DSDL, i.e. DdlSDL, and we
show that DSDL and DdlSDL are deductively equivalent. This equivalence allows us to show
that the rules of DSDL are harmonious: the left introduction rules are inverse of the right one
inasmuch as they are deductively equivalent to the bottom-up elimination rule of DdlSDL
Interpolation in Extensions of First-Order Logic
Get PDFWe prove a generalization of Maehara’s lemma to show that the extensions
of classical and intuitionistic first-order logic with a special type of geometric axioms,
called singular geometric axioms, have Craig’s interpolation property. As a corollary, we
obtain a direct proof of interpolation for (classical and intuitionistic) first-order logic with
identity, as well as interpolation for several mathematical theories, including the theory
of equivalence relations, (strict) partial and linear orders, and various intuitionistic order
theories such as apartness and positive partial and linear orders
- …
