# Prädikatenlogik/Syntaktische Tautologien/Gleichheitstautologien/Textabschnitt

In der Prädikatenlogik gelten die beiden folgenden Tautologien für die Gleichheit.

## Axiom

Es sei $S$ ein Symbolalphabet, $s,t$ seien $S$-Terme und $\alpha$ sei ein $S$-Ausdruck. Dann sind die beiden folgenden Ausdrücke syntaktische Tautologien.
    $\vdash t=t.$
    $\vdash s=t\wedge \alpha {\frac {s}{x}}\rightarrow \alpha {\frac {t}{x}}.$
Diese beiden Axiome (oder genauer Axiomenschemata) heißen Gleichheitsaxiom und Substitutionsaxiom. Mit einer aussagenlogischen Umformulierung sieht man, dass das Substitutionsaxiom äquivalent zu
    $\vdash s=t\rightarrow {\left(\alpha {\frac {s}{x}}\rightarrow \alpha {\frac {t}{x}}\right)}$
ist.

## Lemma

Die Gleichheitsaxiome
sind korrekt.

### Beweis

Es sei $I$ eine beliebige $S$-Interpretation. (1). Aufgrund der Bedeutung des Gleichheitszeichens unter jeder Interpretation gilt $I(t)=I(t)$, also
    $I\vDash t=t.$
(2). Es gelte
    $I\vDash s=t\wedge \alpha {\frac {s}{x}},$
also $I\vDash s=t$ und $I\vDash \alpha {\frac {s}{x}}$. Das bedeutet einerseits $I(s)=I(t)$. Andererseits gilt nach dem Substitutionslemma
    $I{\frac {I(s)}{x}}\vDash \alpha .$
Wegen der Termgleichheit gilt somit auch
    $I{\frac {I(t)}{x}}\vDash \alpha$
und daher, wiederum aufgrund des Substitutionslemmas, auch
    $I\vDash \alpha {\frac {t}{x}}.$
$\Box$
Bei leerer Variablenmenge ist das Substitutionsaxiom aussagelos. In Hinblick auf Fakt fordern wir, dass die Variablenmenge stets unendlich ist.

## Lemma

Aus den Gleichheitsaxiomen lassen sich folgende Gleichheitstautologien ableiten (dabei sind $r,s,t,s_{1},\ldots ,s_{n},t_{1},\ldots ,t_{n}$ Terme, $f$ ein $n$-stelliges Funktionssymbol und $R$ ein $n$-stelliges Relationssymbol).

### Beweis

(1). Aufgrund der Gleichheitsaxiome haben wir
    $\vdash s=s$
und
    $\vdash s=t\wedge (x=s){\frac {s}{x}}\rightarrow (x=s){\frac {t}{x}},$
wobei $x$ eine Variable sei, die weder in $s$ noch in $t$ vorkomme. Daher sind die beiden substituierten Ausdrücke gleich $s=s$ bzw. $t=s$. Eine aussagenlogische Umstellung der zweiten Zeile ist
    $\vdash s=s\rightarrow (s=t\rightarrow t=s),$
sodass sich aus der ersten Zeile mittels Modus ponens
    $\vdash s=t\rightarrow t=s$
ergibt. (2). Es sei wieder $x$ eine Variable, die weder in $r$ noch in $s$ noch in $t$ vorkomme. Eine Anwendung des Substitutionsaxioms liefert
    $\vdash s=t\wedge (r=x){\frac {s}{x}}\rightarrow (r=x){\frac {t}{x}}.$
Nach Einsetzen und einer aussagenlogischen Umstellung ist dies die Behauptung. Für (3) siehe Aufgabe. (4). Es sei $u$ eine Variable, die weder in einem der $s_{i}$ noch in einem der $t_{i}$ vorkommt. Für jedes $i=1,\ldots ,n$ gilt nach Axiom (2) (mit $\alpha =\alpha _{i}=Rt_{1}\ldots t_{i-1}us_{i+1}\ldots s_{n}$) dann
    $\vdash s_{i}=t_{i}\rightarrow {\left(Rt_{1}\ldots t_{i-1}us_{i+1}\ldots s_{n}{\frac {s_{i}}{u}}\rightarrow Rt_{1}\ldots t_{i-1}us_{i+1}\ldots s_{n}{\frac {t_{i}}{u}}\right)},$
also
    $\vdash s_{i}=t_{i}\rightarrow {\left(Rt_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}\rightarrow Rt_{1}\ldots t_{i-1}t_{i}s_{i+1}\ldots s_{n}\right)}.$
Diese Ableitbarkeiten gelten auch, wenn man die Vordersätze durch ihre Konjunktion
    $(s_{1}=t_{1})\wedge \ldots \wedge (s_{n}=t_{n})$
ersetzt. Durch die Transitivität der Implikation ergibt sich daher
    $\vdash (s_{1}=t_{1})\wedge \ldots \wedge (s_{n}=t_{n})\rightarrow {\left(Rs_{1}\ldots s_{n}\rightarrow Rt_{1}\ldots t_{n}\right)}.$
$\Box$