Hilbert Deductive System

Axioms

Propositional Axioms Logical Axioms Axioms for Equality

Rules of inferences

Modus Ponens Generalization

At this stage, we’ll use proof in a line structure, but generally speaking there’s no restriction on that(eg tree structure proof.)

Remark

In this note, we use $⟹,⟺,$ when we’re talking about metalanguage(eg English)

Definition

$\Sigma$ is set of sentences in language $\mathcal{L}$, we say $C_1\sim C_2$ iff $\Sigma ⊢C_1=C_2$

Claim: This is an equivalence relation on constant symbols.

Proof: (i) $C\sim C$ (ii) $C_1\sim C_2⟹C_2\sim C_1$ (iii) $C_1\sim C_2,C_2\sim C_3⟹C_1\sim C_3$ That is want to show (i) $\Sigma ⊢C=C$ $u=u$ (Equality Axiom) $\forall u(u=u)$ (Generalization) $\forall u(u=u)\to C=C$ (Second Quantifier Axiom--- C a constant thus a term ) $C=C$, (Modus Ponens) (ii) if $\Sigma ⊢C_1=C_2$ then $\Sigma ⊢C_2=C_1$ Suppose we have a formal proof ${\phi }_1\dots {\phi }_n(\text{is equal to}(C_1=C_2))$ $u=v\to v=u$(Equality Axiom) $\forall v(u=v\to u=v)$(Generalization) $\forall u,\forall v(u=v\to u=v)$(Generalization) $C_1=C_2\to C_2=C_1$(Quantifier Axiom) $C_2=C_1$(Modus Ponens) (iii) if $\Sigma ⊢C_1=C_2$ and $\Sigma ⊢C_2=C_3$ then $\Sigma ⊢C_1=C_3$ Suppose we have a formal proof ${\phi }_1\dots {\phi }_n(\text{is equal to}(C_1=C_2))$, and a formal proof ${\psi }_1\dots {\psi }_n(\text{is equal to}(C_2=C_3))$. Then ${\phi }_1\dots {\phi }_n,{\psi }_1\dots {\psi }_n(\text{is equal to}(C_2=C_3))$ is a formal proof, by tautology $\phi \to (\psi \to (\psi \wedge \phi ))$, we get ${\phi }_1\dots {\phi }_n,{\psi }_1\dots {\psi }_n(\text{is equal to}(C_2=C_3)),{\phi }_n\to ({\psi }_n\to ({\psi }_n\wedge {\phi }_n))$ is a formal proof. Furthermore, by Modus Ponens we get ${\phi }_1\dots {\phi }_n,{\psi }_1\dots {\psi }_n,{\phi }_n\to ({\psi }_n\to ({\psi }_n\wedge {\phi }_n)),{\psi }_n\to ({\phi }_n\wedge {\psi }_n)$ , again by Modus Ponens, we get ${\phi }_1\dots {\phi }_n,{\psi }_1\dots {\psi }_n{\phi }_n\to ({\psi }_n\to ({\psi }_n\wedge {\phi }_n)),{\psi }_n\to ({\phi }_n\wedge {\psi }_n),{\phi }_n\wedge {\psi }_n$ From Equality Axiom, $(u=v\wedge v=w)\to (u=w)$. From Generalization Rule, we get $\forall u(u=v\wedge v=w)\to (u=w),$ again from Generalization Rule, $\forall v\forall u(u=v\wedge v=w)\to (u=w)$ again from Generalization Rule, $\forall w\forall v\forall u(u=v\wedge v=w)\to (u=w)$. For $C_1,C_2,C_3$ constant, from Quantifier Axiom $(C_1=C_2\wedge C_2=C_3)\to C_1=C_3$ So we get ${\phi }_1\dots {\psi }_n,{\phi }_n\to ({\psi }_n\to ({\psi }_n\wedge {\phi }_n)),{\psi }_n\to ({\phi }_n\wedge {\psi }_n),{\phi }_n\wedge {\psi }_n,(C_1=C_2\wedge C_2=C_3)\to C_1=C_3$ by Modus Ponens, we get $C_1=C_3$ in the formal proof.

Remark: If $\Sigma ⊢\phi$, $\Sigma ⊢\psi$ then $\Sigma ⊢(\phi \to (\psi \to \phi \wedge \psi ))$ is a proof follow generalization not an axiom but $\phi \to (\psi \to \phi \wedge \psi )$ is the Propositional Axiom.

$⊢\phi \to \psi ⟺\phi ⊢\psi ⟺\phi \models \psi ⟺\models \phi \to \psi$

Existential Generalisation

Suppose $\phi (v)$ is a formula of $\mathcal{L}$, $\phi (t)$ is obtained from $\phi$ by substituting $t$ for each free occurrence of $v$ in $\phi$, and no variable of $t$ occurs bound in $\phi$ at the places where it is substituted. Then $⊢$

Deduction Theorem

Suppose $\Sigma$ is a set of formulas, $\sigma$ is a sentence, $\tau$ is a formula, then $\Sigma \cup \{\sigma \}⊢\tau ⟺\Sigma ⊢\sigma \to \tau$

remark: when we’re discussing proof, we’re using meta language rather than $\mathcal{L}$.

Proof: Stick $\tau ,\sigma$ at the end of the proof $\Sigma ⊢\sigma \to \tau$.

$⟹$ direction: Let ${\phi }_1\dots {\phi }_n$ be a formal proof of $\Sigma \cup \{\sigma \}⊢\tau$. We’ll show by induction on $i$, that $\Sigma ⊢\sigma \to {\phi }_i$. Note $\Sigma \cup \{\sigma \}⊢{\phi }_i\{i=1,\dots ,n\}$

(i)If ${\phi }_i$ is an axiom or ${\phi }_i\in \Sigma$, want to show $\Sigma ⊢\sigma \to {\phi }_i$ $\Sigma ⊢{\phi }_i$ $\Sigma ⊢{\phi }_i\to (\sigma \to {\phi }_i)$ (tautology, propositional axiom) $\Sigma ⊢\sigma \to {\phi }_i$ (Modus Ponens)

(ii)If ${\phi }_i\text{is}\sigma$, then $\sigma \to \sigma$ is such a derivation ($\sigma \to \sigma$is a tautology of $\mathcal{L}$) (iii) If ${\phi }_i$ is deduced by modus ponens from ${\phi }_j$ and from ${\phi }_k={\phi }_j\to {\phi }_i,(j,k<i)$, let ${\theta }_1,\dots ,{\theta }_n,\sigma \to {\phi }_j$ be the derivation for $\Sigma ⊢\sigma \to {\phi }_j$, and ${\theta }_1^{\prime },\dots ,{\theta }_m^{\prime },\sigma \to ({\phi }_j\to {\phi }_i)$ be the derivation for $\Sigma ⊢\sigma \to ({\phi }_j\to {\phi }_i)$.

Then the following is a derivation for $\Sigma ⊢\sigma \to {\phi }_i$:

$\begin{array}{rlrl}& {\theta }_1,\dots ,{\theta }_n,\sigma \to {\phi }_j,{\theta }_1^{\prime },\dots ,{\theta }_m^{\prime },\sigma \to ({\phi }_j\to {\phi }_i),& & \\ & (\sigma \to ({\phi }_j\to {\phi }_i))\to ((\sigma \to {\phi }_j)\to (\sigma \to {\phi }_i)),& & (\text{propositional axiom})\\ & (\sigma \to {\phi }_j)\to (\sigma \to {\phi }_i),& & (\text{modus ponens})\\ & \sigma \to {\phi }_i.& & (\text{modus ponens})\end{array}$

(iv) If ${\phi }_i$ is deduced from ${\phi }_j$ by generalisation, i.e. ${\phi }_i=\forall v{\phi }_j$, let ${\theta }_1,\dots ,{\theta }_n,\sigma \to {\phi }_j$ be a derivation for $\Sigma ⊢\sigma \to {\phi }_j$. Then the following is a derivation for $\Sigma ⊢\sigma \to {\phi }_i$. (Note that in the application of quantifier axiom 1, $v$ is not free in $\sigma$ since $\sigma$ is a sentence.)

$\begin{array}{rlrl}& {\theta }_1,\dots ,{\theta }_n,\sigma \to {\phi }_j,& & \\ & \forall v(\sigma \to {\phi }_j),& & (\text{generalisation})\\ & \forall v(\sigma \to {\phi }_j)\to (\sigma \to \forall v{\phi }_j),& & (\text{quantifier axiom 1})\\ & \sigma \to \forall v{\phi }_j.& & (\text{modus ponens})\end{array}$

By induction $\Sigma ⊢\sigma \to {\phi }_j$, $\&$ $\Sigma ⊢\sigma \to ({\phi }_j\to {\phi }_i)$.