Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Substitution
(Aufgabentyp: Uebung 9 Aufgabe 2.2)
Da unsere Korrektur bei dieser Aufgabe nicht sehr konstruktiv ist, wollte ich mich hier nochmal vergewissern, ob die folgende Heransgehensweise passt.
(∃X. p(X)) ∧ ∀Y. (r(Y, Z) ∨ ∃Z. r(X, Z)))
gilt es mit σ := [f (X, Y )/X, c/Y, f (f (X, Y ), Z)/Z]
zu substituieren
- Schritt:
(∃X. p(X)) ∧ ∀Y. (r(Y, Z) ∨ ∃Z. r(X, Z)))[f (X, Y )/X, c/Y, f (f (X, Y ), Z)/Z]
Man soll alle freien X durch f (X, Y ) ersetzen.
Fragen:
- Ist es korrekt auch die auftretenden X im Rest von σ zu ersetzen? (wie schon rot hervorgehoben)
- Da das Y hier im zu ersetzenden Abschnitt allerdings
gebunden ist wuerde ich alle freien Y vor dem 1. Schritt
z.B. durch Y* ersetzen.
Ist das legitim:
(∃X. p(X)) ∧ ∀Y. (r(Y, Z) ∨ ∃Z. r(X, Z)))[f (X, Y )/X, c/Y, f (f (X, Y ), Z)/Z]
→
(∃X. p(X)) ∧ ∀Y. (r(Y, Z) ∨ ∃Z. r(X, Z)))[f (X, Y* )/X, c/Y*, f (f (X, Y*), Z)/Z]
…?
edit:
wenn ich das so durchzieh’ komm ich auf:
(∃X. p(X)) ∧ ∀Y. (r(Y, f(f(f(X,c),c),Z)) ∨ ∃Z. r(f(X, c),Z))