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.
Natural Deduction in First Order Logic
Ich dachte es eigentlich verstanden zu haben, bin jetzt aber doch wieder verwirrt.
In Assignement 10.1 Teil 2: warum kann man da nicht einfach folgendermaßen herangehen.
Annahme
[P(X)]^1
forall Y.P(Y) forall-Introduction (Umbenennung der Variable macht ja nix)
P(X) → forall Y.P(Y) → Introduction
exists X. P(X) → forall Y.P(Y) exists-Introduction
Die exists-Introduction wurde so auch in der Musterlösung gemacht, die scheint also zu passen.
Also scheitert es wohl an der forall-Introduction.
Auf den Folien steht *means that A does not depend on any hypothesis in which X is free
Diese Aussage verstehe ich schon nicht, weil was soll “abhängen” in dem Fall bedeuten.
Kann mir da jemand ein konkretes Gegenbeispiel geben, wann etwas von einer Hypothese abhängt.
Wenn es oben an der Umbenennung scheitert, dann verstehe ich das auch nicht, weil
exists X. P(X) → forall X.P(X) ist doch gleichbedeutend, da das innere X von P(X) vom forall abhängt.
Also generell, wenn ich eine Aussage A habe. Wann darf ich dann
forall X. A
und wann darf ich dann
exists X. A
folgern? Mir kommt es so vor, als dürfe man exists X. A immer folgern, jedoch forall nur unter mir nicht offensichtlichen Einschränkungen.
Genau das was du da machst soll das heißen 
An der Stelle an der du die Forall-Introduction machst ist eine Annahme/Hypothese offen (nämlich P(X) ), die X frei enthält. Das darf nicht passieren.
forall x.A darfst du folgern wenn du keine offene Annahme hast, die X frei enthält. exists X. A darfst du immer folgern
1 „Gefällt mir“
Und wie ist es dann bei Problem 10.1.1? Als Annahme macht man dort X ≤ -X (in der X als freie Variable auftaucht). Später in Zeile 3 wird dann mit ⇒I X ≤ −X ⇒ ∃Y.X ≤ Y. In Zeile 4 wird dann durch ∀I die Formel ∀X.(X ≤ −X ⇒ ∃Y.X ≤ Y ) hergleitet. Der Vierte Schritt wäre doch jetzt nicht erlaubt, da X als freie Variable in den Hypothesen (Assumption 1) auftaucht.
Die Hypothese ist nicht mehr offen, also ist das erlaubt. (original in den Folien steht: “means that A does not depend on any hypothesis in which X is free”). Depend meint hier, dass die Hypothese noch offen ist, nehme ich mal sehr stark an.
2 „Gefällt mir“
Danke, jetzt habe ich es verstanden 
1 „Gefällt mir“
Ganz genau 
Nach der =>-Introduction ist die Annahme geschlossen, dann ist die Regel also erlaubt
Ich sollte vielleicht auch nochmal auf diesen post verweisen; da wurde die regel und die nebenbedingung auch schon diskutiert:
https://fsi.cs.fau.de/forum/thread/15652-A-question-regarding-the-Sequent-Calculus