Section 2.4: A Deductive Calculus

Suppose that $\Sigma\vDash\tau$ . What methods of proof might be required to demonstrate that fact? Is there necessarily a proof at all?

• Finiteness. This is potentially possible due to the Compactness Theorem for First-Order Logic (to be proved in Section 2.5) implying that only a finite subset of $\Sigma$ is needed to prove $\Sigma\vDash\tau$ .
• Decidability. Each step of the proof should be able to be verified, implying the set of proofs from the empty set of hypotheses ($\Sigma=\emptyset$ ) should be decidable. This would, in particular, imply that the set of all validities is effectively enumerable. This is potentially possible due to the Enumerability Theorem (to be proved in Section 2.5) implying that, under reasonable assumptions, the validities are effectively enumerable.

Deductions

1. Tautologies.
   A prime formula is either an atomic formula or one of the form $\forall x\alpha$ . A nonprime formula is any other formula (built up from prime formulas using $\neg$ and $\rightarrow$ ).
   Given any wff, it is build up from prime formulas by using $\mathcal{E}_{\neg}$ and $\mathcal{E}_{\rightarrow}$ , hence, can be considered as a wff of sentential logic where all prime formulas are considered as sentence symbols. A wff is called a tautology iff it is a tautology of sentential logic. Similarly, tautological implications are defined.
   • If $\Gamma$ tautologically implies $\phi$ , then $\Gamma$ logically implies $\phi$ , but not necessarily vice versa.
2. $\forall x\alpha\rightarrow\alpha_{t}^{x}$ where $t$ is substitutable for $x$ in $\alpha$ .
   $\alpha_{t}^{x}$ is defined as follows: a) if $\alpha$ is atomic, $t$ replaces each $x$ , b) $(\neg\alpha)_{t}^{x}=(\neg\alpha_{t}^{x})$ , c) $(\alpha\rightarrow\beta)_{t}^{x}=(\alpha_{t}^{x}\rightarrow\beta_{t}^{x})$ , d) $(\forall x\alpha)_{t}^{x}=\forall x\alpha$ , and e) $(\forall y\alpha)_{t}^{x}=\forall y\alpha_{t}^{x}$ , $y\neq x$ .
   $t$ is substitutable for $x$ in $\alpha$ iff: a) if $\alpha$ is atomic, b) if $\alpha=(\neg\beta)$ and $t$ is substitutable for $x$ in $\beta$ , c) $\alpha=(\beta\rightarrow\gamma)$ and $t$ is substitutable for $x$ in $\beta$ and $\gamma$ , or d) if $\alpha=(\forall y\beta)$ and [$x$ does not occur free in $\alpha$ ] or [$y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\beta$ ].
   Note: $x$ is always substitutable for $x$ , and $t$ not containing any variables that occur in $\alpha$ is always substitutable for any $x$ in $\alpha$ .
   For any $\alpha$ , $t$ and $x$ there is always $\alpha'$ “equivalent” to $\alpha$ such that $t$ is substitutable for $x$ in $\alpha'$ (see the Existence of Alphabetic Variants Theorem below; the idea is that the only substitutability problem we may encounter is in the case of some $\forall y\beta$ where $y\neq x$ , $x$ is free in $\beta$ , $t$ is substitutable for $x$ in $\beta$ , but $y$ occurs in $t$ , in which case we rewrite it as $\forall z\beta_{z}^{y}$ ).
3. $\forall x(\alpha\rightarrow\beta)\rightarrow(\forall x\alpha\rightarrow\forall x\beta)$ .
4. $\alpha\rightarrow\forall x\alpha$ where $x$ does not occur free in $\alpha$ .
5. (if the language has $=$ ) $x=x$ .
6. (if the language has $=$ ) $x=y\rightarrow\alpha\rightarrow\alpha'$ where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in zero or more but not necessary all places by $y$ .

1. Modus ponens: From $\alpha$ , $\alpha\rightarrow\beta$ we infer $\beta$ .

• $\Gamma\vdash\alpha$ iff $\Gamma\cup\Lambda$ tautologically implies $\alpha$ .
• If $\alpha$ tautologically implies $\beta$ , then $\alpha$ logically implies $\beta$ .

Additional Rules of Inference

• (Generalization on Constants) If $\Gamma\vdash\alpha$ and a constant symbol $c$ does not occur in any wffs in $\Gamma$ , then there is a variable $x$ that does not occur in $\alpha$ such that $\Gamma\vdash\forall x\alpha_{x}^{c}$ (and a deduction of $\forall x\alpha_{x}^{c}$ from $\Gamma$ that does not use $c$ ).
  • If $\Gamma\vdash\alpha_{c}^{x}$ where the constant symbol $c$ does not occur in any wffs in $\Gamma$ or $\alpha$ , then $\Gamma\vdash\forall x\alpha$ (and there is a deduction of $\forall x\alpha$ from $\Gamma$ that does not not use $c$ ).
  • (Rule EI - Existential Instantiation) If $\Gamma;\alpha_{c}^{x}\vdash\beta$ where the constant symbol $c$ does not occur in any wffs in $\Gamma$ , $\alpha$ or $\beta$ , then $\Gamma;\exists x\alpha\vdash\beta$ (and there is a deduction of $\beta$ from $\Gamma;\exists x\alpha$ that does not use $c$ ).

• For every consistent $\Gamma$ there is a consistent $\Delta\supseteq\Gamma$ such that for every wff $\alpha$ , either $\alpha\in\Delta$ or $(\neg\alpha)\in\Delta$ .

• The formulas $\alpha'$ as described in the theorem are called alphabetic variants of $\alpha$ .

Strategy

1. If $\phi=(\alpha\rightarrow\beta)$ , it is sufficient (and always possible) to show $\Gamma;\alpha\vdash\beta$ .
2. If $\phi=\forall x\alpha$ ,
   1. If $x$ does not occur free in $\Gamma$ , it is sufficient (and always possible) to show $\Gamma\vdash\alpha$ .
   2. If $x$ does occur free in $\Gamma$ , it is sufficient (and always possible) to show $\Gamma\vdash\alpha_{y}^{x}$ using the Re-Replacement Lemma.
3. If $\phi=(\neg\alpha)$ ,
   1. If $\alpha=(\beta\rightarrow\gamma)$ , it is sufficient (and always possible) to show $\Gamma\vdash\{\beta,\neg\gamma\}$ .
   2. If $\alpha=\neg\beta$ , it is sufficient (and always possible) to show $\Gamma\vdash\beta$ .
   3. If $\alpha=\forall x\beta$ , it is sufficient to show $\Gamma\vdash\neg\beta_{t}^{x}$ where $t$ is substitutable for $x$ in $\beta$ , but it is not always possible.
      1. One can try, $\Gamma;\gamma\vdash\neg\forall x\beta$ iff $\Gamma;\forall x\beta\vdash\neg\gamma$ , or $\Gamma;\forall y\gamma\vdash\neg\forall x\beta$ if $\Gamma;\forall x\beta\vdash\neg\gamma$ .
      2. Reductio ad absurdum.