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:

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.”

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,\dots ⊢G$

where $K_1,K_2,\dots$ are the assumptions (what we know) and $G$ is the goal (what we want to prove). The turnstile $⊢$ 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}:K\dots ,G⊢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}:K\dots ,A,\neg A⊢G$

If you have both $A$ and $\neg A$ among assumptions, you can prove anything (contradiction).

Example: $p(a),\neg p(a)⊢q(b)$ — closed, we have contradictory assumptions.

FalseAssum: $\text{FalseAssum}:K\dots ,\perp ⊢G$

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

2. Structural Rules

Drop: $\frac{K\dots ⊢G}{\text{Drop}:K\dots ,A⊢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\dots ⊢AK\dots ,A⊢G}{\text{Cut}:K\dots ⊢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\dots ,\neg G⊢\perp }{\text{Indirect}:K\dots ⊢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\dots ,G⊢\perp }{\text{P-}\neg :K\dots ⊢\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\dots ,\neg G⊢A}{\text{A-}\neg :K\dots ,\neg A⊢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\dots ⊢F_{1}K\dots ⊢F_2}{\text{P-}\wedge :K\dots ⊢F_1\wedge F_2}$

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

Example: $\frac{⊢p(a)⊢q(b)}{\text{P-}\wedge :⊢p(a)\wedge q(b)}$

A-∧: $\frac{K\dots ,F_1,F_2⊢G}{\text{A-}\wedge :K\dots ,F_1\wedge F_2⊢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)⊢r(c)}{\text{A-}\wedge :p(a)\wedge q(b)⊢r(c)}$

Disjunction

P-∨: $\frac{K\dots ,\neg F_1⊢F_2}{\text{P-}\vee :K\dots ⊢F_1\vee 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)⊢q(b)}{\text{P-}\vee :⊢p(a)\vee q(b)}$

A-∨: $\frac{K\dots ,F_1⊢GK\dots ,F_2⊢G}{\text{A-}\vee :K\dots ,F_1\vee F_2⊢G}$

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

Example: $\frac{p(a)⊢r(c)q(b)⊢r(c)}{\text{A-}\vee :p(a)\vee q(b)⊢r(c)}$

Implication

P-→: $\frac{K\dots ,F_1⊢F_2}{\text{P-}\to :K\dots ⊢F_1\to F_2}$

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

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

A-→: $\frac{K\dots ⊢F_{1}K\dots ,F_2⊢G}{\text{A-}\to :K\dots ,F_1\to F_2⊢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\dots ,F_1,F_2⊢G}{\text{MP}:K\dots ,F_1\to F_2,F_1⊢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)⊢r(c)}{\text{MP}:p(a)\to q(b),p(a)⊢r(c)}$

Modus Tollens (MT): $\frac{K\dots ,\neg F_2,\neg F_1⊢G}{\text{MT}:K\dots ,F_1\to F_2,\neg F_2⊢G}$

If you have $F_1\to F_2$ and $\neg F_2$, you get $\neg F_1$.

Equivalence

P-↔: $\frac{K\dots ⊢F_1\to F_{2}K\dots ⊢F_2\to F_1}{\text{P-}\leftrightarrow :K\dots ⊢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-}=:K\dots ⊢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:

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\dots ⊢F[\bar{x}/x]}{\text{P-}\forall :K\dots ⊢\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{⊢p(\bar{x})}{\text{P-}\forall :⊢\forall x:p(x)}$

The $\bar{x}$ is “arbitrary but fixed” - you can’t assume anything about it.

A-∀: (Instantiation) $\frac{K\dots ,\forall x:F,F[t/x]⊢G}{\text{A-}\forall :K\dots ,\forall x:F⊢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)⊢q(b)}{\text{A-}\forall :\forall x:p(x)⊢q(b)}$

Here we instantiated with $t=a$.

P-∃: (Instantiation - need a witness) $\frac{K\dots ⊢F[t/x]}{\text{P-}\exists :K\dots ⊢\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{⊢p(a)}{\text{P-}\exists :⊢\exists x:p(x)}$

We “witnessed” the existence with $t=a$.

A-∃: (Skolemization) $\frac{K\dots ,F[\bar{x}/x]⊢G}{\text{A-}\exists :K\dots ,\exists x:F⊢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})⊢q(b)}{\text{A-}\exists :\exists x:p(x)⊢q(b)}$