Tupel/Formale Definition

aus GlossarWiki, der Glossar-Datenbank der Fachhochschule Augsburg
Wechseln zu:Navigation, Suche

Dieser Artikel erfüllt die GlossarWiki-Qualitätsanforderungen nur teilweise:

Korrektheit: 3
(zu größeren Teilen überprüft)
Umfang: 4
(unwichtige Fakten fehlen)
Quellenangaben: 5
(vollständig vorhanden)
Quellenarten: 5
(ausgezeichnet)
Konformität: 5
(ausgezeichnet)

Eine informelle Definition des Begriffs Tupel wurde im zugehörigen Artikel angegeben. Dort findet man auch einen Überblck über die zugehörige Geschichte einschließlich unterschiedlicher Definitionen. Im Folgenden wird der tupelbegriff auf Basis dieser Definitionen formalisiert. Dabei wird vorausgesetzt, dass der Term „geordnetes Paar[math][x,y][/math] schon definiert oder axiomatisch eingeführt wurde.

Man beachte, dass sich das geordnete Paar [math][x,y][/math] vom Tupel [math](x,y)[/math] (in Listennotation) unterscheidet, sofern Letzteres mit Hilfe von [math][x,y][/math] definiert wird. Allerdings erfüllt [math](x,y)[/math] (nachdem es definiert wurde) ebenfalls das Paaraxiom und kann überall, wo ein geordnetes Paar benötigt wird, genauso gut wie [math][x,y][/math] verwendet werden. In LISP sieht man den Unterschied sehr schön: Die „Cons-Zelle“ (x . y) unterscheidet sich von der Liste (x y), die als Abkürzung für (x . (y . NIL)) steht. Beide Definitionen erfüllen jedoch das Paaraxiom.

1 Definition (Kowarschick)

1.1 Attributtupel, Familie (in Anlehnung an Bourbaki[1] und Schmidt[2])

Es sei [math]t: I \rightarrow \mathcal{V}[/math] eine beliebige Funktion von einer Menge oder Klasse [math]I[/math] in die Allklasse [math]\mathcal{V}[/math]:

$t \subseteq I \times \mathcal{V} \,\wedge\, \bigwedge x, y_1, y_2: [x,y_1] \in f \wedge [x,y_2] \in f \rightarrow y_1=y_2$

[math]t[/math] wird nicht nur Funktion genannt, sondern, insbesondere wenn man sich mehr für den Definitionsbereich als für die Funktion selbst interessiert, auch (Attribut-)Tupel oder Familie über [math]I[/math]. Alternativ kann man auch [math]I[/math]-Tupel oder [math]I[/math]-Familie sagen.

[math]\rm{TupA}(t) :\leftrightarrow \rm{Fkt}(t)[/math] (siehe Funktion)

1.1.1 Indexbereich und Indexmenge

Die Definitionsmenge [math]I := I(t) = \rm{Def}(f) := \{x| \bigvee y: [x,y] \in t\}[/math] der Funktion [math]t[/math] heißt in diesem Fall Indexbereich. Falls es sich bei [math]I[/math] um eine echte Menge und nicht um eine Unmenge handelt, kann man auch Indexmenge sagen.

1.1.2 Tupellänge (Attributtupel)

Die Mächtigkeit des Indexbereichs heißt Länge des Tupels:

[math]\rm{lg}(t) := |I(t)|[/math]

Ein Tupel der Länge [math]l[/math] wird auch [math]l[/math]-Tupel genannt.

1.1.3 Schlüssel und Wert (Attributtupel)

Jedes Element [math]i[/math] des Indexbereichs heißt Schlüssel oder Index.

Das zum Index [math]i[/math] gehörende Element [math]t_i := t(i)[/math] wird als Wert bezeichnet.

1.1.4 Anmerkungen (Attributtupel)

Mit [math]\rm{Fkt}(f)[/math] wird ausgedrückt, dass es sich bei einer Menge oder Klasse [math]f[/math] um eine Funktion handelt, dass [math]f[/math] also eine Menge oder Klasse von geordneten Paaren ist, die die Eindeutigkeitsbedingung

$\bigwedge x, y_1, y_2: [x,y_1] \in f \wedge [x,y_2] \in f \rightarrow y_1=y_2$

erfüllt.

Mit [math]\rm{TupA}(t)[/math] wird ausgedrückt, dass es sich bei [math]t[/math] um ein Attributtupel handelt.

Schmidt verwendet die Bezeichnung „Glied“ an Stelle von „Wert“.

Der Begriff „I-Tupel“ geht auf Ebbinghaus[3] zurück.

1.2 Positionstupel (in Anlehnung an McCarthy et al.[4])

Der Begriff des geordneten Paars kann induktiv für eine beliebige endliche Anzahl von Elementen verallgemeinert werden:

Eine Menge oder Klasse [math]t[/math] heißt (Positions-)Tupel – in Zeichen [math]\rm{TupV}(t)[/math] – wenn entweder [math]t=\emptyset[/math] gilt oder wenn [math]t[/math] ein geordnetes Paar [math][x,t][/math] ist, dessen erstes Element beliebig und dessen zweites Element ein Tupel ist:

[math]\rm{TupV}(\emptyset)[/math]
[math]\bigwedge x, t: \rm{TupV}(t) \rightarrow \rm{TupV}([x,t])[/math]

Andere Positionstupel gibt es nicht. Das heißt, für jedes Tupel [math]t \not= \emptyset[/math] gibt es ein Element [math]x[/math]
und ein Tupel [math]t'[/math] mit [math]t = [x,t'][/math]:

[math]\bigwedge t: (\rm{TupV}(t) \wedge t \not= \emptyset \rightarrow \bigvee x, t': (\rm{TupV}(t') \wedge t = [x,t']))[/math]

Das Tupel [math]t'[/math] ist wegen des Paaraxioms sogar eindeutig bestimmt:

[math]\bigwedge t: (\rm{TupV}(t) \;\rightarrow\; \bigwedge x_1, x_2, t_1, t_2: (\rm{TupV}(t_1) \wedge \rm{TupV}(t_2) \wedge t = [x_1,t_1] \wedge t = [x_2,t_2] \,\rightarrow\, t_1=t_2 \wedge x_1=x_2))[/math]

In einem klassenbasierten Axiomen-System (wie es z.B. der Neumann-Bernays-Gödel-Mengenlehre zu Grunde liegt) ist diese Formel allerdings nur im Falle von Klassenpaaren gültig (vgl. Abschnitt „Reihenfolge der Elemente“ im Artikel geordnetes Paar). Für Mengenpaare müsste sie entsprechend auf Mengen eingeschränkt werden, da Mengenpaare keine Klassen enthalten können:

[math]\bigwedge a,b: (\rm{UMg}(a) \vee \rm{UMg}(b)) \leftrightarrow (a,b) = \mathcal{V}[/math]

In diesem Fall gilt nur:

[math]\bigwedge t: (\rm{Mg}(t) \wedge \rm{TupV}(t) \;\rightarrow\; \bigwedge x_1, x_2, t_1, t_2: (\rm{TupV}(t_1) \wedge \rm{TupV}(t_2) \wedge t = [x_1,t_1] \wedge t = [x_2,t_2] \,\rightarrow\, t_1=t_2 \wedge x_1=x_2 \wedge \rm{Mg}(x_1) \wedge \rm{Mg}(x_2) \wedge \rm{Mg}(t_1) \wedge \rm{Mg}(t_2) ))[/math]

1.2.1 Tupellänge (Positionstupel)

Es sei [math]t[/math] ein Positionstupel: [math]TupV(t)[/math]. Die Länge [math]\rm{lg}(t)[/math] von [math]t[/math] wird ebenfalls induktiv definiert:

[math]\rm{lg}(\emptyset) := 0[/math]
[math]\bigwedge x, t: \rm{TupV}(t) \rightarrow \rm{lg}([x,t]) := \rm{lg}(t)+1[/math]

Ein Tupel der Länge [math]l[/math] heißt [math]l[/math]-Positionstupel.

Das 0-Tupel wird auch leeres Tupel genannt.

1.2.1.1 Lemma: Eindeutigkeit der Länge eines Positionstupels

Die Länge eines Positionstupels ist eindeutig bestimmt.

Beweis

Das leere Tupel ist das einzige Tupel der Länge [math]0[/math]. Für jedes andere Tupel [math]t[/math] existiert genau ein Element [math]x[/math] und ein Tupel [math]t'[/math], für die [math]t=[x,t'][/math] gilt. Für [math]t'[/math] ist die Länge laut Induktionsvoraussetzung eindeutig bestimmt und damit ist die Länge [math]\rm{lg}(t) = \rm{lg}(t')+1[/math] ebenfalls eindeutig bestimmt.

1.2.2 Indexbereich (Positionstupel)

Für ein Positionstupels [math]t[/math] wird die Indexbereich [math]I(t)[/math] folgendermaßen definiert :

[math]I(t) := \{i \in \mathbb{N}: 0 \lt i \le \rm{lg}(t)\}[/math]

Anmerkung
Die Zählung der Attribute beginnt laut dieser Definition bei [math]1[/math] und endet bei [math]\rm{lg}(t)[/math]. Man könnte ohne Probleme auch die in der Informatik übliche Zählung von [math]0[/math] bis[math]\rm{lg}(t)-1[/math] verwenden, müsste dann aber ein paar Anpassungen vornehmen (z. B. beim nachfolgenden Lemma).

1.2.2.1 Lemma: Länge des Tupels

Die Länge eines Positionstupels [math]t[/math] ist gleich der Mächtigkeit des Indexbereichs: [math]\rm{lg}(t) = |I(t)|[/math]

Beweis

[math]|I(t)| = |\{i \in \mathbb{N}: 0 \lt i \le \rm{lg}(t)\}| = \rm{lg}(t)[/math]

1.2.3 Schlüssel und Wert (Positionstupel)

Es seien [math]t[/math] ein nicht-leeres Positionstupel und [math]I := I(t)[/math] der zugehörige Indexbereich. Die Elemente [math]i\in I[/math] des Indexbereichs heißen Schlüssel.

Jedem Schlüssel [math]i\in I[/math] wird durch das Tupel [math]t[/math] ein eindeutiger Wert [math]t_i[/math] zugeordnet. [math]t_i[/math] wird wieder induktiv definiert:

Da laut Voraussetzung [math]t \not= \emptyset[/math] gilt, gibt es zwei (eindeutige) Elemente [math]x[/math] und [math]t'[/math] mit [math]\rm{TupV}(t')[/math] und [math]t=[x,t'][/math].

[math]t_i := \begin{cases} x & \mbox{wenn } i = 1\\ t'_{i-1} & \mbox{wenn } i \gt 1 \end{cases} [/math]

Man beachte, dass aus [math]i\in I[/math] stets [math]0 \lt i \lt \rm{lg}(t)[/math] folgt. Diese Invariante bleibt im rekursiven Zweig der Definition erhalten: [math]i\gt 1 \rightarrow 0 \lt i-1 \lt \rm{lg}(t)-1 = \rm{lg}(t')[/math]. Das heißt, es gilt auch hier [math]i-1 \in I(t')[/math].

Für [math]i\notin I[/math] ist [math]t_i[/math] nicht definiert. Man kann in diesem Fall allerdings [math]t_i := \mathcal{V}[/math] setzen, um [math]t_i[/math] für jede beliebige Klasse [math]i[/math] zu definieren.

1.2.4 Listennotation

Für Positionstupel wird folgende abkürzende Schreibweise eingeführt:

[math]() := \emptyset[/math]
[math](x_1) := [\emptyset, x_1][/math]
[math](x_1,x_2) := [[\emptyset, x_1], x_2][/math]
[math](x_1,x_2,x_3) := [[[\emptyset, x_1], x_2], x_3][/math]

Allgemein für [math]n \ge 2[/math]:

[math](x_1,\ldots,x_n) := [(x_1,\ldots,x_{n-1}), x_n] = [[[\ldots[\emptyset,x_1]\ldots], x_{n-1}], x_n][/math]

1.2.5 Anmerkungen (Positionstupel)

1.2.5.1 Ursprung und Varianten der Listennotation

Die obige Definition der Listennotation geht auf McCarthy zurück (wobei er die Liste allerdings vom letzten Element ausgehend aufbaut):

The list [math](m_1,m_2,···,m_n)[/math] is represented by the S-expression [math](m_1·(m_2·(···(m_n·\rm{NIL})···)))[/math].
Here [math]\rm{NIL}[/math] is an atomic symbol used to terminate lists.[5]

McCarthy definiert eine LISP-Liste als abkürzende Schreibweise für eine Folge von [math]cons[/math]-Zellen, d.h. als Folge von LISP-Paaren [math](a \cdot b)[/math]. In LISP wird eine Liste also als verkette Liste implementiert: Jede [math]cons[/math]-Zelle enthält das eigentlich Listenelement sowie einen Verweis auf die Nachfolgerliste. Die letzte [math]cons[/math]-Zelle enthält keinen Verweis, sondern die LISP-Konstante [math]\rm{NIL}[/math].

In seinen ursprünglichen Publikationen wie auch im Benutzerhandbuch von LISP I[6] bezeichnet McCarthy [math]\rm{NIL}[/math] lediglich als „atomares Symbol“, welches benutzt wird, um Listen zu terminieren. Erst im Beutzerhandbuch von LISP 1.5[4] legt er zusätzlich fest, dass [math]\rm{NIL}[/math] identisch zur leeren Liste [math]()[/math] ist.

Die Definition von McCarthy ist den Definitionen von anderen Autoren, wie z.B. Gödel oder Schmidt, vorzuziehen.

Definition von Schmidt[2] (und diversen anderen Autoren):

[math](x_1, x_2)[/math] ist ein (Klassen-)Paar.
[math](x1, x2, x3) := ((x1, x2), x3)[/math] ist ein (Klassen-)Tripel.
[math](x1, x2, x3, x4) := ((x1, x2, x3), x4) = (((x1, x2), x3), x4)[/math] ist ein (Klassen-)Quadrupel.

Diese Definition hat zwei Nachteile:

  • Es gibt kein 0- und keine 1-Tupel.
  • Tupel unterschiedlicher Länge können gleich sein (jedes n-Tupel für n>2 ist gleichzeitig auch ein 2-Tupel; ein Beweis einer Aussage analog zu Lemma 4.2.1.1 scheitert daher beim Induktionsanfang).

Definition von Gödel[7] (und diversen anderen Autoren):

Gödel hat Tupel im Prinzip genauso wie Schmidt definiert. Zusätzlich hat er allerdings noch 1-Tupel eingeführt:

[math](x_1) := x_1[/math]

Doch auch diese zusätzliche Festlegung löst die obigen Probleme nicht wirklich.

1.2.5.2 Mengentupel und Klassentupel (Positionstupel)

In einer klassenbasierten Mengenlehre erhält man mit Hilfe der obigen Definition so genannte Klassentupel, sofern man der Definition der Tupel Klassenpaare zugrunde legt. Bei Benutzung einer mengenbasierten Mengenlehre oder wenn man Tupel mit Hilfe von Mengenpaaren definiert, erhält man dagegen lediglich so genannte Mengentupel.

Ein Klassentupel kann nicht nur Mengen, sondern auch Unmengen als Elemente beinhalten.

Beispielsweise kann man das Monoid der Ordinalzahlen [math]\Omega[/math] mit Addition [math]+[/math] und neutralem Element [math]0[/math] als Klassentupel [math](\Omega,+,0)[/math] definieren, obwohl es sich bei [math]\Omega[/math] um eine Unmenge handelt. Für Mengentupel gilt dagegen, dass [math](\Omega,+,0)[/math] entweder nicht definiert ist oder gleich der Allklasse [math]\mathcal{V}[/math] ist. Im letzteren Fall sind alle Mengentupel, die ein oder mehrere Unmengen enthalten, ebenfalls gleich [math]\mathcal{V}[/math].

Objektsprache und Metasprache
Man beachte auch, dass hinsichtlich der Definitionen und Beweise ein wesentlicher Unterschied zwischen Mengen- und Klassentupeln besteht.

Für Mengen kann [math]TupV[/math] als echte Funktion definiert werden. Die zugehörigen, auf vollständiger Induktion basierenden Beweise können daher innerhalb der formalen Sprache (Objektsprache) des jeweiligen Axiomensystems der Mengenlehre (unter Zuhilfenahme des Unendlichkeitaxioms) durchgeführt werden. In einem ersten Schritt formalisiert man innerhalb der Mengenlehre die natürlich Zahlen (samt vollständiger Induktion) und in einem zweiten Schritt wendet man diesen Formalismus bei den Beweisen der obigen Aussagen an.

Für Klassen kann [math]TupV[/math] dagegen nicht als echte Funktion, sondern nur als Abkürzung, definiert werden, da eine Unmenge niemals in einer Funktion als Urbild oder Bildelement auftauchen kann. Es gilt nämlich

$\rm{UMg}(a) \rightarrow \{a\}= \mathcal{V}$ (Schmidt (1966), S. 73)

und damit auch

$\rm{UMg}(a) \vee \rm{UMg}(b) \rightarrow \rm{UMg}((a,b))$ (Schmidt (1966), S. 97)
$\rightarrow \{\ldots,(a,b),\ldots\}= \mathcal{V} $

Das heißt, sobald man versucht, eine Unmenge in die Definition einer Funktion [math]f[/math] als Urbild oder Bildelement einzuschleusen, degeneriert [math]f[/math] zur Allklasse.

[math]TupV(t)[/math] ist also im Falle von Klassentupeln eine Abkürzung für eine mengentheoretische Formel, genauso wie [math]Mg(m)[/math], als Abkürzung für die Formel [math]\bigvee a: m \in a[/math] steht (siehe Klasse). Die zugehörigen Induktionsbeweise müssen in diesem Fall außerhalb des Axiomensystems der Mengenlehre auf geführt werden, also beispielsweise mit Hilfe der Metasprache, die zur Definition des formalen System verwendet wurde. Man beachte, dass die obigen Beweise genaugenommen sogar innerhalb der Metametasprache „Deutsch“ geführt wurden.

Das Problem ist, dass man, obwohl man eine Arithmetik der natürlichen Zahlen formal mit Hilfe der Mengenlehre-Axiome – d.h. innerhalb der Objektsprache – definieren kann, dennoch eine Arithmetik außerhalb – d.h. innerhalb der Metasprache – des Systems braucht, um das formale System überhaupt definieren zu können. Metamathematische Induktionsbeweise beruhen auf „gesundem Menschenverstand“. Im Prinzip definiert man ein Beweisschema, aus dem man für jeden konkreten Einzelfall einen formalen Beweis ableiten kann. Dies war schon Gödel bekannt:

... einziger Zweck dieser allgemeinen metamathematischen Überlegungen ist es zu zeigen, wie die Beweise für Sätze von einem gewissen Typus nach einer allgemeinen Methode ausgeführt werden können; ... diese allgemeinen metamathematischen Überlegungen könnten ganz wegbleiben, wenn man sich die Mühe nähme, die Beweise in jedem Fall einzeln durchzuführen ...[8]

1.3 Abbildung der Listen- auf die Attributnotation

Für jedes [math]n[/math]-Tupel [math]t[/math] ([math]n \in \mathbb N[/math]) in Listennotation kann ein zugehöriges Tupel [math]t'[/math] in Attributnotation definiert werden, sofern es sich bei [math]t[/math] um ein „Mengentupel“ handelt, d. h., sofern das Tupel nur Mengen aber keine Unmengen enthält, d.h., sofern [math]\rm{Mg}(t_i)[/math] für alle [math]i \in I(t)[/math]:

[math]t' := \{[i,t_i]: i \in I(t)\}[/math]

Anmerkung:
Diese Aussage kann mit ziemlicher Sicherheit für beliebige Ordinalzahlen verallgemeinert werden. Dazu müssen die Positionstupel mittels transfiniter Induktion an Stelle der natürlichen Induktion definiert werden, und für alle Aussagen, die zuvor induktiv bewiesen wurden oder die im Folgenden noch induktiv beweisen werden, muss ebenfalls die transfinite Induktion verwendet werden.

1.3.1 Lemma: Korrektheit der Abbildung der Listen- auf die Attributnotation

[math]t[/math] und [math]t'[/math] beschreiben dasselbe Tupel:

  1. [math]I(t) = I(t') = \{i \in \mathbb{N}: 0 \lt i \le \rm{lg}(t)\}[/math]
  2. [math]\rm{lg}(t) = \rm{lg}(t')[/math]
  3. [math]\bigwedge i \in I: t_i = t'_i[/math], wobei [math]I := I(t) = I(t')[/math]

Beweis

$I(t') = \{x: \bigvee y: [x,y] \in t'\}$ (Definition von [math]I(t')[/math])
$I(t') = \{x: \bigvee y: [x,y] \in \{[i,t_i]: i \in I(t)\} \}$ (Definition von [math]t'[/math])

Man kann die erste Aussage

$I(t') = I(t)$

beweisen, indem man

$I(t') \subseteq I(t)$ (*1)
$I(t') \supseteq I(t)$ (*2)

nachweist. ([math]I(t) = \{i \in \mathbb{N}: 0 \lt i \le \rm{lg}(t)\}[/math] ist bereits laut Definition von [math]I(t)[/math] richtig.)

Begründung für *1
Es sei [math]x \in I(t')[/math], d.h., es gibt ein [math]y[/math] mit [math][x,y] \in \{[i,t_i]: i \in I(t)\}[/math], d.h., es gibt ein [math]i \in I(t)[/math] mit [math][x,y] = [i,t_i][/math] und damit gilt [math]x = i \in I(t)[/math], wegen des Paaraxioms.

Begründung für *2
Es sei [math]i \in I(t)[/math]. Wenn man [math][x,y] := [i, t_i][/math] setzt, ist [math][x,y] \in \{[i,t_i]: i \in I(t)\}[/math]. Und damit ist [math]i \in I(t')[/math].

Die zweite Aussage folgt direkt aus der ersten Aussage, der Definition von [math]\rm{lg}(t')[/math] und Lemma 4.2.2.1:

[math]\rm{lg}(t) = |I(t)| = |I(t')| =: \rm{lg}(t')[/math]

Die dritte Behauptung folgt direkt aus der ersten Aussage und der Definition von [math]t'_i[/math] und [math]t'[/math]:

Es sei [math]i \in I[/math], dann ist [math]t'_i = t'(i) = t_i[/math]

1.3.2 Anmerkungen

Ein geordnetes Paar [math][a,b][/math] kann, wie bereits definiert wurde, als 2-Tupel aufgefasst werden.

Allerdings liefert die allgemeine Tupeldefinition, die i.Allg. auf dem geordneten Paar basiert, ihrerseits ein 2-Tupel, das heißt, ein geordnetes Paar: [math](a,b)[/math]. Da dieses Paar ebenfalls das Paaraxiom erfüllt, wird das spezielle geordnete Paar [math][a,b][/math] künftig nicht mehr benötigt. Es wird durch [math](a,b)[/math] ersetzt.

2 Gleichheit zweier Tupel

Die Gleichheit von Tupel wird – unabhängig von der Art der Definition – auf die Gleichheit von Klassen zurückgeführt:

Zwei Tupel [math]t_1[/math] und [math]t_2[/math] sind genau dann gleich, wenn [math]t_1[/math] und [math]t_2[/math] als Klassen gleich sind, d.h., wenn:

[math]t_1 \subseteq t_2 \wedge t_2 \subseteq t_1[/math]

oder, anders formuliert:

[math]\bigwedge x \in \mathcal{V}: x \in t_1 \Leftrightarrow x \in t_2[/math]

2.1 Lemma

Zwei gleiche Tupel (in Attribut- oder Listennotation) sind trivialerweise gleich lang :

[math]t_1 = t_2 \Rightarrow \text{lg}(t_1) = \text{lg}(t_2)[/math]

Beweis
Die Behauptung folgt direkt aus der Reflexivität der Gleichheit ([math]\text{lg}(t_1) = \text{lg}(t_1)[/math]) und der Leibnizschen Ersetzbarkeit.

2.2 Satz

Es seien [math]t_1[/math] und [math]t_2[/math] zwei Tupel (in Attribut- oder Listennotation).

[math]t_1[/math] und [math]t_2[/math] sind genau dann gleich, wenn die zugehörigen Indexbereiche [math]I(t_1)[/math] und [math]I(t_2)[/math] übereinstimmen und wenn die Funktionswerte für jedes Element des Indexbereichs ebenfalls übereinstimmen:

[math]t_1 = t_2 \Leftrightarrow I(t_1) = I(t_2) \wedge \bigwedge i \in I(t_1): t_1(i) = t_2(i)[/math]

Die Behauptung [math]\Rightarrow[/math] folgt wieder direkt aus der Reflexivität der Gleichheit und der Leibnizschen Ersetzbarkeit.

Beweis für Attributnotation: siehe Schmidt (1966), S. 123, Aussagen 14.10 und 14.11

Beweis für Listennotation: mittels vollständiger Induktion.
Es sei [math]I := I(t_1) = I(t_2)[/math].

Induktionsanfang: [math]I = \emptyset[/math]
Dann ist [math]\rm{lg}(t_1) = \rm{lg}(t_2) = 0[/math] und damit [math]t_1 = t_2 = \emptyset[/math].

Induktionsvoraussetzung:
Es seien [math]t_1 = t_2[/math], [math]I(t_1) = I(t_2)[/math], [math]n := \rm{lg}(I(t_1)) = \rm{lg}(I(t_2))[/math] und [math]I' := I \cup \{n+1\} = \{\mathbb{N}: 0 \lt i \le n+1\}[/math]. Dann ist [math]|I'| = n+1[/math].

Induktionsschritt:
Es seien überdies [math]t'_1 = [x_1, t_1][/math] und [math]t'_2 = [x_2, t_2][/math] (n+1 > 0!). Da laut Voraussetzung (rechte Seite von [math]\Leftrightarrow[/math]) [math]x_1 = t'_1(n+1) = t'_2(n+1) = x_2[/math] und laut Induktionsvoraussetzung [math]t_1 = t_2[/math], gilt wegen des Paaraxioms auch [math]t'_1 = t'_2[/math], was zu beweisen war.

3 Quellen

  1. Bourbaki (1939): Nicolas Bourbaki; Théorie des ensembles; Verlag: Hermann; Adresse: Paris; 1939; Quellengüte: 5 (Buch), S. E III.45
  2. 2,0 2,1 Schmidt (1966): Jürgen Schmidt; Mengenlehre – Grundbegriffe; Reihe: B.I.Hochschultaschenbücher; Band: 1; Nummer: 56; Verlag: Bibliographisches Institut AG; Adresse: Mannheim; ISBN: B0000BUJC6; 1966; Quellengüte: 5 (Buch), S. 122
  3. Ebbinghaus (2003): Heinz-Dieter Ebbinghaus; Einführung in die Mengenlehre; Reihe: Hochschultaschenbuch; Auflage: 4; Verlag: Spektrum Akademischer Verlag; Adresse: Heidelberg, Berlin; ISBN: 3-8274-1411-3; 2003; Quellengüte: 5 (Buch), S. 59–60
  4. 4,0 4,1 McCarthy et. al. (1965): John McCarthy, Paul W. Abrahams, Daniel J. Edwards, Timothy P. Hart und Michael I. Levin; LISP 1.5 Programmer's Manual; Verlag: The MIT Press; Adresse: Cambridge, Massachusetts; Web-Link; 1965 (Buch)
  5. McCarthy (1960): John McCarthy; Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I; in: Communications of the ACM; Band: 3; Nummer: 4; Seite(n): 184-195; Verlag: Association for Computing Machinery; Adresse: New York; Web-Link 0, Web-Link 1; 1960; Quellengüte: 5 (Artikel)
  6. McCarthy et. al. (1960): John McCarthy, R. Brayton, Daniel J. Edwards, P. Fox, L. Hodes, D. Luckham, K. Maling, D. Park und S. Russell; LISP I Programmer's Manual; Hochschule: Massachusetts Institute of Technology; Adresse: Cambridge, Massachusetts; Web-Link; 1960; Quellengüte: 5 (Technischer Bericht), S. 11
  7. Gödel (1940): Kurt Gödel; The Consistency of the Continuum Hypothesis; Verlag: Princeton University Press; ISBN: 0-691-07927-7; Web-Link; 1940; Quellengüte: 5 (Buch)
  8. zitiert nach Schmidt (1966), S. 174