Jump to content

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

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Axioms we use

[edit]

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

Term identity lemma

[edit]
For all ,

Main lemma

[edit]

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

Conjunction lemma

[edit]

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

Notes

[edit]
  1. ^ a b Ruzsa, Imre: Bevezetés a modern logikába. Osiris Kiadó, Budapest, 1997.