sequent calculus

A syntactic proof system that derives conclusions from premises using formal rules of inference.

Semantic entailment $F_1,...,F_n\models G$ means $G$ is true in every model where all of $F_1,...,F_n$ are true. A model (or interpretation) consists of a domain of objects plus assignments of meaning to all constants, functions, predicates, and variables. To verify semantic entailment directly, you’d need to check infinitely many such models.

Sequent calculus provides inference rules: patterns like “if you can prove $A$ and you can prove $B$, then you can prove $A\wedge B$.” These rules depend only on formula structure, not meaning. You build a proof tree by repeatedly applying rules until you reach trivially true statements (axioms).

If the rules are sound (derived sequents are semantically valid) and complete (all semantic entailments are derivable), then:

$$F_1,...,F_n⊢G⟺F_1,...,F_n\models G$$

Soundness

$\Gamma ⊢F⟹\Gamma \models F$

If you can build a valid proof tree from $\Gamma$ to $F$ using the inference rules, then $F$ actually holds in every model where all of $\Gamma$ holds. The rules don’t let you “prove” something that doesn’t follow.

Completeness

$\Gamma \models F⟹\Gamma ⊢F$

If $F$ is true in every model satisfying $\Gamma$, then there exists some proof tree that derives $F$ from $\Gamma$. No semantic truth escapes the proof system.

Gödel’s Completeness Theorem: First-order predicate logic has a proof calculus that is both sound and complete. No logic stronger than first-order can have both.

Undecidability

There is no algorithm that takes $\Gamma$ and $F$, always terminates, and correctly outputs whether $\Gamma \models F$. (Related: halting problem, church-turing thesis)

We do get semidecidability: by completeness, if $\Gamma \models F$ then a proof exists. Systematically enumerate all possible proof trees; if one exists, you eventually find it. But if $\Gamma /\models F$, the search runs forever. You can’t distinguish “no proof exists” from “haven’t found it yet.”

Result	Statement
Completeness	$\Gamma \models F\iff \Gamma ⊢F$
Undecidability	No algorithm decides $\Gamma \models F$ for all inputs
Semidecidability	Can confirm $\Gamma \models F$, but can’t confirm $\Gamma /\models F$
Incompleteness	Some true arithmetic statements have no proof

Completeness and incompleteness aren’t contradictory: completeness says “every semantic consequence of your axioms is provable,” incompleteness says “in systems rich enough for arithmetic, some statements true in $\mathbb{N}$ aren’t provable from the axioms.”

Why arithmetic? Because addition and multiplication let you encode formulas and proofs as numbers (Gödel numbering). The system becomes powerful enough to make statements about itself, including “this statement is not provable.” Systems too weak for arithmetic can’t self-reference this way, so they escape the incompleteness trap.

---

You build a proof tree by applying inference rules that break down complex formulas into simpler components. The goal is to reach axioms or trivially true sequents at the leaves.

proof by induction

$$\frac{K\cdots ⊢F\left[m/n\right]K\dots ,\bar{n}\in {\mathbb{N}}_{\ge m},F[\bar{n}/n]⊢F[(\bar{n}+1)/n]}{K\cdots ⊢\forall n\in {\mathbb{N}}_{\ge m}:F}$$

In words: To prove a property $F$ holds for all natural numbers $n\ge m$:
$K\cdots ⊢F\left[m/n\right]$ : Prove the base case, that $F$ holds for the smallest $n=m$.
$K\dots ,\bar{n}\in {\mathbb{N}}_{\ge m},F[\bar{n}/n]⊢F[(\bar{n}+1)/n]$ : Prove the inductive step, that for any arbitrary $\bar{n}\ge m$, if $F$ holds for $\bar{n}$, then it also holds for $\bar{n}+1$.
Then you can conclude $F$ holds for all $n\ge m$.

The below is not a minimal but a practical set of inference rules; many rules can be derived from others.

Inference Rules

A sequent has the form: $$
K_1, K_2, \ldots \vdash G

where $K_1, K_2, \ldots$ are the **assumptions** (what we know) and $G$ is the **goal** (what we want to prove). The turnstile $\vdash$ separates them. --- ### 1. Closing Rules (rules with no premises - they "close" a branch) These are your "base cases" - when you can stop and say "done." **GoalAssum (GA):** $$ \text{GA}: \quad K\ldots, G \vdash G

If the goal is already among the assumptions, you’re done.

Example: $p(a),q(b)⊢p(a)$ — closed immediately, the goal $p(a)$ is an assumption.

---

ContrAssum (CA): $$
\text{CA}: \quad K\ldots, A, \neg A \vdash G

If you have both $A$ and $\neg A$ among assumptions, you can prove anything (contradiction). _Example:_ $p(a), \neg p(a) \vdash q(b)$ — closed, we have contradictory assumptions. --- **FalseAssum:** $$ \text{FalseAssum}: \quad K\ldots, \bot \vdash G

If $\perp$ (false) is among assumptions, you can prove anything.

---

2. Structural Rules

Drop: $$
\frac{K\ldots \vdash G}{\text{Drop}: \quad K\ldots, A \vdash G}

You can always drop an assumption you don't need. (Going top-down in your quiz: the premise has fewer assumptions.) --- **Cut:** $$ \frac{K\ldots \vdash A \quad\quad K\ldots, A \vdash G}{\text{Cut}: \quad K\ldots \vdash G}

To prove $G$, first prove some intermediate statement $A$, then prove $G$ using $A$. This requires “an idea” for what $A$ should be.

---

Indirect: $$
\frac{K\ldots, \neg G \vdash \bot}{\text{Indirect}: \quad K\ldots \vdash G}

Proof by contradiction: assume $\neg G$, derive a contradiction. --- ### 3. Connective Rules For each connective, there's typically: - A **P-rule** (prove it as a goal) - An **A-rule** (use it as an assumption) --- #### Negation **P-¬:** $$ \frac{K\ldots, G \vdash \bot}{\text{P-}\neg: \quad K\ldots \vdash \neg G}

To prove $\neg G$: assume $G$ and derive a contradiction.

Example: To prove $⊢\neg p(a)$, we’d need to show $p(a)⊢\perp$.

---

A-¬: $$
\frac{K\ldots, \neg G \vdash A}{\text{A-}\neg: \quad K\ldots, \neg A \vdash G}

If you know $\neg A$ and want to prove $G$: assume $\neg G$ and prove $A$. (This is a bit indirect - essentially a contraposition argument.) --- #### Conjunction **P-∧:** $$ \frac{K\ldots \vdash F_1 \quad\quad K\ldots \vdash F_2}{\text{P-}\land: \quad K\ldots \vdash F_1 \land F_2}

To prove $F_1\wedge F_2$: prove $F_1$ AND prove $F_2$ (two branches).

Example: $$
\frac{\vdash p(a) \quad\quad \vdash q(b)}{\text{P-}\land: \quad \vdash p(a) \land q(b)}

--- **A-∧:** $$ \frac{K\ldots, F_1, F_2 \vdash G}{\text{A-}\land: \quad K\ldots, F_1 \land F_2 \vdash G}

If you have $F_1\wedge F_2$ as assumption: you can split it into two separate assumptions $F_1$ and $F_2$.

Example: $$
\frac{p(a), q(b) \vdash r(c)}{\text{A-}\land: \quad p(a) \land q(b) \vdash r(c)}

--- #### Disjunction **P-∨:** $$ \frac{K\ldots, \neg F_1 \vdash F_2}{\text{P-}\lor: \quad K\ldots \vdash F_1 \lor F_2}

To prove $F_1\vee F_2$: assume $\neg F_1$ and prove $F_2$. (Or symmetrically, assume $\neg F_2$ and prove $F_1$.)

Example: $$
\frac{\neg p(a) \vdash q(b)}{\text{P-}\lor: \quad \vdash p(a) \lor q(b)}

--- **A-∨:** $$ \frac{K\ldots, F_1 \vdash G \quad\quad K\ldots, F_2 \vdash G}{\text{A-}\lor: \quad K\ldots, F_1 \lor F_2 \vdash G}

Case distinction: if you know $F_1\vee F_2$, prove $G$ in both cases (two branches).

Example: $$
\frac{p(a) \vdash r(c) \quad\quad q(b) \vdash r(c)}{\text{A-}\lor: \quad p(a) \lor q(b) \vdash r(c)}

--- #### Implication **P-→:** $$ \frac{K\ldots, F_1 \vdash F_2}{\text{P-}\to: \quad K\ldots \vdash F_1 \to F_2}

To prove $F_1\to F_2$: assume $F_1$ and prove $F_2$.

Example: $$
\frac{p(a) \vdash q(b)}{\text{P-}\to: \quad \vdash p(a) \to q(b)}

--- **A-→:** $$ \frac{K\ldots \vdash F_1 \quad\quad K\ldots, F_2 \vdash G}{\text{A-}\to: \quad K\ldots, F_1 \to F_2 \vdash G}

If you have $F_1\to F_2$ as assumption: you need to prove $F_1$ (to “trigger” the implication), then you get $F_2$ to use.

---

Modus Ponens (MP): (common shortcut) $$
\frac{K\ldots, F_1, F_2 \vdash G}{\text{MP}: \quad K\ldots, F_1 \to F_2, F_1 \vdash G}

If you have both $F_1 \to F_2$ AND $F_1$ as assumptions, you get $F_2$ as a new assumption. Only one branch! _Example:_ $$ \frac{p(a), q(b) \vdash r(c)}{\text{MP}: \quad p(a) \to q(b), p(a) \vdash r(c)}

---

Modus Tollens (MT): $$
\frac{K\ldots, \neg F_2, \neg F_1 \vdash G}{\text{MT}: \quad K\ldots, F_1 \to F_2, \neg F_2 \vdash G}

If you have $F_1 \to F_2$ and $\neg F_2$, you get $\neg F_1$. --- #### Equivalence **P-↔:** $$ \frac{K\ldots \vdash F_1 \to F_2 \quad\quad K\ldots \vdash F_2 \to F_1}{\text{P-}\leftrightarrow: \quad K\ldots \vdash F_1 \leftrightarrow F_2}

To prove equivalence: prove both directions (two branches, each is an implication).

---

A-↔: (substitution)

If you have $F_1\leftrightarrow F_2$ as assumption, you can replace occurrences of $F_1$ by $F_2$ (or vice versa) in assumptions or in the goal.

---

4. Equality Rules

P-=: $$
\text{P-}=: \quad K\ldots \vdash t = t

Any term equals itself - closed immediately. --- **A-=:** (substitution) If you have $t_1 = t_2$ as assumption, you can replace occurrences of $t_1$ by $t_2$ (or vice versa) in assumptions or in the goal. --- ### 5. Quantifier Rules This is where the quiz exercises get tricky. There are four rules, and the key distinction is: | |Goal|Assumption| |---|---|---| |**Universal $\forall$**|Skolemize (new constant)|Instantiate (pick a term)| |**Existential $\exists$**|Instantiate (pick a witness)|Skolemize (new constant)| **Notation: $F[t/x]$** means "substitute $t$ for $x$ in $F$". If $F = p(x, f(x))$ and $t = a$, then $F[a/x] = p(a, f(a))$. --- **P-∀:** (Skolemization) $$ \frac{K\ldots \vdash F[\bar{x}/x]}{\text{P-}\forall: \quad K\ldots \vdash \forall x: F}

where $\bar{x}$ is a fresh Skolem constant not appearing anywhere else.

To prove “for all $x$, $F$ holds”: introduce a new arbitrary constant $\bar{x}$ and prove $F$ for that $\bar{x}$.

Example: $$
\frac{\vdash p(\bar{x})}{\text{P-}\forall: \quad \vdash \forall x: p(x)}

The $\bar{x}$ is "arbitrary but fixed" - you can't assume anything about it. --- **A-∀:** (Instantiation) $$ \frac{K\ldots, \forall x: F, F[t/x] \vdash G}{\text{A-}\forall: \quad K\ldots, \forall x: F \vdash G}

where $t$ is some term built from available symbols.

If you have $\forall x:F$ as assumption, you can instantiate it with any specific term $t$ to get $F[t/x]$ as a new assumption. The $\forall x:F$ stays available for more instantiations.

Example: $$
\frac{\forall x: p(x), p(a) \vdash q(b)}{\text{A-}\forall: \quad \forall x: p(x) \vdash q(b)}

Here we instantiated with $t = a$. --- **P-∃:** (Instantiation - need a witness) $$ \frac{K\ldots \vdash F[t/x]}{\text{P-}\exists: \quad K\ldots \vdash \exists x: F}

where $t$ is some term built from available symbols.

To prove $\exists x:F$: find a specific witness term $t$ and prove $F[t/x]$.

Example: $$
\frac{\vdash p(a)}{\text{P-}\exists: \quad \vdash \exists x: p(x)}

We "witnessed" the existence with $t = a$. --- **A-∃:** (Skolemization) $$ \frac{K\ldots, F[\bar{x}/x] \vdash G}{\text{A-}\exists: \quad K\ldots, \exists x: F \vdash G}

where $\bar{x}$ is a fresh Skolem constant not appearing anywhere else (including in $G$!).

If you have $\exists x:F$ as assumption: introduce a new constant $\bar{x}$ representing “some $x$ that satisfies $F$”, and add $F[\bar{x}/x]$ as assumption. The existential disappears (you can only skolemize it once).

Example: $$
\frac{p(\bar{x}) \vdash q(b)}{\text{A-}\exists: \quad \exists x: p(x) \vdash q(b)}

___ | Rule | When to use | Effect | | ---- | --------------------------------- | -------------------------------------------- | | GA | Goal is an assumption | Close branch | | CA | $A$ and $\neg A$ both assumptions | Close branch | | P-∧ | Goal is $F_1 \land F_2$ | Split into two branches | | A-∧ | Assumption is $F_1 \land F_2$ | Get both $F_1$ and $F_2$ | | P-∨ | Goal is $F_1 \lor F_2$ | Assume $\neg F_1$, prove $F_2$ | | A-∨ | Assumption is $F_1 \lor F_2$ | Case split (two branches) | | P-→ | Goal is $F_1 \to F_2$ | Assume $F_1$, prove $F_2$ | | MP | Have $F_1 \to F_2$ and $F_1$ | Get $F_2$ | | P-∀ | Goal is $\forall x: F$ | New constant $\bar{x}$, prove $F[\bar{x}/x]$ | | A-∀ | Assumption is $\forall x: F$ | Pick term $t$, get $F[t/x]$ | | P-∃ | Goal is $\exists x: F$ | Pick witness $t$, prove $F[t/x]$ | | A-∃ | Assumption is $\exists x: F$ | New constant $\bar{x}$, get $F[\bar{x}/x]$ |