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. The key step is the use of A5 in step (7), since this is the axiom that talks about rules for distributing quantifiers over implications.

@example~

We use the deduction theorem twice. First we prove $\forall x _ 0 \lnot \alpha$ in $\{\forall x _ 0 (\alpha \to \beta), \forall x _ 0 \lnot \beta\}$.

1. HYP: $\forall x _ 0 (\alpha \to \beta)$
2. A4: $\forall x _ 0 (\alpha \to \beta) \to (\alpha \to \beta)$
3. MP: $(\alpha \to \beta)$
4. HYP: $\forall x _ 0 \lnot \beta$
5. A4: $\forall x _ 0 \lnot \beta \to \lnot \beta$
6. MP: $\lnot \beta$
7. TAUT: $((\alpha \to \beta) \to (\lnot \beta \to \lnot \alpha))$
8. MP: $(\lnot \beta \to \lnot \alpha)$
9. MP: $\lnot \alpha$
10. GEN: $\forall x _ 0 \lnot \alpha$

Now we prove $\exists x _ 0 \alpha \to \exists x _ 0 \beta$ in $\{\forall x _ 0 (\alpha \to \beta)\}$:

1. DT: $\forall x _ 0 \lnot \beta \to \forall x _ 0 \lnot \alpha$
2. TAUT: $(\forall x _ 0 \lnot \beta \to \forall x _ 0 \lnot \alpha) \to (\lnot \forall x _ 0 \lnot \alpha \to \lnot \forall x _ 0 \lnot \beta)$
3. MP: $\lnot \forall x _ 0 \lnot \alpha \to \lnot \forall x _ 0 \lnot \beta$
4. DEF: $\exists x _ 0 \alpha \to \exists x _ 0 \beta$

And finally we prove $\forall x _ 0 (\alpha \to \beta) \to (\exists x _ 0 \alpha \to \exists x _ 0 \beta)$ in $\{\}$, i.e. what the question asks:

1. DT: $\forall x _ 0 (\alpha \to \beta) \to (\exists x _ 0 \alpha \to \exists x _ 0 \beta)$

@example~ @exam~