Not logged in. · Lost password · Register

Fertu
Member since Nov 2013
29 posts
Subject: 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.
Jazzpirate
Member since Oct 2016
803 posts
+1 Fertu
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.
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.

Also generell, wenn ich eine Aussage A habe. Wann darf ich dann
forall X. A
und wann darf ich dann
exists X. A
forall x.A darfst du folgern wenn du keine offene Annahme hast, die X frei enthält. exists X. A darfst du immer folgern ;)
Fuxicus
Member since Apr 2017
47 posts
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.
This post was edited on 2018-02-10, 10:54 by Fuxicus.
tyr
Avatar
Member since Oct 2014
93 posts
+2 Fertu, Jazzpirate
 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.
"Debugging is like doing surgery by randomly squeezing stuff in a patient's body and going like 'lmao tell me when this guy stops breathing'." -- Orteil, Creator of Cookie-Clicker
This post was edited on 2018-02-10, 11:33 by tyr.
Fertu
Member since Nov 2013
29 posts
+1 Jazzpirate
Danke, jetzt habe ich es verstanden :)
Jazzpirate
Member since Oct 2016
803 posts
Ganz genau ;) Nach der =>-Introduction ist die Annahme geschlossen, dann ist die Regel also erlaubt :)
Jazzpirate
Member since Oct 2016
803 posts
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-regard…
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen