Derivation (Formal Proof)

Derivation (Formal Proof)

Deduction/Derivation/Formal proof is a sequence of formulas ${\phi }_1\cdots {\phi }_n(=\phi )$ such that for each ${\phi }_i$ (i) ${\phi }_i\in \Sigma$ or (ii) ${\phi }_i$ is a logical axioms or (iii)${\phi }_i$ is deducible from earlier ${\phi }_j$ by modus ponens or generalisation.

Syntactic Entailment

Suppose $\Sigma$ is a set of formulas, $\phi$ is a formula from the language $\mathcal{L}$ $\Sigma ⊢\phi$ means there is a deduction from formulas in $\Sigma$ to formula $\phi$.

Universal Validity of the Logical Axioms

The logical axioms are universally valid.

Inference Preserves Validity

The two rules of inference preserve validity in the following sense: (i) if $\mathfrak{A}\models \phi$ and $\mathfrak{A}\models \phi \to \psi$ then $\mathfrak{A}\models \psi$, (ii) if $\mathfrak{A}\models \phi$ then $\mathfrak{A}\models \forall v\phi$.

Combine these two theorem, we get soundness theorem.

Soundness Theorem

If $\Sigma$ is a set of formulas and $\phi$ is a formula(all in the same language $\mathcal{L}$), then $\Sigma ⊢\phi$, implies $\Sigma \models \phi$

Proof Assume $\Sigma ⊢\phi$ and ${\phi }_1,{\phi }_2,\cdots {\phi }_n(=\phi )$ is a corresponding derivation. To prove that $\Sigma \models \phi$ we need to show that if $\mathfrak{A}\models \Sigma$ then $\mathfrak{A}\models \phi$. So we assume $\mathfrak{A}\models \Sigma$. We will show by induction on $i$ that $\mathfrak{A}\models {\phi }_i$ for $i=1,...,n$. Since ${\phi }_1$ is either a logical axiom or ${\phi }_1\in \Sigma$, it follows that $\mathfrak{A}\models {\phi }_1$. Suppose $i>1$ and $\mathfrak{A}\models {\phi }_j$ for all $j<i$. If ${\phi }_i$ is a logical axiom or ${\phi }_i\in \Sigma$, then as for ${\phi }_1$, $\mathfrak{A}\models {\phi }_i$. If ${\phi }_i$ is obtained from previous ${\phi }_j$s by modus ponens or generalization, through inference preserves validity, $\mathfrak{A}\models {\phi }_j$. It follows by induction that $\Sigma \models {\phi }_n$, that is $\Sigma \models \phi$.

Remark

1.$\Sigma ⊢\phi ⟺\Sigma ⊢\forall v\phi .$ (Follow by generalization.) 2. (Finite Nature of Proofs). Since derivations are finite, it is an important immediate consequence that $\Sigma ⊢\phi$ iff ${\Sigma }_0⊢\phi$ for some finite ${\Sigma }_0\subset \Sigma$. 3.(Why these Axioms and Inference Rules?). As noted previously, we are working within a Hilbert-style system. Of course, the axioms should be true in any $\mathcal{L}$-structure under any assignment for the free variables, and the inference rules should preserve truth. This is so, and it is the main content of the Soundness Theorem