Deductive Calculus

  • Deductions are formal proofs
  • Given a set of formula $\Lambda$ called logical axioms, the theorems of a set of formula $\Gamma$ are formulas obtained from $\Lambda\cup\Gamma$ by using the rules of inference.
  • The choice of the rules of inference and $\Lambda$ are arbitrary.
  • An example for the choice of rules of inference Modus ponens: $\alpha,\alpha\rightarrow\beta\vdash\beta$
  • A deduction of $\varphi$ from $\Gamma$ is a finite sequence $\langle a_1,\ldots,a_n\rangle\ni a_n=\varphi\land\forall k\le n:$
    • $a_k\in\Gamma\cup\Lambda$ or
    • $\exists\ i<k,j<k:\alpha_j=\alpha_i\rightarrow\alpha_k$
  • If a deduction of $\varphi$ from $\Gamma$ exists, we say $\varphi$ is deducible from $\Gamma$ or that $\varphi$ is a theorem of $\Gamma$, and we write it as $\Gamma\vdash\varphi$
  • Rules of inference as an operation may not be totally defined or generate theorems freely.
  • $\mathrm{wff}\ \varphi$ is a generalization of $\psi\ \mathrm{iff}$ $\varphi=\forall x_1\ldots\forall x_n\psi$
  • Prime formulas are either atomic formulas or formula of the form $\forall\ x\ \varphi$. Tautologies in FOL are obtained by replacing sentential symbols in tautology in sentential logic with prime formulas.
  • $\mathrm{wff}$ in FOL are also $\mathrm{wff}$ in sentential logic.
  • Substitution of $x$ by $t$ in $\alpha$, $\alpha^x_t$ is defined as:
    1. For an atomic $\alpha$, replace occurrences of $x$ with $t$
    2. $(\alpha\rightarrow\beta)^x_t=(\alpha^x_t\rightarrow\beta^x_t)$
    3. $(\forall\ y\ \alpha)^x_t=\begin{cases}\forall\ y\ \alpha&&\text{if }x=y\\forall\ y(\alpha^x_t)&&\text{if }x\ne y\end{cases}$
  • An example for the choice of $\Lambda$:
    1. Tautologies
    2. $\forall\ x\ \alpha\rightarrow\alpha^x_t$ where $t$ is substitutable for $x$ in $\alpha$
    3. $\forall\ x\ (\alpha\rightarrow\beta)\rightarrow(\forall \ x\ \alpha\rightarrow\forall\ x\ \beta)$
    4. $\alpha\rightarrow\forall\ x\ \alpha$ where $x$ does not freely occur in $\alpha$
    5. $x=x$
    6. $x=y\rightarrow(\alpha\rightarrow\alpha’)$ where $\alpha’$ is an atomic obtained from $\alpha$ by replacing some or all $x$ with $y$
  • $\Gamma\models\varphi\longrightarrow\Gamma\vdash\varphi$. Since modes ponens is a tautological implication, with modus ponens as the rule of inference, we have $\Gamma\models\varphi\longleftrightarrow\Gamma\vdash\varphi$