Senter for Marxistiske og Matematiske Studium, Enschede (SMMSE)

I førre teksten såg vi ein metode for å undersøkje om ei slutning er gyldig eller ikkje. Denne metoden vert ofte kalla for sanningstre. I denne teksten skal vi sjå eit dataprogram som hjelper deg i å lage sanningstrea. Programmet finn du her, og vi kan kalle programmet for ein slutningskalkulator.

Programmet har eit stort tekstfelt for å vise fram sanningstrea og eit mindre eit for å skrive inn slutningane vi vil undersøkje. Når vi skriv inn slutningar nyttar vi ei line per premiss, ei line for konklusjonsstreken og ei line for konklusjonen. Vi skriv # for "ikkje", / \ for "og", \ / for "eller" og -> for "viss-så". Konklusjonsstreken er ei line med minst fire bindestrekar ("----").

Lat oss nytte eksempla frå førre teksten. I det mindre tekstfeltet skriv vi:

#A -> B
-------
A \/ B

For å starte eit sanningstre trykkar vi på "Start". Programmet vil ta premissane og negasjonen av konklusjonen, skrive dei om til negasjons normalform og setje dei opp under kvarandre. Alle utsegnene i treet er nummererte og programmet vil fortelje oss kva for utsegner vi har å jobbe med for å byggje vidare på treet. Så om vi trykkar på "Start" vil vi i det store tekstfeltet sjå:

      1.1  (A \/ B)       
     ---------------      
     2.1  (#A /\ #B)      


Utsegner å jobbe med: 1.1  2.1  

Bak startknappen er det eit lite tekstfelt og ein knapp merkt "Steg". Om vi no vil gå vidare med øvste utsegna skriv vi "1.1" i dette feltet og trykkar på "Steg". Programmet vil no tekne opp det nye treet:

         1.1  (A \/ B) *   
         ---------------   
         2.1  (#A /\ #B)   
     -----------------------
     3.1  A           3.2  B


Utsegner å jobbe med: 2.1 

Vi går vidare med utsegn 2.1, og får:

           1.1  (A \/ B) *       
          -----------------      
          2.1  (#A /\ #B) *      
      ------------------------   
      3.1  A            3.2  B   
     -------           -------   
     4.1  #A           4.2  #A   
     -------           -------   
     5.1  #B           5.2  #B   
     -------           -------   
        X                 X      

Alle greiner er lukka, slutninga er gyldig!

No er vi ferdige, og kan gå laus på det andre eksempelet. Vi skriv inn

A \/ (B \/ C)
B -> C
-------------
C

og trykkar "Start". Programmet viser oss no:

     1.1  (A \/ (B \/ C))   
     --------------------   
        2.1  (#B \/ C)      
        --------------      
            3.1  #C         


Utsegner å jobbe med: 1.1  2.1  

Av di vi er late orkar vi ikkje utføre alle stega sjølv. Vi trykkar på "Automatisk" og programmet byggjer systematisk treet for oss til det ikkje er meir å gjere. (Programmet vil for kvart steg velje det lægste nummeret, men utsegner med "og" går alltid føre utsegner med "eller" for å gjere treet meir kompakt.) Resultatet vert:

                             1.1  (A \/ (B \/ C)) *                           
                             ----------------------                           
                                2.1  (#B \/ C) *                              
                                ----------------                              
                                     3.1  #C                                  
              -----------------------------------------------------           
              4.1  A                                4.2  (B \/ C) *           
     ------------------------                -----------------------------    
     5.1  #B           5.2  C                5.3  #B                5.4  C    
                       ------        -----------------------        ------    
                         X           6.1  B           6.2  C          X       
                                     ------           ------                  
                                       X                X                     

Moteksempel funne: A=SANN  B=USANN  C=USANN

Det er ikkje meir å jobbe med.

Som vi kan sjå er det ikkje meir å gjere, og programmet har funni eit moteksempel.

Heilt til slutt, litt om parentesar. For at vi skal sleppe å skrive så mykje parentesar når vi skriv inn store samansette utsegner har programmet ein konvensjon for parentesbruk. Vi seier at "ikkje" bind sterkare enn "og", "og" bind sterkare enn "eller" og "eller" bind sterkare enn "viss-så", på same måte som "gange" bind sterkare enn "pluss" i vanleg aritmetikk. Det vil seie at om vi skriv inn

A -> B \/ C /\ D

vil programmet tolke dette som

A -> (B \/ (C /\ D))

Som du kanskje har lagt merke til har vi allereie nytta at "ikkje" bind sterkast, men utan at vi har sagt noko om det. Vidare bind symbol av same type sterkare frå venstre mot høgre, så om vi skriv inn

A -> B -> C

vil det verte tolka som

(A -> B) -> C

Som du òg kanskje har sett vil programmet sjølv ikkje nytte desse konvensjonane når det skriv utsegner, men nytte alle parentesane.