Propositional Calculus / Aussagenlogik #
Die Aussagenlogik ist ein Teilgebiet der Logik. Es Verknüpft Predicate (Aussagen) mit Junktoren. Diese Aussagen können entweder Wahr oder Falsch sein. Ein Junktor ist eine Logische Verknüpfung wie “und”, “oder”, “nicht”, “impliziert”.
Es gibt also im Wesentlichen 2 Eigenschaften dieser klassischen Logik:
- Jede Aussage hat genau zwei Wahrheitswerte, meistens Wahr oder Falsch.
- Jede zusammengesetzte Aussage kann durch die Wahrheitswerte ihrer Teilaussagen bestimmt werden.
Beispiel eines Predicate #
\[ A \land B \implies B \land A \]Dieses Predikat ist immer Wahr, denn die beiden Predikate A sowie B dürfen vertauscht werden. Wer mit Datenbanken gearbeitet hat, kann sich die Where Bedingung als Predikat vorstellen.
Sequents in Propositional Calculus #
In Sequenzenkalkül ist der Sequents Begriff (ist ein generischer Name für etwas, dass wir beweisen wollen) eingeführt worden und soll für diese Logik erweitert werden.
Eine Sequent ist nun definiert als \( H \vdash G \) und wird gelesen als “Unter der Hypothesis H, beweise das Ziel G”. H kann auch als Set von Annahmen bezeichtnet werden, die alle zutreffen müssen, damit G gilt. H ist dabei eine Menge von Predikaten und G ist ein einzelnes Predikat. Damit ein Ziel G bewiesen werden kann, müssen alle Hypothesen zutreffen. Ein Predikat P ist nur valide, wenn und nur wenn es einen kompletten Beweis der Sequent \( \vdash P \) in der Theorie gibt. Das bedeutet, dass das Predikat ohne Annahmen gültig ist.
Syntax eines Predicate #
\[ P ::= \bot \mid \neg P \mid P \land P \] \[ \top \equiv \neg \bot \] \[ P \lor Q \equiv \neg (\neg P \land \neg Q) \] \[ P \implies Q \equiv \neg P \lor Q \] \[ P \iff Q \equiv (P \implies Q) \land (Q \implies P) \]Die Bindungsstärke ist mit den Symbolen aus der klassichen Logik identisch. Das Symobl \(\equiv\) gehört natürlich nicht zur Sprache und wird hier nur für das Aufzeigen der Syntax verwendet.
Proof Rules von Propositional Calculus #
Axiom #
\[ \frac{}{H, P \vdash P}hyp \]Unter der Annahme H oder P, gilt P ist immer zutreffend.
\[ \frac{}{H, \bot \vdash P}\top goal \]Wenn eine der Annahmen falsch ist, spielt P keine Rolle mehr.
\[ \frac{}{H \vdash \top}\top hyp \]Wenn die Schlussfolgerung wahr ist, müssen die Hypothesen nicht mehr bewiesen werden.
Strukturelle Regel #
\[ \frac{H \vdash Q}{H, P \vdash Q}mon \]Hier ist es einfacher, wenn zuerst nur ein Sequent betrachtet wird. Das Antecedent (Rechte-Seite) darf immer strenger sein als vorher, denn diese engen den Beweis ein (z.B. Autos haben Räder wird zu schwarze Autos haben Räder). Im Succedent (Linker Teil) ist es auch erlaubt, denn es darf eine alternative Schlussfolgerung geben (daraus folgt bzw. beweist, dass Autos Räder oder Flügel haben). Die Regel ist also sinnvoll von oben nach unten gelesen. Bei einem Beweis wird jedoch von unten nach oben gearbeitet und es muss also erraten werden, was entfernt werden darf.
Cut Regel #
\[ \frac{H \vdash P \ \ \ H, P \vdash Q}{H \vdash Q}cut \]Bei der Cut Regel ist es verständlicher, wenn sie von oben nach unten gelesen wird. Wenn P sowohl in der Annahme wie auch im Ziel vorkommt, darf P entfernt und die zwei Prädikate zusammengeführt werden. Das Linke Prädikat beweist P, weshalb es im rechten Prädikat “überflüssig” ist. Wenn es von unten nach oben gelesen wird, wird eine neue Annahme eingeführt, die es dann aber auch separat zu beweisen gilt.
Da beim Beweis von unten nach oben gearbeitet wird, entsteht die Schwierigkeit zu erraten was P sein könnte.
Widerspruchsbeweis #
\[ \frac{H, \neg P \vdash \bot}{H \vdash P}contr \]Es wird dann angenommen, dass P den anderen Wert hat und das Sequent damit falsch sein muss.
\[ \frac{H, P \vdash \bot}{H \vdash \neg P}\neg goal \]Es wird dann angenommen, dass P den anderen Wert hat und das Sequent damit falsch sein muss.
\[ \frac{H \vdash P}{H, \neg P \vdash Q}\neg hyp \]Um zu Beweisen, dass \(H, \neg P \vdash Q\) gilt, genügt es zu beweisen, dass \(H \vdash P\) gilt. Wenn P gilt, ist eine der Hypothesen falsch und somit das Sequent.
Und Regeln #
\[ \frac{H \vdash P \ \ \ H \vdash Q}{H \vdash P \land Q}\land goal \] \[ \frac{H, P, Q \vdash R}{H, P \land Q \vdash R}\land hyp \]Abgeleitete Regeln #
Mit diesen Regeln und Synatxumwandlungen, können diese Regeln erstellt werden.