Monday, October 17, 2011 CC-BY-NC
Proofs involving equality

Maintainer: admin

1Substitution rules for equality

These are all standalone things, like tautologies, that can be inserted in any line of a proof?

  1. 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)$
  2. 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.)

  1. Not strictly formal because monotonicity should have been used, but it's okay, we can skip that now.