Friday, October 14, 2011
More proofs, and some logical axioms
Note: 10th was a holiday, 12th was the midterm so yeah works out
1A proof¶
From last class:
"All horses are animals. Therefore, all heads of horses are heads of animals."
$$\forall x (Hx \to Ax) \vdash A (\exists x(Hx \land H^*yx) \to \exists x (Ax \land H^*yx))$$
Where $Hx$ means "x is a horse", $H^*xy$ means "x is the head of y", and $Ax$ means "x is an animal".
Strategy for the proof: let's try to get $\forall x ( \quad) \vdash \exists x (\quad) \to \exists x ( \quad )$ using a deduction?.
So working up from the bottom:
$$\forall x(\quad) \vdash \exists x (\quad) \to \exists x (\quad)$$
$$\forall x(\quad), \exists x(\quad) \vdash \exists x (\quad)$$
The last quantifier to be put back on: middle term.
Anyways, whatever. The proof:
| Sequent | Justification/rule |
|---|---|
| (1) $Hx \to Ax,\,Hx \land H^*yx \vdash Ax \land H^*yx$ | Tautology |
| (2) $Hx \to Ax,\,Hx \land H^*yx \vdash \exists x (Ax \land H^*yx)$ | $\exists$-introduction from (1) |
| (3) $\forall x(Hx \to Ax) \vdash Hx \to Ax$ | $\forall$-elimination |
| (4) $\forall x (Hx \to Ax),\,Hx \to Ax,\,Hx \land H^*yx \vdash \exists x (Ax \land H^*yx)$ | Monotonicity from (2) |
| (5) $\forall x (Hx \to Ax), \, Hx \land H^*yx \vdash Hx \to Ax$ | Monotonicity from (3) |
| (6) $\forall x(Hx \to Ax),\,Hx \land H^*yx \vdash \exists x (Ax \land H^*yx)$ | Transitivity using (4), (5) |
| (7) $\forall x (Hx \to Ax),\,\exists x (Hx \land H^*yx) \vdash \exists x(Ax \land H^*yx)$ | $\forall$-elimination |
| (8) $\forall x (Hx \to Ax) \vdash \exists x (Hx \land H^*yx) \to \exists x (Ax \land H^*yx)$ | Deduction from (7) |
| (9) $\forall x(Hx \to Ax) \vdash \forall y (\exists x(Hx \land H^*yx) \to \exists x(Ax \land H^*yx))$ | $\forall$-introduction from (8) |
2Some logical axioms for equality¶
- $\forall x(x = x)$ (reflexivity)
- $\forall x\forall y(x = y \to y = x)$ (symmetry)
- $\forall x \forall y \forall z ((x =y \land y = z) \to x =z)$
These are all properties of equivalence relations, and equality is, in a way, the epitome of equivalence relations.
Since these are logical axioms, you can use them in any line of a proof, in the following manner:
$$\vdash \forall x (x = x)$$
2.1Quantifying existence¶
How do you say that there is exactly one boy? (Or Buddha, or whatever.) Well, you'd have to use equality. For instance:
$$\exists x (Bx \land \forall y (By \to x = y))$$
So there is a boy, and anything else that is also a boy is the same as our original boy. So there is only one boy.
How would you say there is at most one boy?
$$\exists x \forall y (By \to y = x)$$
So if there are boys, they are all the same boy.
2.2Using the logical axioms¶
Here's a proof that uses logical axiom 1 in its first line:
$$\vdash \exists x (x = x)$$
| Sequent | Justification/rule |
|---|---|
| (1) $\vdash \forall x (x=x)$ | Logical axiom |
| (2) $\forall x(x=x) \vdash x = x$ | $\forall$-elimination |
| (3) $\vdash x = x$ | Transitivity using (1) and (2) |
| (4) $\vdash \exists x (x =x)$ | $\exists$-introduction from (3) |
This fails in an empty universe, but don't worry about that. Loveys doesn't care about empty universes and neither should you.