Notes - Logic MT24, Example proofs in first-order logic

1. Hyp: $\forall x _ i \phi$
2. A4: $(\forall x _ i \phi \to \phi[x _ j / x _ i])$
3. MP1,2: $\phi[x _ j/x _ i]$
4. Gen: $\forall x _ j \phi[x _ j /x _ i]$

@example~

Note that $\forall x _ i (\psi \to \tau)$ is a sentence. We show

\[\\{ \forall x_i (\psi \to \tau) \\} \vdash (\exists x_i \psi \to \tau)\]

1. Hyp: $\forall x _ i (\psi \to \tau)$
2. A4: $\forall x _ i (\psi \to \tau) \to (\psi \to \tau)$
3. MP1,2: $(\psi \to \tau)$
4. Taut: $((\psi \to \tau) \to (\lnot \tau \to \lnot \psi))$
5. MP3,4: $(\lnot \tau \to \lnot \psi)$
6. Gen5: $\forall x _ i (\lnot \tau \to \lnot \psi)$
7. A5: $(\forall x _ i (\lnot \tau \to \lnot \psi) \to (\lnot \tau \to \forall x _ i \lnot \psi))$
8. MP6,7: $(\lnot \tau \to \forall x _ i \lnot \psi)$
9. Taut: $((\lnot \tau \to \forall x _ i \lnot \psi) \to (\lnot \forall x _ i \lnot \psi \to \tau))$
10. MP8,9: $(\lnot \forall x _ i \lnot \psi \to \tau)$
11. Def. $\exists$: $(\exists x _ i \psi \to \tau)$

where in (7), $x _ i \notin \text{Free}(\lnot \tau)$ because $\tau$ is a sentence, so the conditions for A5 are met.

@example~