Logic MT24, Example proofs in first-order logic

Created: January 09, 2025 | Updated: May 16, 2025 | Read markdown | About these notes | View in context | Study these flashcards |

Flashcards

Suppose:

  • $\mathcal L$ is a first-order language
  • $\phi \in \mathrm{Form}(\mathcal L)$
  • $\mathrm{Free}(\phi) = \{x _ i\}$
  • $\phi[x _ j / x _ i]$ is defined

@Prove in $K(\mathcal L)$ that then:

\[\{\forall x _ i \phi\} \vdash \forall x _ j \phi[x _ j / x _ i]\]
k-proof-bound-variable-renaming
  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~

Suppose:

  • $\mathcal L$ is a first-order language
  • $\tau \in \mathrm{Sent}(\mathcal L)$
  • $\psi \in \mathrm{Form}(\mathcal L)$
  • $\mathrm{Free}(\psi) \subseteq \{x _ i\}$

@Prove in $K(\mathcal L)$ that then:

\[\vdash ( \forall x _ i (\psi \to \tau) \to (\exists x _ i \psi \to \tau) )\]
k-proof-exists-elimination

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 \mathrm{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.

Finally, the deduction theorem gives $\vdash (\forall x _ i (\psi \to \tau) \to (\exists x _ i \psi \to \tau))$ (this is why we noted that $\forall x _ i (\psi \to \tau)$ is a sentence).

@example~

Suppose:

  • $\mathcal L$ is a first-order language
  • $\alpha, \beta \in \mathrm{Form}(\mathcal L)$
  • $\mathrm{Free}(\alpha), \mathrm{Free}(\beta) \subseteq \{x _ 0\}$ (so the universal closures over $x _ 0$ below are sentences, as the deduction theorem requires)

@Prove in $K(\mathcal L)$ that then:

\[\vdash ( \forall x _ 0 (\alpha \to \beta) \to (\exists x _ 0 \alpha \to \exists x _ 0 \beta) )\]
k-proof-exists-monotone

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~



Related posts