In der Vorlesung wurde gesagt, dass beim Baumkalkül bei der Existenzbeseitigung immer eine neue Konstante genommen werden muss („Die Konstante muss neu sein, sie darf auf dem Ast nicht vorkommen, der erweitert wird.“). Ich hatte aber das Gefühl, dass bei Aufgabe 1b, c, d und f genau dies nicht befolgt wurde. Habe ich die Regel falsch verstanden und darf die Konstante nur nicht bei der Formel, die man gerade „auflösen“ möchte, bereits vorhanden sein (was weiter oben ist, ist egal?) ? Wenn dem so wäre, verstehe ich nicht, wieso man bei Aufgabe 3b dann die Formel -Ax(Px ^ Qx -> Rx) in Zeile 10 nicht einfach mit -(Pa ^ Qa -> Ra) auflösen konnte (anstatt Formel in Zeile 12)? Dann wäre der Baum sehr schnell geschlossen gewesen…
(^ entspricht Konjunktion, -> entspricht Konditional, – entspricht Negation, A entspricht der Allaussage)
Danke im Voraus für eure Hilfe.
One Comment
Die Konstante, die bei einer Existenzbeseitigung neu eingeführt werden muss, darf auf dem ganzen Ast des Baumes (von der zu entwickelnden Formel bis ganz nach oben zum Ursprung des Baums) noch nicht vorgekommen sein.
Bitte beachte: Mit einem negierten Existenzquantor wird eine Allaussage gemacht!!! (Vgl.: ¬∃xPx ist äquivalent zu ∀x¬Px) D.h. bei der Elimination eines neg. Existenzquantors darf die Konstante beliebig gewählt werden, da es sich um eine Allbeseitigung handelt.
Umgekehrt wird mit einem negierten Allquantor eine Existenzaussage gemacht. (Vgl.: ¬∀xPx ist äquivalent zu ∃x¬Px)
Herzlich, Simon
Post a Comment