Prädikatenlogik/Gleichheitstautologien/Folgerungen/Fakt

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

$⊢ s = t \to t = s .$

$⊢ r = s \land s = t \to r = t .$

$⊢ s_{1} = t_{1} \land \dots \land s_{n} = t_{n} \to f s_{1} \dots s_{n} = f t_{1} \dots t_{n} .$

$⊢ s_{1} = t_{1} \land \dots \land s_{n} = t_{n} \land R s_{1} \dots s_{n} \to R t_{1} \dots t_{n} .$

Zum Beweis, Alternativen Beweis erstellen