Prädikatenlogik/Gleichheitstautologien/Folgerungen/Funktion/Aufgabe/Lösung

Es sei ${}u$ eine Variable, die weder in einem der ${}s_{i}$ noch in einem der ${}t_{i}$ vorkommt. Für jedes ${}i=1,\ldots ,n$ setzen wir ${}\alpha _{i}:=ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}us_{i+1}\ldots s_{n}$. Nach Axiom  (2) ergibt sich daraus

$\vdash s_{i}=t_{i}\rightarrow {\left(\alpha _{i}{\frac {s_{i}}{u}}\rightarrow \alpha _{i}{\frac {t_{i}}{u}}\right)},$

also

$\vdash s_{i}=t_{i}\rightarrow {\left({\left(ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}\right)}\rightarrow {\left(ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}t_{i}s_{i+1}\ldots s_{n}\right)}\right)}.$

Da der Vordersatz in der Implikation rechts nach Axiom  (1) ableitbar ist, ergibt eine aussagenlogische Umformulierung

$\vdash s_{i}=t_{i}\rightarrow {\left(ft_{1}\ldots t_{i-1}s_{i}s_{i+1}\ldots s_{n}=ft_{1}\ldots t_{i-1}t_{i}s_{i+1}\ldots s_{n}\right)}.$

Diese Ableitbarkeiten gelten auch, wenn man die Vordersätze durch ihre Konjunktion

$(s_{1}=t_{1})\wedge \ldots \wedge (s_{n}=t_{n})$

ersetzt. Durch die Transitivität der Implikation ergibt sich daher

$\vdash (s_{1}=t_{1})\wedge \ldots \wedge (s_{n}=t_{n})\rightarrow {\left(fs_{1}\ldots s_{n}=ft_{1}\ldots t_{n}\right)}.$

Zur gelösten Aufgabe