2.2  Deduction

Axiom 2.2.1. Each axiom represents a scheme, where \(\phi,\psi,\) and \(\theta\) are formulas, \(x\) is a variable, and \(t,u,\) and \(v\) are terms. All substitutions replace only free occurrences of \(x\) and require that the substituted term is free for \(x\) in the formula.

  1. \(\phi \rightarrow(\psi \rightarrow \phi).\)
  2. \((\phi \rightarrow(\psi \rightarrow \theta)) \rightarrow((\phi \rightarrow \psi) \rightarrow(\phi \rightarrow \theta)).\)
  3. \(((\neg \phi) \rightarrow(\neg \psi)) \rightarrow(\psi \rightarrow \phi).\)
  1. \((\forall x) \phi \rightarrow \phi[t / x].\)
  2. \((\forall x)(\phi \rightarrow \psi) \rightarrow(\phi \rightarrow(\forall x) \psi),\) if there is no free occurrence of \(x\) in \(\phi.\)
  1. \(t=t\).
  2. \((t=u) \rightarrow(u=t)\).
  3. \((t=u) \rightarrow((u=v) \rightarrow(t=v))\).
  4. \((t=u) \rightarrow(\phi[t / x] \rightarrow \phi[u / x]).\)

Rule 2.2.2 (Rules of inference). Let \(\phi\) and \(\psi\) be formulas, and let \(x\) be a variable. Let \(\Gamma\) be the set of undischarged assumptions.

  1. From \(\phi\) and \(\phi \rightarrow \psi,\) infer \(\psi\) (modus ponens).
  2. From \(\phi\) infer \((\forall x)\phi,\) provided \(x\) is not free in any formula of \(\Gamma\) (generalization).

Proposition 2.2.3. Let \(\phi\) be formula, \(x\) be a variable, and let \(t\) be free term for \(x\) in \(\phi.\)

  1. \((\forall x)\phi\rightarrow \phi[t/x]\) (universal instantiation).
  2. \(\phi[t/x]\rightarrow (\exists x)\phi\) (existential introduction).

Definition 2.2.4. Let \(\Gamma\) be a set of \(\mathcal L\)-formulas. A derivation from \(\Gamma\) is a finite sequence of formulas \(\phi_1,\dots,\phi_n\) in which each formula is

  1. an instance of a logical axiom scheme;
  2. a member of \(\Gamma;\) or
  3. obtained from earlier formulas by a rule of inference, with the restriction on Generalization checked against \(\Gamma.\)

We write \(\Gamma\vdash\phi\) if there is a derivation from \(\Gamma\) whose last formula is \(\phi.\) We write \(\vdash\phi\) when \(\Gamma=\varnothing,\) and call \(\phi\) a theorem of first-order logic.

Theorem 2.2.5 (Deduction theorem). Let \(T\) be an \(\mathcal L\)-theory, let \(\phi\) be an \(\mathcal L\)-sentence, and let \(\psi\) be an \(\mathcal L\)-formula. Then

\[T\cup\{\phi\}\vdash\psi \ \Longleftrightarrow\ T\vdash\phi\rightarrow\psi.\]

Definition 2.2.6. An \(\mathcal L\)-theory \(T\) is consistent if there is no \(\mathcal L\)-formula \(\phi\) such that both \(T\vdash\phi\) and \(T\vdash\neg\phi.\) Otherwise, \(T\) is inconsistent.

Proposition 2.2.7 (Finite character of deduction). Let \(T\) be an \(\mathcal L\)-theory and let \(\phi\) be an \(\mathcal L\)-formula. Then

\[T\vdash\phi \ \Longleftrightarrow\ T_0\vdash\phi\text{ for some finite }T_0\subseteq T.\]