Zum Inhalt springen

Prädikatenlogik/Existenzeinführung im Antezedens/Korrektheit/Fakt/Beweis

Aus Wikiversity
Beweis

Es sei allgemeingültig, d.h.

für jede -Interpretation . Wir müssen zeigen, dass dann auch allgemeingültig ist (unter den gegebenen Voraussetzungen). Es sei dazu eine Interpretation mit

Aufgrund der Modellbeziehung bedeutet dies, dass es ein (aus der Grundmenge der Interpretation) mit

gibt. Die Variable kommt nach Voraussetzung in nicht frei vor, d.h. bei , dass in nicht frei vorkommt. Wir können daher das Koinzidenzlemma anwenden und erhalten

Diese Aussage gilt trivialerweise auch bei . Damit gilt auch

Wir schreiben dies (etwas künstlich) als

Darauf können wir das Substitutionslemma (für die Interpretation und den Term ) anwenden und erhalten

Wegen der vorausgesetzten Allgemeingültigkeit von folgt

Da in nicht frei vorkommt, liefert das Koinzidenzlemma