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$.

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