2.4: The Sequent Calculus

Sets, Logic, Computation · LibreTexts

0%

Contents

    Text

    Size
    100%
    Theme
    Typeface
    Line length
    Spacing

    From LibreTexts, under CC BY, as the source states it; its equations are written in TeX, which the PDF shows typeset. This page at LibreTexts.

    • 2.4.1: Rules and Derivations
      A sequent is an expression of the form \(\Gamma \Rightarrow \Delta\). \(\Gamma\) is called the antecedent, while \(\Delta\) is the succedent. The intuitive idea behind a sequent is: if all of the sentences in the antecedent hold, then at least one of the sentences in the succedent holds.
    • 2.4.2: Propositional Rules
      Rules for \(\lnot\), \(\land\), \(\lor\), and \(\rightarrow\)
    • 2.4.3: Quantifier Rules
      Rules for \(\forall\) and \(\exists\)
    • 2.4.4: Structural Rules
      We also need a few rules that allow us to rearrange sentences in the left and right side of a sequent.
    • 2.4.5: Derivations
      We’ve said what an initial sequent looks like, and we’ve given the rules of inference. Derivations in the sequent calculus are inductively generated from these: each derivation either is an initial sequent on its own, or consists of one or two derivations followed by an inference.
    • 2.4.6: Examples of Derivations
      Examples of \(\mathbf{LK}\)-derivations for the sequents \(A \land B \Rightarrow A\), \(\lnot A \lor B \Rightarrow A \rightarrow B\), and \(\lnot A \lor \lnot B \Rightarrow \lnot (A \land B)\), and an example of the contraction rule
    • 2.4.7: Derivations with Quantifiers
      An example of an \(\mathbf{LK}\)-derivation of the sequent \(\exists{x}\,{\lnot A(x)} \Rightarrow \lnot \forall{x}\,{A(x)}\)
    • 2.4.8: Proof-Theoretic Notions
      Just as we’ve defined a number of important semantic notions (validity, entailment, satisfiability), we now define corresponding proof-theoretic notions. These are not defined by appeal to satisfaction of sentences in structures, but by appeal to the derivability or non-derivability of certain sequents. It was an important discovery that these notions coincide. That they do is the content of the soundness and completeness theorem.
    • 2.4.9: Derivability and Consistency
      We will now establish a number of properties of the derivability relation. They are independently interesting, but each will play a role in the proof of the completeness theorem.
    • 2.4.10: Derivability and the Propositional Connectives
    • 2.4.11: Derivability and the Quantifiers
    • 2.4.12: Soundness
      A derivation system, such as the sequent calculus, is sound if it cannot derive things that do not actually hold.
    • 2.4.13: Derivations with Identity predicate
      Derivations with identity predicate require additional initial sequents and inference rules.
    • 2.4.14: Soundness with Identity predicate
      \(\mathbf{LK}\) with initial sequents and rules for identity is sound.
    • 2.4.15: Summary

    This page titled 2.4: The Sequent Calculus was last modified on Sun, 12 Sep 2021 15:29:22 GMT and is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .