2.4: The Sequent Calculus
- Page ID
- 121607
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)
( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\id}{\mathrm{id}}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\kernel}{\mathrm{null}\,}\)
\( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\)
\( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\)
\( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)
\( \newcommand{\vectorA}[1]{\vec{#1}} % arrow\)
\( \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow\)
\( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vectorC}[1]{\textbf{#1}} \)
\( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)
\( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)
\( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
- 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.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.