Semantisch tableau

Een semantisch tableau is een grafische weergave van een manier om in de logica op systematische wijze het gedrag van een logische stelling of formule te onderzoeken. Semantische tableaus worden vooral gebruikt om te onderzoeken of een stelling volgt uit een reeks andere stellingen, dat wil zeggen of een stelling waar is, gegeven dat een aantal andere stellingen waar zijn. Het semantisch tableau is een schepping van de Nederlandse logicus Evert Willem Beth.^[1]

Een semantisch tableau kan in vele verschillende soorten logica gebruikt worden. De basis van het semantisch tableau ligt in de propositielogica. Een semantisch tableau begint met een lijn. Alles wat links van de lijn staat is waar, alles wat rechts van de lijn staat is onwaar. Als onderzocht moet worden wat het betekent voor de variabelen A, B en C als ${\displaystyle (A\lor B)\land \neg (A\lor C)}$ waar is, begint men als volgt:

(A ∨ B) ∧ ¬ (A ∨ C)

Dat deze stelling waar is betekent dat zowel ${\displaystyle A\lor B}$ waar moet zijn, als ${\displaystyle \neg (A\lor C)}$. Deze twee stellingen komen dus aan de linkerkant van de lijn te staan:

(A ∨ B) ∧ ¬ (A ∨ C)
A ∨ B
¬ (A ∨ C)

Deze twee stellingen worden ieder verder onderzocht. Als ${\displaystyle A\lor B}$ waar is, is A waar of B waar. Dit zijn twee verschillende situaties, die ieder apart onderzocht moeten worden. Om dit te bereiken wordt het tableau gesplitst:

(A ∨ B) ∧ ¬ (A ∨ C)
A ∨ B
¬ (A ∨ C)
A		B

De overgebleven delen van de stelling moeten nu voor beide takken onderzocht worden.

(A ∨ B) ∧ ¬ (A ∨ C)
A ∨ B
¬ (A ∨ C)
A		B
¬ (A ∨ C)		¬ (A ∨ C)

Als ${\displaystyle \neg (A\lor C)}$ waar is, moet ${\displaystyle A\lor C}$ niet waar zijn. ${\displaystyle A\lor C}$ komt dus aan de rechterkant van de lijn te staan.

(A ∨ B) ∧ ¬ (A ∨ C)
A ∨ B
¬ (A ∨ C)
A		B
¬ (A ∨ C)		¬ (A ∨ C)
		A ∨ C				A ∨ C

Om ten slotte ${\displaystyle A\lor C}$ niet waar te maken moeten A en C allebei niet waar zijn.

(A ∨ B) ∧ ¬ (A ∨ C)
A ∨ B
¬ (A ∨ C)
A		B
¬ (A ∨ C)		¬ (A ∨ C)
		A ∨ C				A ∨ C
		A				A
		C				C

De linkertak toont een contradictie. A staat aan beide kanten van de lijn, maar kan niet tegelijk waar en onwaar zijn. Die tak levert dus een tegenvoorbeeld op van de stelling, voor A is waar, en C is onwaar is de stelling onwaar. De rechtertak heeft geen contradicties, en toont een situatie waarvoor de stelling waar is, voor B is waar, A is onwaar en C is onwaar is de stelling waar.

Het is van belang op te merken dat er alleen een contradictie optreedt als er variabelen in dezelfde tak aan weerszijden van de lijn staan. In het onderstaande tableau is de B die in de rechtertak als waar staat in conflict met de B die in de hoofdtak als onwaar staat. Alles wat boven de splitsing staat geldt voor beide takken.

¬B ∧ (C ∨ B) ∧ ¬ (A ∨ D)
¬B
				B
C ∨ B
¬ (A ∨ D)
C		B
¬ (A ∨ D)	¬ (A ∨ D)
	A ∨ D			A ∨ D
	A			A
	D			D

Het volgende overzicht toont voor de vijf meest gebruikte connectieven ${\displaystyle (\lnot ,\land ,\lor ,\to ,\leftrightarrow )}$ de manier om ontbonden te worden in een semantisch tableau.

A

¬A

A

A ∧ B

¬(A ∧ B)

A

A ∧ B

B

A

B

A ∨ B

¬(A ∨ B)

A ∨ B

A

B

A

B

A → B

¬(A → B)

A → B

A

B

A

B

A ${\displaystyle \leftrightarrow }$ B

¬(A ${\displaystyle \leftrightarrow }$ B)

A ${\displaystyle \leftrightarrow }$ B

A

A

A

B

B

A

B

B

Zie ook: reductio ad absurdum

Over het algemeen worden semantische tableaus gebruikt om te bewijzen dat een stelling waar moet zijn, gegeven dat een aantal andere stellingen waar is. Dit wordt genoteerd als ${\displaystyle A,B,C\models D}$. Gezegd wordt: A, B, C impliceert D. A, B en C zijn hierin de premissen en D is de conclusie. Om dit te bewijzen met semantische tableaus wordt een bewijs uit het ongerijmde gezocht. De premissen worden aan de linkerkant van de streep geschreven (en dus waar verondersteld) en de conclusie wordt aan de rechterkant van de streep geschreven (en dus onwaar verondersteld).

Bij het uitschrijven van het tableau wordt nu gezocht naar een tak die geen contradictie oplevert, waar dus geen variabele aan beide kanten van de lijn voorkomt. Voor combinatie van variabelen in deze tak is de conclusie, dat wil zeggen dat de conclusie niet zonder meer volgt uit de premissen. Een dergelijke tak, die geen contradictie oplevert heet een open tak. Als alle takken contradicties opleveren (sluiten), dan is bewezen dat de conclusie volgt uit de premissen, ongeacht de waarden van de variabelen.

Het volgend semantisch tableau tracht de stelling ${\displaystyle (A\land B)\rightarrow C,A\models \neg C}$ te bewijzen:

(A ∧ B) → C	¬C
A
C
		C				A ∧ B
gesloten tak
				A				B
		gesloten tak		open tak

Aangezien niet alle takken gesloten kunnen worden, is de stelling niet geldig. Uit de open tak kan een tegenmodel worden afgelezen: als ${\displaystyle A}$ en ${\displaystyle C}$ waar zijn maar ${\displaystyle B}$ niet, dan zijn ${\displaystyle (A\land B)\rightarrow C}$ en ${\displaystyle A}$ waar, maar ${\displaystyle \neg C}$ niet.

Ook in de predicatenlogica kan een semantisch tableau gebruikt worden om een implicatie te bewijzen. Daarvoor moet de formule eerst in prenex-normaalvorm worden omgevormd. Vervolgens is het zaak de existentiële kwantoren kwijt te raken. Hiervoor wordt skolemisatie gebruikt, een proces dat ongeveer als volgt werkt: Alle variabelen die existentieel gekwantificeerd zijn moeten vervangen worden door een unieke, nieuwe variabele. Zo wordt de formule

${\displaystyle \exists y({\mathit {Kat}}(y)\land {\mathit {Grijs}}(y))}$

vervangen door

${\displaystyle {\mathit {Kat}}(d)\land {\mathit {Grijs}}(d)}$,

waarbij de constante d nog niet gebruikt werd in de premissen of de conclusie. In sommige formules werkt deze methode niet vlekkeloos. Toegepast op de formule

${\displaystyle \forall x\exists y({\mathit {Mens(x)}}\rightarrow {\mathit {VaderVan}}(y,x))}$ (voor ieder mens x, bestaat er een vader y van x)

is het resultaat

${\displaystyle \forall x({\mathit {Mens}}(x)\land {\mathit {VaderVan}}(d,x))}$,

wat suggereert dat d de vader van ieder mens is. Om dit op te lossen moet in plaats van de constante d een functie Vader(x) ingevoerd worden:

${\displaystyle \forall x{\mathit {Mens}}(x)\land {\mathit {VaderVan}}({\mathit {Vader}}(x),x))}$.

Als de existentiële kwantoren verwijderd zijn, kunnen de universele kwantoren weggelaten worden (dit hoeft niet, maar komt het overzicht ten goede) en kan het tableau uitgeschreven worden.

• (en) Beth, E.W. (1955). Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde 18 (13): 309–342. Herdrukt in Intikka, Jaakko (1969). The Philosophy of Mathematics. Oxford University Press, Amsterdam.
• (en) Beth, E.W. (1959). The Foundations of mathematics. A study in the philosophy of science. Standaard-Boekhandel, Amsterdam.
• (en) Beth, E.W. (19621962). Formal Methods.
• Beth, E.W. (1967). Moderne logica. Van Gorcum, Assen.
• (en) Fitting, Melvin (1996). First-order logic and automated theorem proving, 2nd. Springer, New York. DOI:10.1007/978-1-4612-2360-3 [1990]. ISBN 978-1-4612-7515-2.