© 1999 François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.


3.6 Gleichheit

Wir haben in Kapitel 2 ein spezielles zweistelliges Gleichheitsrelationssymbol eingeführt. Wie kann man aber erreichen, dass dieses Relationssymbol gerade mit der Gleichheitsrelation und nicht mit einer anderen zweistelligen Relation auf dem Universum interpretiert wird?

Die Eigenschaften eines Relationssymbols werden normalerweise dadurch festgelegt, dass man sie mittels Formeln axiomatisiert. Die Interpretationen, die Modelle dieser Axiome sind, ordnen dem Relationssymbol dann eine Relation mit den axiomatisierten Eigenschaften zu. Im Falle der Gleichheit ist diese Vorgehensweise aber aus den folgenden Gründen unzufriedenstellend:

  1. Man kann mit Formeln der PL1S nicht ausschließen, dass Modelle dieser Formeln zwei verschiedene Elemente des Universums als ,,gleich`` interpretieren.
  2. Der Begriff Gleichheit ist in sehr vielen Anwendungen der PL1S zu finden. Die Gleichheit hat also eine besondere Stellung, die eine besondere Behandlung rechtfertigt.
Der folgende Satz liefert die Begründung für die erste Aussage:

Satz 3.6.1 (Modellerweiterungssatz).   Sei M=(D,Ab,U) eine -Interpretation, sei d'∉D und D'=D∨{d'}. Dann gibt es eine -Interpretation M' mit Universum D', so dass für jede -Formel F gilt gdw. .

Beweis:

Sei d ∈ D beliebig, aber fest gewählt. Wir konstruieren Ab' aus Ab, so dass auch das neue Element d' berücksichtigt wird. Die Grundidee dabei ist, d' als eine Art ,,unscheinbaren Zwilling`` von d zu behandeln: ,,Zwilling``, weil d' als Argument von Funktionen und Relationen genauso wirkt als stünde d an seiner Stelle; ,,unscheinbar``, weil die den Funktionssymbolen zugeordneten Funktionen d' nie als Ergebnis liefern.

Notation: für ein Tupel (d1,...,dn) von Elementen von D' bezeichne (d1,...,dn)[d/d'] das Tupel von Elementen von D, das aus dem ersten entsteht, wenn jedes Vorkommen von d' durch d ersetzt wird. Wir definieren:

Ab'(p) := Ab(p) für jedes 0-stellige Relationssymbol p
Ab'(p) := Ab(p) ∪ {(d1,...,dn)∈D'n |
di = d' für wenigstens ein i mit 1 ≤ i ≤ n
und (d1,...,dn)[d/d']∈Ab(p)}
für jedes n-stellige (n≥1) Relationssymbol p
Ab'(c) := Ab(c) für jedes 0-stellige Relationssymbol p
Ab'(f) := Ab(f) ∪ {(d1,...,dn,dn+1)∈D'n+1 |
di = d' für wenigstens ein i mit 1 ≤ i ≤ n, dn+1≠d'
und (d1,...,dn,dn+1)[d/d']∈Ab(f)}
für jedes n-stellige (n≥1) Funktionssymbol f

Die Definition für ein n-stelliges Relationssymbol p kann man auch so umschreiben: für jedes Tupel in Ab(p) , in dem d vorkommt, enthält Ab'(p) zusätzlich alle Tupel, die aus dem gegebenen entstehen, wenn ein oder mehrere Vorkommen von d durch d' ersetzt werden.

Bei einem n-stelligen Funktionssymbol entstehen für jedes Tupel in Ab(f), in dem d vorkommt, die zusätzlichen Tupel durch Ersetzen eines oder mehrerer Vorkommen von d durch d', aber nur an Argumentpositionen - dadurch wird sichergestellt, dass Ab'(f):D'n->D' linkstotal ist. An der Ergebnisposition ändert sich dagegen nichts - damit ist die Rechtseindeutigkeit von Ab(f) gewährleistet.

Notation: für eine D'-Umgebung U' bezeichne U'[d/d'] die D-Umgebung:

                            U'(x) falls U'(x)≠d'
U'[d/d'](x) := {
                            U'(x) falls U'(x)≠d'


Wir zeigen nun eine Reihe von Hilfssätzen, die im wesentlichen die erforderlichen Rechenregeln für den Hauptbeweis unter 6. bereitstellen.

  1. Für jede D-Umgebung U' und jeden Term t gilt:
    t(D',Ab',U')[d/d'] = t(D',Ab',U'[d/d']).

    Beweis durch strukturelle Induktion.

    Basisfall Konstante c:

    c(D',Ab',U')[d/d']

    = Ab'(c)[d/d'] nach Definition Interpretation
    = Ab'(c) nach Definition Ab' ist Ab'(c)≠d'
    = c(D',Ab',U'[d/d']) nach Definition Interpretation

    Basisfall Variable x:

    1. Falls U'(x) = d', gilt

      x(D',Ab',U')[d/d']
      = U'(x) = [d/d'] nach Definition Interpretation
      = d'[d/d'] nach Annahme
      = d nach Definition [d/d']
      = U'[d/d'](x) nach Definition U'[d/d']
      x(D',Ab',U'[d/d']) nach Definition Interpretation

    2. Falls U'(x) ≠ d', gilt

      x(D',Ab',U')[d/d']
      = U'(x) = [d/d'] nach Definition Interpretation
      = U'(x) nach Annahme U'(x) ≠ d'
      = U'[d/d'](x) nach Definition U'[d/d']
      x(D',Ab',U'[d/d']) nach Definition Interpretation

    Induktionsfallf(t1,...,tn):

    Es gelte
    t1(D',Ab',U')[d/d'] = t1(D',Ab',U'[d/d'])
                               .
                               .
                               .
    tn(D',Ab',U')[d/d'] = t1(D',Ab',U'[d/d'])

    dann gilt
    f(t1,...,tn)(D',Ab',U')[d/d']

    = Ab'(f)(t1(D',Ab',U'),...,tn(D',Ab',U'))[d/d'] Def. Interpretation
    = Ab'(f)(t1(D',Ab',U'),...,tn(D',Ab',U')) da Ab'(f)(...) ≠ d'
    = Ab'(f)(t1(D',Ab',U')[d/d'],...,tn(D',Ab',U')[d/d']) Def. Ab'
    = Ab'(f)(t1(D',Ab',U'[d/d']),...,tn(D',Ab',U'[d/d'])) Indukt.annahme
    f(t1,...,tn)(D',Ab',U'[d/d']) Def. Interpretation

  2. Für jede D'-Umgebung U' gilt
    (t1,...,tn)(D',Ab',U') ∈ Ab'(p)
    gdw.
    (t1,...,tn)(D',Ab',U'[d/d']) ∈ Ab'(p)

    ,,→``: Sei ti(D',Ab',U') = di.
    Aus der Annahme folgt (d1,...,dn) ∈ Ab'(p) und di ∈ D'. Falls alle di ≠ d' sind, ist (d1,...,dn)[d/d'] = (d1,...,dn) und nach Definition von Ab' gilt (d1,...,dn) ∈ Ab(p). Falls einige di = d' sind, ist (d1,...,dn)[d/d'] ∈ Ab(p) nach Definition von Ab'. In jedem Fall ist (t1,...,tn)(D',Ab',U')[d/d'] ∈ Ab(p) und wegen 1. gilt die Behauptung.

    ,,←``: Sei ti(D',Ab',U') = di.
    Wegen 1. folgt aus der Annahme: (t1,...,tn)(D',Ab',U')[d/d'] ∈ Ab'(p), also (d1,...,dn)[d/d'] ∈ Ab'(p). Nach Definition von ∈ Ab' ist dann (d1,...,dn) ∈ Ab'(p), womit die Behauptung gezeigt ist.

  3. Für jede D-Umgebung U und jeden Term t gilt t(D',Ab',U) = t(D,Ab,U).

    Beweis durch strukturelle Induktion.

    Basisfall Variable x:

    x(D',Ab',U) = U(x) = x(D,Ab,U).

    Basisfall Konstante c:

    c(D',Ab',U) = Ab'(c) = Ab(c) = c(D,Ab,U).

    Induktionsfall f(t1,...,tn):

    Es gelte t1(D',Ab',U) = t1(D,Ab,U),...,tn(D',Ab',U) = tn(D,Ab,U),
    dann gilt
    f(t1,...,tn)(D',Ab',U)

    = Ab'(f)(t1(D',Ab',U),...,tn(D',Ab',U)) Definition Interpretation
    = Ab'(f)(t1(D,Ab,U),...,tn(D,Ab,U)) Induktionsannahme
    = Ab(f)(t1(D,Ab,U),...,tn(D,Ab,U)) weil ti(D,Ab,U) ∈ D und
    dafür Ab'(f) mit Ab(f) übereinstimmt.
    = f(t1,...,tn)(D,Ab,U) Definition Interpretation

  4. Für jede D'-Umgebung U' und jede -Formel G gilt:
    es gibt e' ∈ D' mit (D,Ab,U'[e'/x][d/d'])G gdw.
    es gibt e ∈ D mit (D,Ab,U'[d/d'][e/x])G.

    ,,→``: Die Annahme gelte.
    Falls e' ≠ d', gilt U'[e'/x][d/d'] = U'[d/d'][e'/x], und aus der Annahme folgt: es gibt e' ∈ D mit (D,Ab,U'[d/d'][e'/x])G, also die Behauptung für e = e'.
    Falls e' = d', gilt U'[e'/x][d/d'] = U'[d/d'][d/x], und aus der Annahme folgt die Behauptung für e = d.

    ,,←``: Für e ∈ D ist U'[d/d'][e/x] = U'[e/x][d/d'], und wegen $e' = e$ folgt aus der Annahme die Behauptung für e' = e.

  5. Für jede D'-Umgebung U' und jede -Formel G gilt:
    für alle e' ∈ D' gilt (D,Ab,U'[e'/x][d/d'])G gdw.
    für alle e ∈ D gilt (D,Ab,U'[d/d'][e/x])G.

    ,,→``: Wegen $e' = e$ folgt aus der Annahme:
    für alle e ∈ D gilt (D,Ab,U'[e'/x][d/d']) G.
    Für e ∈ D ist e ≠ d', also U'[e/x][d/d'] = U'[d/d'][e/x], somit
    für alle e ∈ D gilt (D,Ab,U'[d/d'][e/x]) G.

    ,,←``: Für e ∈ D ist U'[d/d'][e/x] = U'[e/x][d/d'], also folgt aus der Annahme: für alle e ∈ D gilt (D,Ab,U'[e/x][d/d'])G.
    Insbesondere gilt also auch (D,Ab,U'[d/x][d/d'])G und wegen U'[d/x][d/d'] = U'[d'/x][d/d'] auch (D,Ab,U'[d'/x][d/d'])G, d.h.:
    für alle e' ∈ D' gilt (D,Ab,U'[e'/x][d/d'])G.

  6. Für jede D'-Umgebung U' und jede -Formel G gilt:
    (D,Ab,U')F gdw. (D,Ab,U'[d/d']) F.

    Beweis durch strukturelle Induktion.

    Basisfälle:
    Für $\ensuremath{{\cal L}}$, $\bot$ und nullstelliges p gilt die Behauptung.

    Für n-stelliges p mit n ≥ 1 gilt:

    gdw. Definition
    gdw. nach 2.
    gdw. ∈ Ab(p) nach 3.
    gdw. (D,Ab,U'[d/d']) p(t1,...,tn) Definition

    Induktionsfälle für Junktoren
    ergeben sich unmittelbar durch Anwendung der Definition von .

    Induktionsfall ∃:
    Die Behauptung gelte für G.

    gdw. es gibt mit Definition
    gdw. es gibt mit (D,Ab,U'[e'/x][d/d'])G Ind.annahme
    gdw. es gibt mit (D,Ab,U'[d/d'][e/x])G nach 4.
    gdw. Definition

    Induktionsfall ∀: Die Behauptung gelte für G.

    gdw. für alle gilt Definition
    gdw. für alle gilt (D,Ab,U'[e'/x][d/d'])G Ind.annahme
    gdw. für alle gilt (D,Ab,U'[d/d'][e/x])G nach 5.
    gdw. (D,Ab,U'[d/d'])∀xG Definition

  7. Jede D-Umgebung U ist auch eine D'-Umgebung, für die obendrein gilt. Der Beweis des Modellerweiterungssatzes ergibt sich nun für M' = (D',Ab',U) unmittelbar aus 6.

Die Bedeutung des Modellerweiterungssatzes liegt zunächst darin, dass er eine eindeutige Axiomatisierung der Gleichheitsrelation durch eine Menge von -Formeln ausschließt.

Angenommen, wir hätten eine solche Menge zur Verfügung, die erzwingt, dass ihre Modelle das Relationssymbol mit der Gleichheitsrelation auf dem Universum interpretieren. Dann fügen wir die Formel ∀x∀y xy zu dieser Menge hinzu. Wenn wirklich mit der Gleichheitsrelation interpretiert würde, müsste jedes Modell der erweiterten Formelmenge ein einelementiges Universum haben. Nach dem Modellerweiterungssatz gilt aber: wenn es ein Modell mit einem einelementigen Universum gibt, dann gibt es auch ein Modell mit einem zweielementigen (und folglich auch mit noch größerem) Universum, dessen Elemente alle zueinander in der Relation stehen, mit der interpretiert wird. Also gibt es keine Formelmenge, die erzwingt, dass ihre Modelle das Gleichheitsrelationssymbol nur mit der Gleichheitsrelation interpretieren können.

Eine weitere Folge des Modellerweiterungssatzes ist, dass keine Formelmenge erzwingen kann, dass die Universen ihrer Modelle eine Höchstzahl von Elementen haben. Man kann also für keine natürliche Zahl n ausdrücken, dass es ,,höchstens n`` Objekte geben soll. Dagegen ist es bemerkenswerterweise möglich, mit -Formeln zu erzwingen, dass es ,,mindestens n`` Objekte gibt. Ebenso ist ausdrückbar, dass es unendlich viele Objekte geben soll.

Mit der im folgenden vorgestellten in die Logik ,,eingebauten`` Gleichheitsrelation lässt sich immerhin erreichen, dass für jede vorgegebene natürliche Zahl n ,,höchstens n`` ausdrückbar wird. Allerdings ermöglicht auch die PL1S mit eingebauter Gleichheit nicht, ,,höchstens endlich viele`` auszudrücken, ohne eine konkrete Zahl als Obergrenze vorzugeben (wir werden in Abschnitt 4.9 auf dieses Thema zurückkommen). Diese Nichtausdrückbarkeit einer Obergrenze setzt sich übrigens im Unendlichen fort. Nach dem sogenannten ,,aufsteigenden Satz von Löwenheim und Skolem`` gilt für jede Formelmenge der PL1S mit eingebauter Gleichheit, die ein Modell mit unendlichem Universum hat: für jede beliebige Menge hat die Formelmenge auch ein Modell, dessen Universum mindestens so groß ist wie diese Menge.

Doch nun zur angekündigten eingebauten Gleichheitsrelation.

Definition 3.6.2 (Normale Interpretation).   Eine -Interpretation
M = (D,Ab,U) heißt normal, wenn die Gleichheitsrelation auf D ist. Ist eine normale Interpretation M ein Modell einer Formel F, schreibt man MF. Die Folgerungsbeziehung bezüglich normaler Modelle wird ebenfalls notiert.

Mit Definition 3.6.2 ist die Semantik von Sprachen der PL1S mit Gleichheit festgelegt. Wie wir gesehen haben, ist die Gleichheitsrelation durch Formeln der PL1S nicht eindeutig axiomatisierbar. Wir untersuchen nun, wie weit man mit einer solchen Axiomatisierung genau kommt.

Definition 3.6.3 (Gleichheitsaxiome).   Das Gleichheitsaxiomensystem für eine Sprache der PL1S ist

:= {Refl} ∪ {Subf | f n-stelliges Funktionssymbol in , n ≥ 1}
∪ {Subp | p n-stelliges Relationssymbol in , n ≥ 1}

Reflexivitätsaxiom:

Verträglichkeitsaxiom für ein n-stelliges (n ≥ 1) Funktionssymbol:

Verträglichkeitsaxiom für ein n-stelliges (n ≥ 1) Relationssymbol:
Subp := ∀x1...∀xn∀x'1...∀x'n
((x1x'1 ∧...∧ xnx'n) ⇒ (p(x1,...,xn) ⇒ p(x'1,...,x'n)))

Bemerkungen:  
  1. Die Verträglichkeitsaxiome drücken das Leibniz'sche Prinzip ,,identitas indiscernibilium``, also der Identität der ununterscheidbaren Dinge aus: das Gleiche darf durch das Gleiche in einer Aussage ersetzt werden, ohne die Gültigkeit der Aussage zu verändern.
  2. In der Regel ist unendlich. (Warum?)

Mit wird das Prinzip ,,identitas indiscernibilium`` für die einfachsten Terme und Formeln sichergestellt. Der folgende Satz zeigt, dass es auch für komplexere Terme und Formeln, also für die PL1S allgemein, gilt.

Satz 3.6.4.  
  1. Seien t ein -Term mit var(t) = {x1,...,xn}, seien mit m ≥ n paarweise verschiedene Variablen, so dass kein x'i gleich einem xj ist, und sei t' der Term, der sich aus t ergibt, wenn jedes Vorkommen von xi durch x'i ersetzt wird für . Es gilt:
    {Refl} ∪ {Subf | f n-stelliges Funktionssymbol in , n≥1}

    ∀x1...∀xn∀x'1...∀x'm (x1x'1 ∧...∧ xmx'm ⇒ tt')

  2. Seien F eine -Formel mit fvar(F) = {x1,...,xn}, seien mit m ≥ n paarweise verschiedene Variablen, so dass kein x'i gleich einem xj ist, und sei F' die Formel, die sich aus F ergibt, wenn jedes freie Vorkommen von xi durch x'i ersetzt wird für . Es gilt:


    ∀x1...∀xn∀x'1...∀x'm (x1x'1 ∧...∧ xmx'm ⇒ (F⇒F')

Beweis:   Strukturelle Induktion über den Aufbau von Termen und Formeln.

Die Gleichheitsaxiome werden häufig so formuliert, dass auch ein Symmetrieaxiom und ein Transitivitätsaxiom enthalten sind. Diese folgen aus den Gleichheitsaxiomen in der obigen Formulierung.

Satz 3.6.5.  
  1.     wobei   Sym := ∀x∀y (xy ⇒ yx)
  2.   wobei  

Beweis:  

  1. ∀x∀y∀x'∀y'(xx' ∧ yy' ⇒ (xy ⇒ x'y')) das ist Sub
    Verschmelzung
    von x,y,y' zu y'
    ∀x'∀y'(y'x' ∧ y'y' ⇒ (y'y' ⇒ x'y')) Satz 3.5.13, 3.3.7
    ∀x∀y(xx ∧ xx ∧ xy ⇒ yx) Umbenennung

    Mit gilt damit auch $F = y{\doteq}z$ x∀y(xy ⇒ yx).

  2. Wir wenden Satz 3.6.4 (2) auf F = yz an und erhalten

    ∀y∀z∀y'(yy' ⇒ (yz ⇒ y'z))
    ∀y∀z∀y'(y'y ∧ yz ⇒ y'z) da
    ∀y∀z∀y'(xy ∧ yz ⇒ xz) Umbenennung

Man beachte, dass sowohl Satz 3.6.4 als auch Satz 3.6.5 keine Aussagen über normale Modelle von sind, sondern über beliebige Modelle von , also auch nichtnormale. Auch die Folgerungsbeziehung ist jeweils und nicht . Den Zusammenhang zwischen beliebigen Modellen von und normalen Interpretationen stellt der folgende Satz her.

Satz 3.6.6.  
  1. Jede normale Interpretation ist ein Modell von .
  2. Zu jedem Modell M von gibt es ein normales Modell M' von , so dass für jede -Formel F gilt gdw. M'F
  3. Für jede Formelmenge S und jede Formel F gilt
    gdw. S ∪ F.

Beweis: (skizziert)  
  1. Im wesentlichen durch Ausrechnen. Die Gleichheitsrelation besitzt die von verlangten Eigenschaften.

  2. Sei M = (D,Ab,U) das Modell von . Wir schreiben ~ für die zweistellige Relation Ab() auf dem Universum D.

    Da M die Formeln in erfüllt, kann man leicht nachweisen, dass ~ eine Äquivalenzrelation ist. Obendrein besitzt sie folgende Strukturverträglichkeitseigenschaften, ist also eine Kongruenzrelation:

    Für jedes n-stellige Funktionssymbol f:
    wenn , dann Ab(f)(d1,...,dn) ~ Ab(f)(e1,...,en).

    Für jedes n-stellige Relationssymbol p:
    wenn ,
    dann (d1,...,dn)∈Ab(p) gdw. (e1,...,en)∈Ab(p).

    Für jedes d ∈ D bezeichne [d] die Äquivalenzklasse bezüglich ~. Es gilt also d ~ e gdw. [d]=[e]. Wir definieren
    .

    $U'(x) := [U(x)]$ := [Ab(c)]
    für 0-stelliges Funktionssymbol c
    Ab'(f)([d1],...,[dn]) := [Ab(f)(d1,...,dn)]
    für n-stelliges (n≥1) Funktionssymbol f
    Ab'(p) := Ab(p)
    für 0-stelliges Relationssymbol p
    Ab'(p) := {([d1],...,[dn]) | (d1,...,dn)∈Ab(p)}
    für n-stelliges (n≥1) Relationssymbol p


    M' := (D',Ab',U')

    Dass Ab' wohldefiniert ist, ergibt sich unmittelbar aus den obigen Kongruenzeigenschaften von ~.

    Durch strukturelle Induktion zeigt man, dass für jede Formel F gilt gdw. M'F.

  3. ,,→``: Wir nehmen an, es gilt . Sei M ein Modell von S ∪ . Nach 2. gibt es ein normales Modell M' von S∪, das dieselben Formeln erfüllt wie M. Nach Annahme gilt M'F. Also gilt auch .

    ,,←``: Wir nehmen an, es gilt S ∪ . Sei M' ein normales Modell von S. Nach 1. ist M' auch ein Modell von . Nach Annahme gilt dann auch M' F.

Dieses Ergebnis mildert die Bemerkungen im Anschluss an den Modellerweiterungssatz wieder ab. Zwar kann man mit oder mit einer anderen Formelmenge nicht verhindern, dass das Gleichheitsrelationssymbol mit einer größeren Relation als der Gleichheit interpretiert wird. Aber in diesen größeren Modellen gilt auch nicht mehr und nicht weniger als in dem entsprechenden normalen Modell, und die Folgerungsbeziehung verändert sich dadurch auch nicht.

Validierung