Prädikatenlogik/Ableitungskalkül/Surjektivität/Verknüpfung/Beispiel

Wir wollen zeigen, dass im Sequenzenkalkül

ableitbar ist, was inhaltlich bedeutet, dass die Hintereinanderschaltung von zwei surjektiven Abbildungen wieder surjektiv ist. Es sei dazu die Vereinigung der beiden Vordersätze. Wir haben dann

zu zeigen. Wir zeigen zunächst die entsprechende Existenzaussage. Aufgrund der Substitution gilt

Daraus folgt durch zweimalige Existenzaussage

Da rechts gar nicht vorkommt, erhält man aus

durch Existenzeinführung im Antezedens

Aufgrund der Existeneinführung im Sukzedens gilt

und

Durch Vertauschen der Existenzoperatoren und die Transititvität der Implikation erhält man



Wir haben zunächst

und

also

Ebenso erhält man

Es gilt ferner (Substitutionsregel)

was wir als

schreiben.