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
denote a variable of the object language (or its corresponding structural descriptive name from the meta language). In brief,
Common:
![{\displaystyle \left\{\square {\hat {=}}\square \right\}}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/5a4bfdb16556a132c55a1a0f43595bafa1e74885)
![{\displaystyle \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\}}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/108f1fedabdf5d4a04d6e4de8429e12e77ce73a5)
![{\displaystyle \left\{{\hat {\forall }}\left(\phi \right){\hat {\rightarrow }}\phi [x:=t]\mid \phi \in \mathbf {Form} ,t\in \mathbf {Term} \right\}}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/165734bdc3eb1fcdfda84d0a2cd458f7671caf68)
Let us work on a concrete example:
Can
![{\displaystyle y=s\left(s\left(s\left(0\right)\right)\right)\land \phi }](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/c74cc69bda51bca2ab6b47901943a7ebc1bee00d)
be deduced to
![{\displaystyle \phi [y:=s\left(s\left(s\left(0\right)\right)\right)]}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/943e474138e904fcaa5c5e36f21a61ee964d0eaf)
- For all
, ![{\displaystyle \emptyset \vdash t{\hat {=}}t}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/bb80aaf87765f3898be25c23043c7c7c43cefd64)
Now, let us use this scheme of logical axioms:
![{\displaystyle \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\}}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/b2f2b24226c38b84299b843f236a82fcde123451)
- deduction theorem as a lemma (the latter can be proved from Hilbert system, too)
and thus we can deduce
![{\displaystyle \left\{s{\hat {=}}t,\phi [z:=s]\right\}\vdash \phi [z:=t]}](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/ffa181e56b187f8bb4f48e0ff4ed0adb93c2bc8e)
for all
,
,
.
See detailed proof in p. 136–137 of [1].
We are almost ready. We have to use the following lemme yet:
- For all
, if
, then ![{\displaystyle \left\{\phi {\hat {\land }}\psi \right\}\vdash \xi }](https://wikimedia.riteme.site/api/rest_v1/media/math/render/svg/47bc5e68b69d3b8b5b5938f30945c6e5e1c952a8)
Proof can be figured by solving the exercises in p. 137 of [1].
- ^ a b Ruzsa, Imre: Bevezetés a modern logikába. Osiris Kiadó, Budapest, 1997.