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

Wir wollen zeigen, dass im Sequenzenkalkül

$\vdash (\forall x(\exists y(Fy=x)))\wedge (\forall u(\exists v(Gv=u)))\rightarrow (\forall r(\exists s(FGs=r)))$

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

$\Gamma \vdash \forall r(\exists s(FGs=r))$

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

$\vdash Fy=x\wedge Gz=y\rightarrow FGz=x.$

Daraus folgt durch zweimalige Existenzaussage

$\vdash \exists z\exists y(Fy=x\wedge Gz=y)\rightarrow \exists y\exists zFGz=x.$

Da ${}y$ rechts gar nicht vorkommt, erhält man aus

$\vdash \exists zFGz=x\rightarrow \exists zFGz=x$

durch Existenzeinführung im Antezedens

$\vdash \exists y\exists zFGz=x\rightarrow \exists zFGz=x$

Aufgrund der Existeneinführung im Sukzedens gilt

$\vdash \exists yFy=x\rightarrow \exists z\exists yFy=x$

und

$\vdash \exists zGz=y\rightarrow \exists y\exists zGz=y.$

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

$\vdash$

$\vdash \exists yFy=x\wedge \exists zGz=y\rightarrow \exists zFGz=x.$

Wir haben zunächst

$\Gamma \vdash \forall x(\exists yFy=x)$

und

$\vdash \forall x(\exists y(Fy=x))\rightarrow \exists y(Fy=x),$

also

$\Gamma \vdash \exists y(Fy=x).$

Ebenso erhält man

$\Gamma \vdash \exists z(Gz=y).$

Es gilt ferner (Substitutionsregel)

$\vdash (Fy=x)\wedge (Gz=y)\rightarrow (FGz=x),$

was wir als

$\vdash (Gz=y)\rightarrow ((Fy=x)\rightarrow (FGz=x))$

schreiben.