Die Elementrelation und mengentheoretische Gleichheit
Wir definieren mit Hilfe von Rekursion eine Vergröberung der Iota-Relation x ι y und der Iota-Gleichheit =ι .
Definition (x ∈ y, x = ∈ y, Element, mengentheoretisch gleich)
Wir definieren für alle x, y rekursiv:
| x ∈ y, | falls ∃z ι y x = ∈ z. |
| x = ∈ y, | falls ∀z ι x z ∈ y ∧ ∀z ι y z ∈ x. |
Gilt x ∈ y, so sagen wir auch: x ist ein Element von y.
Gilt x = ∈ y, so nennen wir x und y mengentheoretisch gleich oder ∈ -gleich.
Zur Definition von ∈ und = ∈ für x, y benutzen wir, dass die beiden Relationen für alle a, y mit a ι x und alle x, b mit b ι y bereits definiert sind. Diese Rekursion lässt sich als Rekursion der Form G(x, y) = F(〈 x, y 〉, G ∘ chop(Tr*(x) × Tr*(y))) auffassen, etwa mit G(x, y) = 1 für „x ∈ y“ und G(x, y) = 2 für „x = ∈ y“.
Wie üblich sind x ⊆ ∈ y, x = ∈ { x, y }, usw. definiert.
Wir untersuchen nun die ∈ -Relation und ∈ -Gleichheit genauer. Zuerst zeigen wir, dass sie die ι-Versionen vergröbern:
Satz (Epsilon vergröbert Iota)
Für alle x, y gilt:
| (i) | x ι y | impliziert x ∈ y. |
| (ii) | x =ι y | impliziert x = ∈ y. |
Beweis
Wir zeigen die Aussagen simultan durch Induktion.
zu (i):
Es gelte x ι y. Wir zeigen x ∈ y. Zu zeigen ist:
(+) ∃z ι y x = ∈ z.
Aber x =ι x, also x = ∈ x nach I.V. (ii) für x, x.
Also ist x ein z wie in (+).
zu (ii):
Es gelte x =ι y. Wir zeigen x = ∈ y. Zu zeigen ist:
(++) ∀z ι x z ∈ y ∧ ∀z ι y z ∈ x.
Sei also z ι x. Dann gilt z ι y wegen x =ι y.
Dann gilt aber z ∈ y nach I.V. (i) für z, y.
Analog folgt aus z ι y, dass z ∈ x.
Andererseits gilt etwa 〈 〈 0, 1 〉 〉 = ∈ 〈 〈 1, 0 〉 〉 aber non(〈 〈 0, 1 〉 〉 =ι 〈 〈 1, 0 〉 〉). Also ist die Vergröberung echt. Auflösung der rekursiven Definition zum Nachweis von 〈 〈 0, 1 〉 〉 = ∈ 〈 〈 1, 0 〉 〉 führt z.B. über den Zwischenschritt 〈 0, 1 〉 = ∈ 〈 1, 0 〉. Dieser folgt aus 〈 0, 1 〉 =ι 〈 1, 0 〉 mit Hilfe des Satzes bzw. durch weitere Auflösung der rekursiven Definition von = ∈ . Die volle Auflösung der rekursiven Definitionen wird rechnerisch auch für erblich endliche Listen schnell sehr aufwendig.
Aus dem Satz erhalten wir wegen x =ι x unmittelbar:
Korollar (Reflexivität der ∈ -Gleichheit)
Es gilt x = ∈ x für alle x.
Die ∈ -Gleichheit ist offenbar symmetrisch. Die Transitivität zeigen wir innerhalb eines umfassenderen Kongruenzsatzes.
Satz (Kongruenzsatz)
Für alle x, y, z gilt:
| (i) | x = ∈ y und y = ∈ z | impliziert x = ∈ z. |
| (ii) | x = ∈ y und y ∈ z | impliziert x ∈ z. |
| (iii) | x = ∈ y und z ∈ y | impliziert z ∈ x. |
Beweis
Wir zeigen die Aussagen simultan durch Induktion.
zu (i):
Es gelte x = ∈ y und y = ∈ z. Zu zeigen ist:
(+) ∀a ι x a ∈ z ∧ ∀a ι z a ∈ x.
Sei also a ι x. Dann ist a ∈ y wegen x = ∈ y.
Wegen z = ∈ y gilt dann aber auch a ∈ z nach I.V. (iii) für z, y, a.
Völlig analog folgt aus a ι z, dass a ∈ x.
zu (ii):
Gelte x = ∈ y und y ∈ z. Zu zeigen ist:
(+) ∃x′ ι z x′ = ∈ x.
Wegen y ∈ z existiert aber ein x′ ι z mit y = ∈ x′.
Dann gilt x = ∈ y und y = ∈ x′, also x = ∈ x′ nach I.V. (i) für x, y, x′.
Also ist x′ wie gewünscht.
zu (iii):
Gelte x = ∈ y und z ∈ y. Zu zeigen ist:
(+) ∃z′ ι x z′ = ∈ z.
Wegen z ∈ y existiert ein z ι y mit z = ∈ z.
Wegen x = ∈ y und z ι y existiert ein z′ ι x mit z′ = ∈ z.
Dann gilt z′ = ∈ z und z = ∈ z. Also ist z′ = ∈ z nach I.V. (i) für z′, z, z.
Also ist z′ wie gewünscht.
Korollar
Sei φ(z1, …, zn) eine Formel der Listentheorie, die aus Formeln des Typs „x = ∈ y“ und „x ∈ y“ mit Hilfe der Junktoren und Quantoren aufgebaut ist.
Weiter seien z1, …, zn Listen mit φ(z1, …, zn).
Dann gilt φ(z1, …, zn) für alle z1, …, zn mit zi = ∈ zi für 1 ≤ i ≤ n.
Beweis
Induktion über den Aufbau von φ.
Mit Hilfe des Kongruenzsatzes können wir nun folgende Verstärkung der Iota-Regularität beweisen:
Satz (Epsilon-Regularität)
Für alle x ≠ 〈 〉 existiert ein α < x derart, dass x(α) ∈ -minimal in x ist, d. h. es gibt kein β < x mit x(β) ∈ x(α).
Beweis
Sei x ≠ 〈 〉. Wir definieren rekursiv solange möglich für ν < ω:
z(0) = s(0) = 0,
z(ν + 1) = „das kleinste β < x mit x(β) ∈ x(z(ν))“,
s(ν + 1) = „das kleinste γ < x[ s|(ν + 1) ] mit: x(z(ν + 1)) = ∈ x[ s|(ν + 1) + 〈 γ 〉 ]“.
[ Nach I.V. gilt x(z(ν)) = ∈ x[ s|(ν + 1) ]. Wegen x(z(ν + 1)) ∈ x(z(ν)) existiert also ein solches γ nach dem Kongruenzsatz. Es gilt dann x(z(ν + 1)) = ∈ x[ s|(ν + 2) ].]
Dann ist s|ν anwendbar auf x für alle ν, also bricht die Rekursion an einer Stelle ν* < ω bei der Defintion von z(ν* + 1) ab, d. h. typ(z) = ν* + 1.
Nach Konstruktion ist dann x(z(ν*)) ∈ -minimal in x.
Insbesondere gilt x ∉ x für alle Listen x.
Wir definieren schließlich:
Definition ( ∈ -injektiv, delrep ∈ (x))
x heißt ∈ -injektiv, falls für alle α < β < x gilt, dass x(α) ≠ ∈ x(β).
Wir setzen weiter:
delrep ∈ (x) = sieve(x, „z* ∉ y* “).