Prädikatenlogik/Substitutionslemma/Fakt/Beweis/Aufgabe/Lösung

Aus Wikiversity
Zur Navigation springen Zur Suche springen

Dies wird über den induktiven Aufbau der Terme bewiesen. (1). Für eine Konstante ist die Aussage richtig, da ihre Interpretation unverändert ist. Für eine Variable macht man eine Fallunterscheidung. Wenn

mit einer der an der Substitution beteiligten Variablen ist, so ist

Bei einer an der Substitution nicht beteiligten Variablen ist

Wenn ein -stelliges Funktionssymbol ist und Terme sind, für die die Gleichheit schon bekannt ist, so ist

Zur gelösten Aufgabe