Talk:Diagonal lemma/Proof with diagonal formula/Conjunction and equality reduced to substitution

Axioms we use

We have to resort only tp some “common” axioms for first-order languages (logical axioms, equality axioms). We do not have to use any “specific” axioms for the discussed theory, here: any of the Peano axioms.

We shall use quantification on variables of the object language many times. Thus, x, y, z etc. will denote metavariable (from metal language) on variables of object language.

Sometimes, such quantification is not needed, and we can refer directly to a (concrete) varialble of the object language (or to the corresponding structural descriptive name from meta language). Thus, for sake of ergonomity (Occam's razor), we shall not fade/blur the mentioned distinction, and let our notation system reflect such sophisticated things.

Thus, let $\square$ denote a variable of the object language (or its corresponding structural descriptive name from the meta language). In brief, $\square :\in \mathbf {Var}$

Common:

$\left\{\square {\hat {=}}\square \right\}$

$\left\{\left(x{\hat {=}}y\right)\;{\hat {\rightarrow }}\;\left(\phi [\square :=x]{\hat {\rightarrow }}\phi [\square :=y]\right)\mid x,y\in \mathbf {Var} ,\phi \in \mathbf {Form} \right\}$

$\left\{{\hat {\forall }}\left(\phi \right){\hat {\rightarrow }}\phi [x:=t]\mid \phi \in \mathbf {Form} ,t\in \mathbf {Term} \right\}$

Let us work on a concrete example: Can

$y=s\left(s\left(s\left(0\right)\right)\right)\land \phi$

be deduced to

$\phi [y:=s\left(s\left(s\left(0\right)\right)\right)]$

Term identity lemma

For all $t\in \mathbf {Term}$, $\emptyset \vdash t{\hat {=}}t$

Main lemma

Now, let us use this scheme of logical axioms:

• $\left\{{\hat {\forall }}x\left(\phi \right){\hat {\rightarrow }}\phi [x:=t]\mid x\in \mathbf {Var} ,\phi \in \mathbf {Form} ,t\in \mathbf {Term} \right\}$
• deduction theorem as a lemma (the latter can be proved from Hilbert system, too)

and thus we can deduce

$\left\{s{\hat {=}}t,\phi [z:=s]\right\}\vdash \phi [z:=t]$

for all $\phi \in \mathbf {Form}$, $s,t\in \mathbf {Term}$, $z\in \mathbf {Var}$.

See detailed proof in p. 136–137 of .

Conjunction lemma

We are almost ready. We have to use the following lemme yet:

For all $\phi ,\psi ,\xi \in \mathbf {Form}$, if $\left\{\phi ,\psi \right\}\vdash \xi$, then $\left\{\phi {\hat {\land }}\psi \right\}\vdash \xi$

Proof can be figured by solving the exercises in p. 137 of .