1An example proof¶
Suppose $\Sigma$ has two unary predicate symbols $H$ and $M$, and one constant symbol $S$. Let's try to prove the following:
$$Hs,\,\forall x (Hx \to Mx) \vdash Ms$$
(An instance of transitivity, in an everyday context; an example translation would be "Socrates is human and all humans are mortal, therefore Socrates is mortal" which is almost certainly true.)
$$\begin{align*} (1) & \forall x (Hx \to Mx) \vdash Hs \to Ms \\ (2) & Hs, Hs \to Ms \vdash Ms \\ (3) & Hs, \forall x (Hx \to Mx) \vdash Hs \to Ms \\ (4) & Hs, \forall x(Hx \to Mx), Hs \to Ms \vdash Ms \\ (5) & Hs, \forall x (Hx \to Mx) \vdash Ms\,\, \blacksquare \end{align*}$$
(The last line of the proof was, of course, the sentence we wanted to prove, as it should be.)
1.1Justifications¶
Note: the justification is not necessary in a completely formal proof. Neither are the line numbers. They're only included here to increase understanding etc. (Also, Loveys will often ask for justification.)
(1) Straightforward use of $\forall$elimination
(2) Tautology rule
(3) Added the formula $Hs$; monotonicity from (1)
(4) Transitivity from (3), (4) (cut the $Hs \to Ms$)
This could have actually been done in 3 lines, using deduction.
2Another example proof¶
Consider: Every good boy deserves fudge. Every boy is good. Therefore, every boy deserves fudge.
We can translate this into predicate form using the following unary predicate symbols: $G$ (meaning "is good"), $B$ (meaning "is a boy"), and $F$ (meaning "deserves fudge").
$$\forall x((Bx \land Gx) \to Fx), \forall x (Bx \to Gx) \vdash \forall x (Bx \to Fx)$$
Before we can use the tautology rule, we have to get rid of all the quantifiers. Here's the proof:
Sequent  Justification/rule 

(1) $\forall x ((Bx \land Gx) \to Fx) \vdash (Bx \land Gx) \to Fx$  $\forall$elimination 
(2) $\forall x (Bx \to Gx) \vdash Bx \to Gx$  $\forall$elimination 
(3) $(Bx \land Gx) \to Fx,\,Bx \to Gx \vdash Bx \to Fx$^{1}  Tautology 
(4) $\forall x ((Bx \land Gx) \to Fx),\,Bx \to Gx \vdash (Bx \land Gx) \to Fx$  Monotonicity from (1) 
(5) $\forall x ((Bx \land Gx) \to Fx), \, (Bx \land Gx) \to Fx, \, Bx \to Gx \vdash Bx \to Fx$  Monotonicity from (3) 
(6) $\forall x ((Bx \land Gx) \to Fx),\, Bx \to Gx vdash Bx \to Fx$  Transitivity using (4), (5) 
(7) $\forall x ((Bx \land Gx) \to Fx), \, \forall x(Bx \to Gx) \vdash Bx \to Gx$  Monotonicity from (2) 
(8) $\forall x ((Bx \land Gx) \to Fx),\, \forall x (Bx \to Gx),\, Bx \to Gx \vdash Bx \to Fx$  Monotonicity from (6) 
(9) $\forall x ((Bx \land Gx) \to Fx),\, \forall x (Bx \to Gx) \vdash Bx \to Fx$  Transitivity using (7), (8) 
(10) $\forall x ((Bx \land Gx) \to Fx),\, \forall x (Bx \to Gx) \vdash \forall x (Bx \to Fx) \quad \blacksquare$  $\forall$introduction^{2} 
3More quantifier rules¶
3.1Forall introduction¶
$$\frac{\Gamma \vdash \forall(x)}{\Gamma \vdash \forall x \Phi(x)}$$
provided $x$ does not occur free (bound is okay) anywhere in $\Gamma$ (in other words, take care to avoid clash of variables). If there's a free $x$ on the left, then you'd have to bind it up first before you can do this.
Here's an example of why it works. If you say "let $n$ be a natural number" and reach a conclusion, you can generalise that conclusion for all natural numbers, since $n$ was arbitrary.
3.2Exists introduction¶
Or, "existential generalisation". There are two rules for $\exists$ introduction and elimination, similar to the ones for $\forall$, but slightly more subtle. The rule is:
$$\frac{\Gamma \vdash \Phi(x)}{\Gamma \vdash \exists x \Phi(x)}$$
provided there is no clash of variables, i.e. no variables in $t$ become bound when $t$ is substituted for $x$ in $\Phi(x)$. This is really just making a statement weaker.
4Yet another proof¶
"Every boy deserves fudge. Charlie is a boy. Therefore, somebody deserves fudge."
$$\forall x (Bx \to Fx), Bc \vdash \exists x Fx$$
Sequent  Justification/rule 

(1) $\forall x(Bx \to Fx( \vdash Bx \to Fc$  $\forall$elimination 
(2) $Bc \to Fc, Bc \vdash Fc$  Tautology 
(3) $\forall x (Bx \to Fx),\,Bc \to Fc, \,Bc \vdash Fc$  Monotonicity from (2) 
(4) $\forall x (Bx \to Fx),\,Bx \vdash Bc \to Fc$  Monotonicity from (1) 
(5) $\forall x (Bx \to Fx), \, Bc \vdash Fc$  Transitivity using (3), (4) 
(6) $\forall x (Bx \to Fx),\,Bc \vdash \exists x Fx$  $\exists$introduction 

We have to put the quantifiers back on at the end, but we needed to get rid of them first to be able to invoke the tautology rule here. ↩

To be covered in the next section. Lambdek (textbook author) calls this "universal generalisation", and calls $\forall$introduction "universal specification". Is usually only used near the end of a proof. ↩