Monday, October 3, 2011 CC-BY-NC
Some example proofs and more quantifier rules

Maintainer: admin

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


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$-introduction2

3More quantifier rules

3.1For-all 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
  1. 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. 

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