Semantisch tableau

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken
Grafische weergave van een semantisch tableau

Een semantisch tableau is 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 per definitie waar is, gegeven dat een aantal andere stelling waar is. Onder het kopje bewijs uit het ongerijmde wordt dit verder toegelicht. Het semantisch tableau is een schepping van de Nederlandse logicus Evert Willem Beth.

Semantische tableaus in de propositielogica[bewerken]

Een semantisch tableau kan in vele verschillende logica's 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  (A \or B) \and \neg(A \or C) waar is, dan begint men als volgt:

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

Dat deze stelling waar is betekent dat zowel  A \or B waar moet zijn, als \neg(A \or 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  A \or B is of A waar, of B. 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. Als \neg(A \or C) waar is, moet A \or C niet waar zijn. A \or 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

Om tenslotte A \or 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                       | 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 C die rechtsonder als onwaar staat niet in conflict met de C die in de linkertak als waar staat. De twee takken stellen immers verschillende situaties voor. De B die in de rechtertak als waar staat is echter wel 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) |
                         C ∨ B |
                            ¬B |
                               | B
                    ¬ (A ∨ D)  |
                   ____________|____________
                  |                         |
                C |                       B |
                  | A ∨ D                   | A ∨ D
                  | A                       | A
                  | D                       | C

De volgende tabel toont voor de vijf meest gebruikte connectieven (\and, \or, \rightarrow, \leftrightarrow, \neg) de manier om het te ontbinden in een semantisch tableau.

Connectief Waar Onwaar
A \and B
       |
A ∧ B |
       |
     A |
     B |
     |
     | A ∧ B
 ____|____ 
|A        |B
|         |
A \or B

       |
A ∨ B |
   ____|____
  A|      B|
   |       |
 |
 | A ∨ B
 |
 | A
 | B
A \rightarrow B
       |
A -> B |
   ____|____
  |A       B|  
  |         |
    | A -> B
    |
  A | B
A \leftrightarrow B
        |
A ←→ B |
    ____|____
  A|         |A
  B|         |B
      |
      | A ←→ B
  ____|____ 
A|B       B|A
\neg A
   |
 ~A|
   |
   |A
  |   
  | ~A  
 A|  
  |  

Bewijs uit het ongerijmde[bewerken]

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  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  (A \and B) \rightarrow C, D, \neg E \models \neg C te bewijzen:

                     (A ∧ B) -> C| ~C         
                                D|
                               ~E|
                                 |E                       
                                C|                       
                        _________|________                
                       |C            A ∧ B|      
                   gesloten tak          A|
                                         B| 
                                      open tak

Aangezien niet alle takken gesloten kunnen worden, is de stelling niet geldig. De situatie dat A, B, C en D waar zijn en E niet waar is een tegenvoorbeeld.

Semantische tableaus in de predicatenlogica[bewerken]

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

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

vervangen door

\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

\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

 \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:

 \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.

Literatuur[bewerken]

  • (en) E.W. Beth, The Foundations of mathematics. A study in the philosophy of science, Standaard-Boekhandel Amsterdam 1959
  • (en) E.W. Beth, Formal Methods, 1962
  • (en) E.W. Beth, Moderne logica, Van Gorcum Assen 1967