tableau-kalkül
-
hallo!
kann mir vielleicht jemand erklären was es mit dem tableau-kalkül auf sich hat? das das eine methode ist, um formeln zu beweisen, ist mir klar, aber wie geht das vor sich?
D-U-D-E
-
Das funktioniert durch Widerspruchsbeweis.
Du nimmst Deine Axiome und die Aussage die Du beweisen willst negiert.
Dann zerlegst Du alles. Jede Konjunktion wird in ihre Bestandteile zerlegt, bei Disjunktionen kriegst Du halt Verzweigungen im Beweis. Dann darfst Du noch Formeln mit Existenzquantor instanziieren, indem Du nur die Formel vor der der Ex-Quantor steht mit ner neuen(!) Konstanten, dafür ohne Quantor hinschreibst. Und die Formeln mit Allquantor darfste mit beliebigen Konstanten drin benutzen. Du bist fertig, sobald Du in jedem Zwei einmal eine Formel und deren Negation drinstehen hast.Im Prinzip modelliert das nur ein paar grundlegende Vorgehensweisen:
und: alle Teile müssen wahr sein, man kann die Formeln also einzeln hinschreiben.
oder: wir müssen ne Verwzeigung machen, weil das eine oder das andere wahr sein kann. Wir müssen nämlich beide Fälle zum Widerspruch führen.Der Existenzquantor darf so benutzt werden, weil wir nämlich wissen, daß es ein Element gibt, sodaß dir Formel wahr ist, also können wir dem Element auch einen Namen geben. Aber halt keinen den es schon gibt.
Wenn zum Beispiel gilt: a=5 sowie es ex. x mit x=7, dann dürfen wir für x halt nicht a nehmen sondern müssen was neuen nehmen, z.B: b
Bei Formeln mit Allquantor dürfen wir dann wieder alles benutzen. Diese Formeln braucht man dann oft um einen Widerspruch zu den aus den Ex-Quantoren gefundenen Formeln zu konstruieren.
MfG Jester
-
ok, ich hab hier dann folgende aufgabe:
a = (-(E v -C) ^ D) ^ (-(-(E v -C) ^ D))
löse ich folgendermaßen:
0: T((-(E v -C) ^ D) ^ (-(-(E v -C) ^ D)))
1: T(-(E v -C) ^ D)
2: T(-(-(E v -C) ^ D))
3: F(-(E v -C) ^ D)und da hab ich den widerspruch, da ein und derselbe term gleichzeitig true und false sein muss. richtig?
D-U-D-E
-
Japp. Stimmt.
Das war aber ein einfacher Fall.