Monday, October 3, 2011

Some example proofs and more quantifier rules

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:

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