WikiDer > Semantisches Tableau

Grafische Darstellung eines semantischen Tableaus

EIN semantisches Tableau ist eine grafische Darstellung einer Möglichkeit, in die Logik systematisch das Verhalten einer logischen Aussage oder Formel untersuchen. Semantische Tableaus werden hauptsächlich verwendet, um zu untersuchen, ob eine Aussage aus einer Reihe anderer Aussagen folgt, dh ob eine Aussage wahr ist, wenn eine Reihe anderer Aussagen wahr sind. Das semantische Tableau ist eine Kreation des niederländischen Logikers Evert Willem Beth.

Semantische Tableaus in der Aussagenlogik

Ein semantisches Tableau kann in vielen verschiedenen Logiktypen verwendet werden. Die Grundlage des semantischen Tableaus liegt in der Aussagelogik.Ein semantisches Tableau beginnt mit einer Zeile. Alles links von der Linie ist wahr, alles rechts von der Linie ist falsch. Falls es notwendig ist zu untersuchen, was es für die Variablen A, B und C bedeutet, wenn ${Anzeigestil (Alor B)land zB (Alor C)}$ stimmt, man fängt so an:

Dass diese Aussage wahr ist, bedeutet, dass beide Daten ${displaystyle Alor B}$ muss wahr sein, wenn ${Anzeigestil zB (Alor C)}$. Diese beiden Aussagen stehen also auf der linken Seite der Zeile:

Diese beiden Aussagen werden jeweils weiter untersucht. wenn ${displaystyle Alor B}$ ist wahr, A ist wahr oder B ist wahr. Dies sind zwei unterschiedliche Situationen, die jeweils separat untersucht werden müssen. Um dies zu erreichen, wird das Tableau geteilt:

Die restlichen Teile der Position müssen nun für beide Zweige geprüft werden.

wenn ${Anzeigestil zB (Alor C)}$ ist wahr, muss ${displaystyle Alor C}$ nicht wahr sein. ${displaystyle Alor C}$ es wird also auf der rechten Seite der Linie sein.

Endlich ${displaystyle Alor C}$ unwahr A und C müssen beide falsch sein.

Der linke Ast zeigt einen Widerspruch. A steht auf beiden Seiten der Linie, kann aber nicht gleichzeitig wahr und falsch sein. Dieser Zweig liefert also ein Gegenbeispiel für die Aussage, denn A ist wahr und C ist falsch, die Aussage ist falsch. Der rechte Zweig hat keine Widersprüche und zeigt eine Situation, in der die Aussage wahr ist, denn B ist wahr, A ist falsch und C ist falsch, die Aussage ist wahr.

Es ist wichtig zu beachten, dass ein Widerspruch nur dann auftritt, wenn sich auf beiden Seiten der Linie Variablen im selben Zweig befinden. In der folgenden Tabelle steht das B, das im rechten Zweig wahr ist, in Konflikt mit dem B, das im Hauptzweig falsch ist. Alles oberhalb der Aufteilung gilt für beide Zweige.

Überblick

Die folgende Übersicht zeigt für die fünf am häufigsten verwendeten Konnektive (¬ ,∧ ,∨ , → ,↔) der Weg in ein semantisches Tableau zu faktorisieren.

Beweise aus dem Absurden

Siehe auch: Reduktion ad absurdum

Im Allgemeinen werden semantische Tableaus verwendet, um zu beweisen, dass eine Aussage wahr sein muss, vorausgesetzt, dass eine Reihe anderer Aussagen wahr sind. Dies wird als ${Anzeigestil A,B,CModelle D}$. Es heißt: A, B, C impliziert D. A, B und C sind hier die Prämissen und D ist die Konklusion. Um dies mit semantischen Tableaus zu beweisen, wird ein Widerspruchsbeweis gesucht. Die Prämissen werden links vom Bindestrich geschrieben (und daher als wahr angenommen) und die Schlussfolgerung wird rechts vom Bindestrich geschrieben (und daher als falsch angenommen).

Beim Ausschreiben des Tableaus wird nun nach einer Verzweigung gesucht, die keinen Widerspruch ergibt, d. h. wo auf beiden Seiten der Linie keine Variable vorkommt. Bei Kombination von Variablen in diesem Zweig ist die Konklusion, dh die Konklusion folgt nicht aus den Prämissen. Ein solcher Zweig, der keinen Widerspruch hervorruft, heißt a Öffnen branch.Wenn alle Zweige Widersprüche ergeben (Schließen), dann ist bewiesen, dass die Schlussfolgerung aus den Prämissen folgt, unabhängig von den Werten der Variablen.

Das folgende semantische Tableau versucht den Satz ${displaystyle (Aland B)ightarrow C,Amodels zB C}$ beweisen:

(A ∧ B) → C	C
ein
C
		C				A B
geschlossene Filiale
				ein				B
		geschlossene Filiale		Filiale öffnen

Da nicht alle Zweige geschlossen werden können, ist die Anweisung ungültig. Ein Zählermodell kann aus dem offenen Zweig gelesen werden: if ${Anzeigestil A}$ und ${Anzeigestil C}$ wo sind aber ${Anzeigestil B}$ nicht, dann sind ${displaystyle (Aland B)ightarrow C}$ und ${Anzeigestil A}$ stimmt, aber ${Anzeigestil zB C}$ nicht.

Semantische Tableaus in der Prädikatenlogik

Auch in der Prädikatslogik ein semantisches Tableau kann verwendet werden, um eine Implikation zu beweisen. Dazu muss zuerst die Formel eingegeben werden Pränex-Normalform verwandelt werden. Dann geht es darum existenzielle Quantoren verlieren. Dafür, Skolemisierung verwendet ein Verfahren, das ungefähr so ​​funktioniert: Alle Variablen, die existentiell quantifiziert sind, müssen durch eine eindeutige, neue Variable ersetzt werden. Damit wird die Formel

${displaystyle existiert y({mathit {Cat}}(y)country {mathit {Gray}}(y))}$

wird ersetzt durch

${displaystyle {mathit {Cat}}(d)Land {mathit {Gray}}(d)}$,

wo die Konstante d wurde in den Prämissen oder Schlussfolgerungen noch nicht verwendet In einigen Formeln funktioniert diese Methode nicht einwandfrei. Auf die Formel angewendet

${displaystyle forall xexists y({mathit {Mensch(x)}}ightarrow {mathit {FatherOf}}(y,x))}$ (für jeden Menschen x gibt es einen Vater y von x)

ist das ergebnis

${displaystyle forall x({mathit {Mensch}}(x)country {mathit {FatherOf}}(d,x))}$,

was darauf hindeutet d ist der Vater eines jeden Mannes. Um dies zu lösen, anstelle der Konstanten d Eine Funktion Vater(x) eingegeben werden:

${displaystyle forall x{mathit {Mensch}}(x)country {mathit {FatherOf}}({mathit {Vater}}(x),x))}$.

Wenn die existenziellen Quantoren entfernt werden, universelle Quantoren weggelassen (dies ist nicht notwendig, aber der Übersicht zuträglich) und das Tableau kann ausgeschrieben werden.

Literatur

• (und) E. W. Beth, Die Grundlagen der Mathematik. Ein Studium der Wissenschaftsphilosophie, Standaard-Buchhandlung Amsterdam 1959
• (und) E. W. Beth, Formale Methoden, 1962
• (und) E. W. Beth, Moderne Logik, Van Gorcum Assen 1967