www.wikidata.de-de.nina.az

Baumkalkül e oder Tableaukalküle nach ihrem Erfinder auch Beth Kalküle genannt sind Widerlegungskalküle der Logik Der Na

Baumkalkül

Baumkalküle oder Tableaukalküle, nach ihrem Erfinder auch Beth-Kalküle genannt, sind Widerlegungskalküle der Logik.

Der Name Baumkalkül rührt daher, dass beim Ableiten in einem Beth-Kalkül eine Baumstruktur erzeugt wird. Diese Aussage ist eine Beschreibung, keine Definition, weil nicht jeder Kalkül, der Baumstrukturen erzeugt, auch Baumkalkül genannt wird. Die entstandenen Baumstrukturen werden auch Beth-Tableaux oder Beth-Tableaus (französischer bzw. eingedeutschter Plural von Beth-Tableau) genannt.

Grundlagen Bearbeiten

Für klassische Logiken lässt sich intuitiv ein semantischer Schlussbegriff fassen: Ein Argument ist genau dann gültig, wenn unter allen Interpretationen, unter denen alle Prämissen wahr sind, auch die Konklusion wahr ist; kürzer, prägnanter und mit Leibniz: Aus Wahrem folgt nur Wahres. Somit ist ein Argument genau dann ungültig, wenn es mindestens eine Interpretation gibt, unter der alle Prämissen wahr sind, die Konklusion aber falsch ist.

Wenn ein Satz falsch ist, dann ist nach der klassischen Semantik seine Verneinung wahr. Statt zu sagen, ein Argument ist genau dann ungültig, wenn es mindestens eine Interpretation gibt, unter der alle Prämissen wahr sind, unter der die Konklusion aber falsch ist, kann man daher genauso gut folgendes sagen: Ein Argument ist genau dann ungültig, wenn es mindestens eine Interpretation gibt, unter der alle Prämissen wahr sind und unter der auch die Negation der Konklusion wahr ist.

Kürzer: Ein Argument , wobei die Menge der Prämissen, die Konklusion ist und das metalogische Zeichen die Gültigkeit des Arguments aussagt, ist genau dann ungültig, wenn es mindestens eine Interpretation I gibt, unter der jeder Satz aus wahr ist, unter der aber falsch ist. Da nach der Semantik der Negation I() = F genau dann, wenn I() = W, ist genau dann ungültig, wenn I nicht nur jeden Satz aus , sondern auch wahr macht, wenn also I jeden Satz aus der Menge wahr macht. Ein Argument ist also genau dann ungültig, wenn die Menge erfüllbar ist, und im Umkehrschluss genau dann gültig, wenn die Menge unerfüllbar bzw. inkonsistent ist.

Beth-Kalküle versuchen, die Gültigkeit eines Arguments zu widerlegen (auch deshalb „Widerlegungskalkül“), indem sie den Vorgang formalisieren, ein Modell für anzugeben. So sind die Formationsregeln des Kalküls rein syntaktisch und können ohne jeden semantischen Hintergedanken angewendet werden, sind aber, indem sie letztlich die Gegenmodellkonstruktion formalisieren, semantisch motiviert.

Modelle konstruieren Bearbeiten

Im ersten Schritt soll überlegt werden, wie man für die einzelnen Arten von Aussagen ein Modell bildet. Dabei soll eine aussagenlogische Sprache zugrunde gelegt werden, deren Junktoren folgende sind: (Negation), (Konjunktion), (Disjunktion, nichtausschließendes Oder) und (Konditional oder materiale Implikation). Die Negation verneint den Wahrheitswert eines Satzes; eine Konjunktion verbindet zwei Sätze zu einem neuen Satz, der genau dann wahr ist, wenn beide verbundenen Sätze wahr sind, und der andernfalls falsch ist; die Disjunktion verbindet zwei Sätze zu einem neuen Satz, der nur dann falsch ist, wenn beide verbundenen Sätze falsch sind, und der andernfalls wahr ist; und das Konditional verbindet zwei Sätze zu einem neuen Satz, der nur dann falsch ist, wenn der linke der beiden verbundenen Sätze wahr und der rechte falsch ist.

  • Am einfachsten lässt sich ein Modell für einen atomaren Satz konstruieren: Man setzt und hat in ein geeignetes Modell.
  • Nicht viel schwieriger ist es, ein Modell für zu konstruieren (dabei darf anstelle von auch ein beliebig komplexer zusammengesetzter Satz stehen): Man setzt und hat in ein geeignetes Modell.
  • Auch ein Modell für ist rasch erzeugt: Man setzt und hat per Wahrheitsdefinition der Konjunktion mit in ein Modell für .
  • Um ein Modell für zu erzeugen, gibt es drei Möglichkeiten: (a) Man setzt , (b) man setzt , oder (c) man macht beides.
  • Auch die Konstruktion eines Modells für lässt mehrere Möglichkeiten zu: (a) Man setzt ; (b) man setzt ; (c) man macht beides.

Nach diesen Möglichkeiten sind die Transformationsregeln des Beth-Kalküls modelliert.

Ein erster Blick auf den Kalkül Bearbeiten

Im Ausgang werden alle Sätze der Menge untereinander aufgeschrieben. Dies wird am Beispiel des Arguments gezeigt. Bei diesem Argument ist und ist , ist also . ist hier , also . Man schreibt somit:

a.
b.
c.

Die Reihenfolge ist, da es sich um eine Satzmenge handelt, gleichgültig. Diese Satzmenge wird als Knoten – als ein Knoten – eines Baums angesehen, deshalb die Umrahmung. Nun wird versucht, für diese Satzmenge ein Modell zu bilden, also jeden Satz dieser Menge wahr zu machen. Im Fall der Sätze b. und c. ist das einfach: Damit eine Interpretation ein Modell für b. ist, muss sein. Damit ein Modell für c. ist, muss sein. Damit hat man erste Informationen über .

Schwieriger ist es mit Satz a. Dieser Satz ist ein Konditional, es gibt also drei Möglichkeiten, ihn zu erfüllen: (a) , (b) und (c) beides. Man schreibt die Möglichkeiten (a) und (b) als Kinder des Baums auf; Möglichkeit (c) braucht man nicht gesondert anzuschreiben, weil sie die Kombination von (a) und (b) bedeutet. Um anzuzeigen, dass man Satz a. damit abgehandelt hat, wird er – je nach Geschmack – durchgestrichen, abgehakt oder ganz entfernt. Es entsteht in diesem Schritt folgender Baum:

a.
b.
c.
d.
e.

Dabei liest sich Knoten bzw. Satz d. wie folgt: „Zusätzlich zu den nicht durchgestrichenen Anforderungen, die meine Vorfahren an stellen, stelle ich an die Anforderung, dass .“ (Diese Anforderung resultierte aus der Behandlung von Satz a.)

Knoten bzw. Satz e. liest sich wie folgt: „Zusätzlich zu den nicht durchgestrichenen Anforderungen, die meine Vorfahren an stellen, stelle ich an die Anforderung, dass .“

Man sieht, dass Knoten d. eine unerfüllbare Anforderung an stellt: Der Knoten fordert auf Grund von Satz d., dass ist. Zugleich erbt er aber von seinem Vater auf Grund von Satz b. die Forderung, dass ist. Da diese beiden Forderungen nicht vereinbar sind, ist der linke Versuch, ein Modell für zu bilden, frühzeitig gescheitert. Man markiert das im Baum auf geeignete Weise:

a.
b.
c.
d.
e.

Man liest das als: „Der linke Zweig ist geschlossen“.

Der rechte Zweig ist noch offen und damit die Hoffnung, ein Modell zu finden, noch nicht verloren. Wann ist ein Modell für ? Auf Grund der Wahrheitswertdefinitionen der Konjunktion genau dann, wenn . Das schreibt man auf und streicht den damit abgehandelten Satz e.:

a.
b.
c.
d.
e.
f.
g.

Jetzt liest sich Knoten e. wie folgt: „Zusätzlich zu den Anforderungen, die mein Vater an richtet, fordere ich von , dass und dass .“

Der Weg, der von der Wurzel zu Knoten e. führt, enthält nur mehr atomare Sätze. Die Anforderungen an ein Modell von können daher direkt abgelesen werden: Damit ein solches Modell ist, muss es folgende Anforderungen erfüllen:

  1. aus b. I(P) = W
  2. aus c. I(Q) = F
  3. aus f. I(Q) = W
  4. aus g. I(R) = W

Forderungen b. und g. sind unproblematisch, aber Forderungen c. und f. widersprechen einander und sind daher unerfüllbar. Damit ist es auch im zweiten Ast des Baums nicht gelungen, ein Modell für zu bilden. Der Ast ist also ebenfalls geschlossen, sein Endknoten wird markiert:

a.
b.
c.
d.
e.
f.
g.

Da keine weiteren Äste mehr vorhanden und alle vorhandenen Äste geschlossen sind, wird der ganze Baum geschlossen genannt. Die Geschlossenheit des Baums zeigt an, dass es unmöglich ist, ein Modell für zu bilden. Das wiederum bedeutet, dass es unmöglich ist, das Argument zu widerlegen. Somit ist das Argument damit bewiesen.

Schlussregeln des aussagenlogischen Baumkalküls Bearbeiten

Diese Regeln müssen so lange auf den Baum angewendet werden, bis alle nichtatomaren Sätze durchgestrichen sind. Der entstandene Baum heißt genau dann geschlossen, wenn jeder direkte Weg von der Wurzel bis zu einem Endknoten mindestens einen Widerspruch enthält. Ein Weg enthält genau dann einen Widerspruch, wenn er sowohl einen Satz als auch dessen Negation enthält.

Ist der Baum nicht geschlossen, d. h. gibt es mindestens einen widerspruchsfreien direkten Weg von der Wurzel bis zu einem Endknoten, dann heißt der Baum offen.

Das Argument, für das der Baum gebildet wurde, ist genau dann gültig, wenn der Baum geschlossen ist. Das Argument ist genau dann ungültig, wenn der Baum offen ist. In diesem Fall lässt sich an jedem offenen Ast ein Gegenbeispiel für das Argument ablesen.

Der Beth-Kalkül für die klassische Aussagenlogik, so wie er hier aufgestellt wurde, ist korrekt und vollständig, und er ist ein Entscheidungsverfahren für die klassisch-aussagenlogische Gültigkeit von Argumenten.

Literatur Bearbeiten

  • Evert Willem Beth: Semantic Entailment and formal derivability. In: Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Band 18, Nummer 13, Amsterdam 1955, S. 309–342, gekürzter, übersetzter Nachdruck in Berka/Kreiser 1986, S. 262 ff.
  • Evert Willem Beth: A topological proof of the theorem of Löwenheim-Skolem-Gödel. In: Indag. Math., 13, S. 346–344
  • Karel Berka, Lothar Kreiser: Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik. Akademie, Berlin 1986

Sekundärliteratur Bearbeiten

  • Ansgar Beckermann: Einführung in die Logik. 3. Auflage. De Gruyter, Berlin 2010, ISBN 978-3-11-025434-1.
  • Wilfrid Hodges: Logic. 2. Auflage. Penguin, London 2001, ISBN 0-14-100314-6 (englisch)
  • Wolfgang Bibel: Deduktion. Automatisierung der Logik (=Handbuch der Informatik 6.2). Oldenbourg, München 1992, ISBN 3-486-20785-7

Weblinks Bearbeiten

wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Baumkalkule oder Tableaukalkule nach ihrem Erfinder auch Beth Kalkule genannt sind Widerlegungskalkule der Logik Der Name Baumkalkul ruhrt daher dass beim Ableiten in einem Beth Kalkul eine Baumstruktur erzeugt wird Diese Aussage ist eine Beschreibung keine Definition weil nicht jeder Kalkul der Baumstrukturen erzeugt auch Baumkalkul genannt wird Die entstandenen Baumstrukturen werden auch Beth Tableaux oder Beth Tableaus franzosischer bzw eingedeutschter Plural von Beth Tableau genannt Inhaltsverzeichnis 1 Grundlagen 2 Modelle konstruieren 3 Ein erster Blick auf den Kalkul 4 Schlussregeln des aussagenlogischen Baumkalkuls 5 Literatur 5 1 Sekundarliteratur 6 WeblinksGrundlagen BearbeitenFur klassische Logiken lasst sich intuitiv ein semantischer Schlussbegriff fassen Ein Argument ist genau dann gultig wenn unter allen Interpretationen unter denen alle Pramissen wahr sind auch die Konklusion wahr ist kurzer pragnanter und mit Leibniz Aus Wahrem folgt nur Wahres Somit ist ein Argument genau dann ungultig wenn es mindestens eine Interpretation gibt unter der alle Pramissen wahr sind die Konklusion aber falsch ist Wenn ein Satz falsch ist dann ist nach der klassischen Semantik seine Verneinung wahr Statt zu sagen ein Argument ist genau dann ungultig wenn es mindestens eine Interpretation gibt unter der alle Pramissen wahr sind unter der die Konklusion aber falsch ist kann man daher genauso gut folgendes sagen Ein Argument ist genau dann ungultig wenn es mindestens eine Interpretation gibt unter der alle Pramissen wahr sind und unter der auch die Negation der Konklusion wahr ist Kurzer Ein Argument G f displaystyle Gamma models varphi nbsp wobei G displaystyle Gamma nbsp die Menge der Pramissen f displaystyle varphi nbsp die Konklusion ist und das metalogische Zeichen displaystyle models nbsp die Gultigkeit des Arguments aussagt ist genau dann ungultig wenn es mindestens eine Interpretation I gibt unter der jeder Satz aus G displaystyle Gamma nbsp wahr ist unter der f displaystyle varphi nbsp aber falsch ist Da nach der Semantik der Negation I f displaystyle varphi nbsp F genau dann wenn I f displaystyle neg varphi nbsp W ist G f displaystyle Gamma models varphi nbsp genau dann ungultig wenn I nicht nur jeden Satz aus G displaystyle Gamma nbsp sondern auch f displaystyle neg varphi nbsp wahr macht wenn also I jeden Satz aus der Menge G f displaystyle Gamma cup neg varphi nbsp wahr macht Ein Argument G f displaystyle Gamma models varphi nbsp ist also genau dann ungultig wenn die Menge G f displaystyle Gamma cup neg varphi nbsp erfullbar ist und im Umkehrschluss genau dann gultig wenn die Menge G f displaystyle Gamma cup neg varphi nbsp unerfullbar bzw inkonsistent ist Beth Kalkule versuchen die Gultigkeit eines Arguments zu widerlegen auch deshalb Widerlegungskalkul indem sie den Vorgang formalisieren ein Modell fur G f displaystyle Gamma cup neg varphi nbsp anzugeben So sind die Formationsregeln des Kalkuls rein syntaktisch und konnen ohne jeden semantischen Hintergedanken angewendet werden sind aber indem sie letztlich die Gegenmodellkonstruktion formalisieren semantisch motiviert Modelle konstruieren BearbeitenIm ersten Schritt soll uberlegt werden wie man fur die einzelnen Arten von Aussagen ein Modell bildet Dabei soll eine aussagenlogische Sprache zugrunde gelegt werden deren Junktoren folgende sind displaystyle neg nbsp Negation displaystyle land nbsp Konjunktion displaystyle vee nbsp Disjunktion nichtausschliessendes Oder und displaystyle to nbsp Konditional oder materiale Implikation Die Negation verneint den Wahrheitswert eines Satzes eine Konjunktion verbindet zwei Satze zu einem neuen Satz der genau dann wahr ist wenn beide verbundenen Satze wahr sind und der andernfalls falsch ist die Disjunktion verbindet zwei Satze zu einem neuen Satz der nur dann falsch ist wenn beide verbundenen Satze falsch sind und der andernfalls wahr ist und das Konditional verbindet zwei Satze zu einem neuen Satz der nur dann falsch ist wenn der linke der beiden verbundenen Satze wahr und der rechte falsch ist Am einfachsten lasst sich ein Modell fur einen atomaren Satz P displaystyle P nbsp konstruieren Man setzt I P W displaystyle I P W nbsp und hat in I displaystyle I nbsp ein geeignetes Modell Nicht viel schwieriger ist es ein Modell fur P displaystyle neg P nbsp zu konstruieren dabei darf anstelle von P displaystyle P nbsp auch ein beliebig komplexer zusammengesetzter Satz stehen Man setzt I P F displaystyle I P F nbsp und hat in I displaystyle I nbsp ein geeignetes Modell Auch ein Modell fur P Q displaystyle P land Q nbsp ist rasch erzeugt Man setzt I P I Q W displaystyle I P I Q W nbsp und hat per Wahrheitsdefinition der Konjunktion mit I P Q W displaystyle I P land Q W nbsp in I displaystyle I nbsp ein Modell fur P Q displaystyle P land Q nbsp Um ein Modell fur P Q displaystyle P vee Q nbsp zu erzeugen gibt es drei Moglichkeiten a Man setzt I P W displaystyle I P W nbsp b man setzt I Q W displaystyle I Q W nbsp oder c man macht beides Auch die Konstruktion eines Modells fur P Q displaystyle P to Q nbsp lasst mehrere Moglichkeiten zu a Man setzt I P F displaystyle I P F nbsp b man setzt I Q W displaystyle I Q W nbsp c man macht beides Nach diesen Moglichkeiten sind die Transformationsregeln des Beth Kalkuls modelliert Ein erster Blick auf den Kalkul BearbeitenIm Ausgang werden alle Satze der Menge G f displaystyle Gamma cup neg varphi nbsp untereinander aufgeschrieben Dies wird am Beispiel des Arguments P Q R P Q displaystyle P rightarrow Q land R P models Q nbsp gezeigt Bei diesem Argument ist G P Q R P displaystyle Gamma P rightarrow Q land R P nbsp und ist f Q displaystyle varphi Q nbsp ist also f Q displaystyle neg varphi neg Q nbsp G f displaystyle Gamma cup neg varphi nbsp ist hier P Q R P Q displaystyle P rightarrow Q land R P cup neg Q nbsp also P Q R P Q displaystyle P rightarrow Q land R P neg Q nbsp Man schreibt somit a P Q R displaystyle P rightarrow Q land R nbsp b P displaystyle P nbsp c Q displaystyle neg Q nbsp Die Reihenfolge ist da es sich um eine Satzmenge handelt gleichgultig Diese Satzmenge wird als Knoten als ein Knoten eines Baums angesehen deshalb die Umrahmung Nun wird versucht fur diese Satzmenge ein Modell zu bilden also jeden Satz dieser Menge wahr zu machen Im Fall der Satze b und c ist das einfach Damit eine Interpretation I displaystyle I nbsp ein Modell fur b ist muss I P W displaystyle I P W nbsp sein Damit I displaystyle I nbsp ein Modell fur c ist muss I Q F displaystyle I Q F nbsp sein Damit hat man erste Informationen uber I displaystyle I nbsp Schwieriger ist es mit Satz a Dieser Satz ist ein Konditional es gibt also drei Moglichkeiten ihn zu erfullen a I P F displaystyle I P F nbsp b I Q R W displaystyle I Q land R W nbsp und c beides Man schreibt die Moglichkeiten a und b als Kinder des Baums auf Moglichkeit c braucht man nicht gesondert anzuschreiben weil sie die Kombination von a und b bedeutet Um anzuzeigen dass man Satz a damit abgehandelt hat wird er je nach Geschmack durchgestrichen abgehakt oder ganz entfernt Es entsteht in diesem Schritt folgender Baum a P Q R displaystyle P rightarrow Q land R nbsp b P displaystyle P nbsp c Q displaystyle neg Q nbsp d P displaystyle neg P nbsp e Q R displaystyle Q land R nbsp Dabei liest sich Knoten bzw Satz d wie folgt Zusatzlich zu den nicht durchgestrichenen Anforderungen die meine Vorfahren an I displaystyle I nbsp stellen stelle ich an I displaystyle I nbsp die Anforderung dass I P F displaystyle I P F nbsp Diese Anforderung resultierte aus der Behandlung von Satz a Knoten bzw Satz e liest sich wie folgt Zusatzlich zu den nicht durchgestrichenen Anforderungen die meine Vorfahren an I displaystyle I nbsp stellen stelle ich an I displaystyle I nbsp die Anforderung dass I Q R W displaystyle I Q land R W nbsp Man sieht dass Knoten d eine unerfullbare Anforderung an I displaystyle I nbsp stellt Der Knoten fordert auf Grund von Satz d dass I P F displaystyle I P F nbsp ist Zugleich erbt er aber von seinem Vater auf Grund von Satz b die Forderung dass I P W displaystyle I P W nbsp ist Da diese beiden Forderungen nicht vereinbar sind ist der linke Versuch ein Modell fur P Q R P Q displaystyle P rightarrow Q land R P neg Q nbsp zu bilden fruhzeitig gescheitert Man markiert das im Baum auf geeignete Weise a P Q R displaystyle P rightarrow Q land R nbsp b P displaystyle P nbsp c Q displaystyle neg Q nbsp d P displaystyle neg P nbsp e Q R displaystyle Q land R nbsp Man liest das als Der linke Zweig ist geschlossen Der rechte Zweig ist noch offen und damit die Hoffnung ein Modell zu finden noch nicht verloren Wann ist I displaystyle I nbsp ein Modell fur Q R displaystyle Q land R nbsp Auf Grund der Wahrheitswertdefinitionen der Konjunktion genau dann wenn I Q I R W displaystyle I Q I R W nbsp Das schreibt man auf und streicht den damit abgehandelten Satz e a P Q R displaystyle P rightarrow Q land R nbsp b P displaystyle P nbsp c Q displaystyle neg Q nbsp d P displaystyle neg P nbsp e Q R displaystyle Q land R nbsp f Q displaystyle Q nbsp g R displaystyle R nbsp Jetzt liest sich Knoten e wie folgt Zusatzlich zu den Anforderungen die mein Vater an I displaystyle I nbsp richtet fordere ich von I displaystyle I nbsp dass I Q W displaystyle I Q W nbsp und dass I R W displaystyle I R W nbsp Der Weg der von der Wurzel zu Knoten e fuhrt enthalt nur mehr atomare Satze Die Anforderungen an ein Modell von P Q R P Q displaystyle P rightarrow Q land R P neg Q nbsp konnen daher direkt abgelesen werden Damit I displaystyle I nbsp ein solches Modell ist muss es folgende Anforderungen erfullen aus b I P W aus c I Q F aus f I Q W aus g I R WForderungen b und g sind unproblematisch aber Forderungen c und f widersprechen einander und sind daher unerfullbar Damit ist es auch im zweiten Ast des Baums nicht gelungen ein Modell fur P Q R P Q displaystyle P rightarrow Q land R P neg Q nbsp zu bilden Der Ast ist also ebenfalls geschlossen sein Endknoten wird markiert a P Q R displaystyle P rightarrow Q land R nbsp b P displaystyle P nbsp c Q displaystyle neg Q nbsp d P displaystyle neg P nbsp e Q R displaystyle Q land R nbsp f Q displaystyle Q nbsp g R displaystyle R nbsp Da keine weiteren Aste mehr vorhanden und alle vorhandenen Aste geschlossen sind wird der ganze Baum geschlossen genannt Die Geschlossenheit des Baums zeigt an dass es unmoglich ist ein Modell fur P Q R P Q displaystyle P rightarrow Q land R P neg Q nbsp zu bilden Das wiederum bedeutet dass es unmoglich ist das Argument P Q R P Q displaystyle P rightarrow Q land R P models Q nbsp zu widerlegen Somit ist das Argument P Q R P Q displaystyle P rightarrow Q land R P models Q nbsp damit bewiesen Schlussregeln des aussagenlogischen Baumkalkuls BearbeitenUnd Regel Tritt in einem Knoten eine Aussage P Q displaystyle P land Q nbsp auf wird diese durchgestrichen und der Knoten wird um die beiden Satze P displaystyle P nbsp und Q displaystyle Q nbsp erweitert Oder Regel Tritt in einem Knoten eine Aussage P Q displaystyle P vee Q nbsp auf wird diese durchgestrichen und der Knoten erhalt zwei Kinder Eines der beiden Kinder enthalt den Satz P displaystyle P nbsp das andere Kind enthalt den Satz Q displaystyle Q nbsp Pfeil Regel Tritt in einem Knoten eine Aussage P Q displaystyle P to Q nbsp auf wird diese durchgestrichen und der Knoten erhalt zwei Kinder Eines der beiden Kinder enthalt den Satz P displaystyle neg P nbsp das andere Kind enthalt den Satz Q displaystyle Q nbsp Nicht Und Regel Tritt in einem Knoten eine Aussage P Q displaystyle neg P land Q nbsp auf wird diese durchgestrichen und der Knoten erhalt zwei Kinder Eines der beiden Kinder enthalt den Satz P displaystyle neg P nbsp das andere Kind enthalt den Satz Q displaystyle neg Q nbsp Nicht Oder Regel Tritt in einem Knoten eine Aussage P Q displaystyle neg P vee Q nbsp auf wird diese durchgestrichen und der Knoten wird um den Satz P displaystyle neg P nbsp und um den Satz Q displaystyle neg Q nbsp erweitert Nicht Pfeil Regel Tritt in einem Knoten eine Aussage P Q displaystyle neg P to Q nbsp auf wird diese durchgestrichen und der Knoten wird um den Satz P displaystyle P nbsp und um den Satz Q displaystyle neg Q nbsp erweitert Diese Regeln mussen so lange auf den Baum angewendet werden bis alle nichtatomaren Satze durchgestrichen sind Der entstandene Baum heisst genau dann geschlossen wenn jeder direkte Weg von der Wurzel bis zu einem Endknoten mindestens einen Widerspruch enthalt Ein Weg enthalt genau dann einen Widerspruch wenn er sowohl einen Satz P displaystyle P nbsp als auch dessen Negation P displaystyle neg P nbsp enthalt Ist der Baum nicht geschlossen d h gibt es mindestens einen widerspruchsfreien direkten Weg von der Wurzel bis zu einem Endknoten dann heisst der Baum offen Das Argument fur das der Baum gebildet wurde ist genau dann gultig wenn der Baum geschlossen ist Das Argument ist genau dann ungultig wenn der Baum offen ist In diesem Fall lasst sich an jedem offenen Ast ein Gegenbeispiel fur das Argument ablesen Der Beth Kalkul fur die klassische Aussagenlogik so wie er hier aufgestellt wurde ist korrekt und vollstandig und er ist ein Entscheidungsverfahren fur die klassisch aussagenlogische Gultigkeit von Argumenten Literatur BearbeitenEvert Willem Beth Semantic Entailment and formal derivability In Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen Band 18 Nummer 13 Amsterdam 1955 S 309 342 gekurzter ubersetzter Nachdruck in Berka Kreiser 1986 S 262 ff Erste systematische Ausarbeitung des Baumkalkuls Evert Willem Beth A topological proof of the theorem of Lowenheim Skolem Godel In Indag Math 13 S 346 344 Erste Gedanken in Richtung eines Baumkalkuls Karel Berka Lothar Kreiser Logik Texte Kommentierte Auswahl zur Geschichte der modernen Logik Akademie Berlin 1986 Gekurzter ubersetzter Nachdruck von Beth 1955 ab S 262Sekundarliteratur Bearbeiten Ansgar Beckermann Einfuhrung in die Logik 3 Auflage De Gruyter Berlin 2010 ISBN 978 3 11 025434 1 In dieser Einfuhrung wird ein Baumkalkul fur Aussagen und Pradikatenlogik von Grund auf und auf einem fur Anfanger verstandlichen Niveau entwickelt Wilfrid Hodges Logic 2 Auflage Penguin London 2001 ISBN 0 14 100314 6 englisch Ein sehr einfach beginnendes Einfuhrungsbuch in die formale Logik in dem langsam ein Baumkalkul entwickelt wird Fur Einsteiger in die formale Logik die der englischen Sprache machtig sind ware es eine ausgezeichnete Wahl Wolfgang Bibel Deduktion Automatisierung der Logik Handbuch der Informatik 6 2 Oldenbourg Munchen 1992 ISBN 3 486 20785 7 Der Titel steht stellvertretend fur Werke deren Zielsetzung innerhalb der Informatik und im automatisierten Beweisen liegt einer Zielsetzung bei der uberwiegend mit Widerlegungskalkulen gearbeitet wird Voraussetzung fur das fruchtbare Studium solcher Titel sind Vorkenntnisse auf dem Gebiet der formalen Logik und der Programmierung Weblinks BearbeitenTorsten Wilholt Logik und Argumentation PDF 2 7 MB Skript zur Einfuhrung in die formale Logik unter Verwendung eines Baumkalkuls fur Aussagen und Pradikatenlogik mit Identitat enthalt Beweise fur Korrektheit und Vollstandigkeit des Kalkuls Wolfgang Schwarz Tree Proof Generator JavaScript das fur logisch wahre Satze der Aussagen oder Pradikatenlogik Beweise im Baumkalkul generiert Abgerufen von https de wikipedia org w index php title Baumkalkul amp oldid 238718983