Logic MT24, Example proofs in first-order logic

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

Flashcards

Suppose:

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

Give a proof in $K(\mathcal L)$ that then:

\[\\{\forall x_i \phi\\} \vdash \forall x_j \phi[x_j / x_i]\]
  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 \text{Sent}(\mathcal L)$
  • $\psi \in \text{Form}(\mathcal L)$
  • $\text{Free}(\psi) \subseteq \{i\}$

Give a proof in $K(\mathcal L)$ that then:

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

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~

Suppose:

  • $\mathcal L$ is a first-order language
  • $\alpha, \beta \in \text{Form}(\mathcal L)$

Give a proof in $K(\mathcal L)$ that then:

\[\vdash ( \forall x_0 (\alpha \to \beta) \to (\exists x_0 \alpha \to \exists x_0 \beta) )\]

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