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:
Let us work on a concrete example:
Can
be deduced to
- For all ,
Now, let us use this scheme of logical axioms:
- deduction theorem as a lemma (the latter can be proved from Hilbert system, too)
and thus we can deduce
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
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.