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 quasiformal 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 onetoone (injective) functions is also onetoone. Will be proved next class. (Note that an injective function could also be the composite of one injective function and one noninjective 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. ↩