# 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¶

1. $\forall x(x = x)$ (reflexivity)
2. $\forall x\forall y(x = y \to y = x)$ (symmetry)
3. $\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.