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.

1. $\vdash t=t.$

2. $\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).

1. $\vdash s=t\rightarrow t=s.$

2. $\vdash r=s\wedge s=t\rightarrow r=t.$

3. $\vdash s_{1}=t_{1}\wedge \ldots \wedge s_{n}=t_{n}\rightarrow fs_{1}\ldots s_{n}=ft_{1}\ldots t_{n}.$

4. $\vdash s_{1}=t_{1}\wedge \ldots \wedge s_{n}=t_{n}\wedge Rs_{1}\ldots s_{n}\rightarrow Rt_{1}\ldots t_{n}.$

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$