Monday, October 17, 2011
Proofs involving equality
1Substitution rules for equality¶
These are all standalone things, like tautologies, that can be inserted in any line of a proof?
- Say $t(x_1, ... x_n)$ is a term. Then $s_1 = t_1 ..., s_n = t_n \vdash t(s_1, ... s_n) = t(t_1,...t_n)$
- Say $\Phi(x_1, ... x_n)$ is a formula. Then $s_1=t_n, s_n=t_n \vdash \Phi(s_1,...s_n) \iff \Phi(t_1, ... t_n)$
provided we avoid a clash of variables.
For example, if we have a binary function symbol $f$ (which sort of behaves like a prefix operator, but isn't one really - just think a regular function call, without the parentheses around the arugments) in our signature, then $fx_1a = fx_2faa \vdash ffx_1ax_2 = ffx_2faax_3$. With the parentheses: $f(x_1, a) = f(x_2, f(a, a)) \vdash f(f(x_1, a), x_3) = f(f(x_2, f(a, a)), x_3)$.
2Quantifying existence continued¶
How do you say there are at least two things having property P, where P is a unary predicate symbol?
$$\exists x \exists y (Px \land Py \land x \neq y)$$
This can of course be generalised to "at least $n$ things".
You can also say there are at most $n$ things, and combining this with "at least $n$ things" you can say "there are exactly $n$ things". This seems to have been neglected in the lecture though.
3A quasi-formal proof¶
$$\exists x (Px \land Qx),\,\exists y(Py \land \neg Qy) \vdash \exists x \exists y (Px \land Py \land x \neq y)$$
| Sequent | Justification/rule |
|---|---|
| (1) $Px \land Qx,\,Py \land Qy \vdash Px \land Py$ | Tautology |
| (2) $x =y \vdash Qx \iff Qy$ | Substitution rule #2 |
| (3) $Px \land Qx,\,Px \land \neg Qy \vdash \neg (Qx \iff Qy)$ | Tautology |
| (4) $\vdash (x=y) \to (Qx \iff Qy)$ | Deduction from (2) |
| (5) $(x = y) \to (Qx \iff Qy) \vdash \neg (Qx \iff Qy) \to \neg (x=y)$ | Tautology (contrapositive) |
| (6) $\vdash \neg (Qx \iff Qy) \to \neg (x=y)$ | Transitivity using (4), (5) |
| (7) $\neg (Qx \iff Qy) \vdash \neg (x=y)$ | Deduction from (6) |
| (8) $Px \land Qx,\,Py \land \neg Qy \vdash \neg (x=y)$ | Transitivity using (3), (7)1 |
| (9) $Px \land Py,\,\neg(x=y) \vdash Px \land Py\land \neg (x=y)$ | Tautology |
| (10) $Px \land Qx,\,Py \land \neg Qy \vdash Px \land Py \land \neg (x=y)$ | Transitivity using (1), (8) and (9) |
| (11) $Px \land Qx,\,Py \land \neg Qy \vdash \exists x \exists y(Px \land Py \land \neg (x=y))$ | $\exists$-introduction (twice) |
| (12) $Px \land Qx,\,\exists y (Py \land \neg Qy) \vdash \exists x \exists y (Px \land Py \land \neg(x=y))$ | $\exists$-elimination from (11) |
| (13) $\exists x(Px \land Qx), \, \exists y(Py \land \neg Qy) \vdash \exists x \exists y (Px \land Py \land \neg (x=y))$ | $\exists$-elimination from (12) |
You could also go on two more lines to show that you can have $\exists x$ for both premises:
(14) $\exists x (Px \land \neg Qx) \vdash \exists y (Py \land \neg Qy)$ (change of bound variable - informal)
(15) $\exists x (Px \land Qx), \exists x (Px \land \neg Qx) \vdash \exists x \exists y (Px \land Py \land \neg(x=y))$
4Function composition¶
Say $f$ and $g$ are unary function symbols. Then the following is true:
$$\forall x \forall y (fx = fy \to x=y), \, \forall x \forall y(gx = gy \to x = y) \vdash \forall x \forall y (gfx = gfy \to x = y)$$
So the composition of two one-to-one (injective) functions is also one-to-one. Will be proved next class. (Note that an injective function could also be the composite of one injective function and one non-injective function. Discussed on the fall 2009 final exam, question 4.)
-
Not strictly formal because monotonicity should have been used, but it's okay, we can skip that now. ↩