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.

I teksten som omhandla lur bruk av logikkpianoet til Jevons såg vi korleis vi kunne undersøkje gyldigheita til ei slutning ved å leite etter moteksempel. Om vi har ei slutning frå P₁, P₂, ..., P_n til K, vil alle utsegner M som er konsistente med mengda {P₁, P₂, ..., P_n, ¬K} representere eit moteksempel til slutninga (vi finn moteksempelet ved å gjere M sann). Om vi ikkje kan finne nokon sånn M, er slutninga gyldig.

Det vi skal gjere no er å sjå på ein enkel metode for å undersøkje slutningar etter same prinsippet; gjevi ei slutning, systematisk leite etter moteksempel. Metoden vi skal sjå på kallest gjerne for tremetoden eller sanningstre, og vi skal nytte ein forenkla versjon av metoden sånn Jeffrey presenterer han. Forenklinga går ut på at vi skal late alle utsegnene vere på ei form som kan kallast negasjons normalform (som er enklare enn den disjunktive normalforma vi nytta i førre teksten).

I negasjons normalform er ei utsegn bygd opp av berre "og" (∧), "eller" (∨) og "ikkje" (¬), og "ikkje" står alltid inst. Det vil seie at "ikkje" alltid står rett føre ei grunnutsegn. Ved hjelp av fire reglar kan alle utsegner skrivast om til negasjons normalform:

1. ¬¬P = P
2. P → Q = ¬P ∨ Q
3. ¬(P ∧ Q) = ¬P ∨ ¬Q
4. ¬(P ∨ Q) = ¬P ∧ ¬Q

Lat oss sjå korleis vi kan gå fram med utsegna (A ∧ (A → B)) → B (i kolonnen til høgre står nummeret på regelen vi nyttar for kvart steg):

(A ∧ (A → B)) → B	2.
¬(A ∧ (A → B)) ∨ B	3.
(¬A ∨ ¬(A → B)) ∨ B	2.
(¬A ∨ ¬(¬A ∨ B)) ∨ B	4.
(¬A ∨ (¬¬A ∧ ¬B)) ∨ B	1.
(¬A ∨ (A ∧ ¬B)) ∨ B	.

No kan vi gå laus på sanningstrea. I rota på eit sanningstre har vi ei mengd utsegner vi ønskjer å gjere sanne på ein gong (premissane og negasjonen av konklusjonen til slutninga vi vil undersøkje), og så byggjer vi eit tre kor kvar grein er eit forsøk på å finne ein måte å gjere alle utsegnene sanne på. Måten vi gjer det på er som følgjer: Fyrst finn vi ei utsegn som ikkje er ein literal. Om ho er på forma P ∧ Q vert ho sann om både P og Q er sanne, så vi vil freiste å gjere P og Q sanne i standen for. Vi merkjer av P ∧ Q som ferdig og skriv opp P og Q under kvarandre i kvar grein som leier frå P ∧ Q. Vi kan setje dette opp som ein regel:

     P ∧ Q *
       P
       Q

Om utsegna er på forma P ∨ Q får vi ei forgreining; éi grein kor vi freistar gjere P sann og éi grein kor vi freistar gjere Q sann. (Det finst to måtar å gjere P ∨ Q sann på, men berre ein måte å gjere P ∧ Q sann.) Denne regelen kan sjå slik ut

     P ∨ Q *
     /    \ .
    P      Q

Vi må hugse å forgreine alle greiene som leier frå utsegna. No kan vi finne ei ny utsegn og gjere det same med ho, men berre om ho ikkje er merkt som ferdig.

Det fine no er at om vi har ei grunnutsegn (til dømes A) og negasjonen av denne grunnutsegna (¬A) ein eller annan stad i same grein, er det ikkje mogleg å gjere alle utsegnene i greina sanne til same tid (av di det ikkje er mogleg å gjere A og ¬A sanne til same tid.) Ei sånn grein kallar vi lukka, og kryssar ho av som ferdig:

     A     ¬A
    ¬A      A
     X      X

Ei grein som ikkje er lukka kallar vi open. Om vi har nytta (og merkt) alle utsegnene i ei grein og ho framleis er open har vi funni ein måte å gjere alle utsegnene i greina sanne på ein gong. Denne finn vi ved å gjere alle literalane i greina sanne. Og sidan dei utsegnene vi starta med er starten på alle greinene i treet har vi funni ein måte å gjere dei sanne på òg. Så om utsegnene vi starta med var ei mengd premissar og negasjonen av ein konklusjon, har vi faktisk funni eit moteksempel til slutninga.

På tide med eksempel. Lat oss undersøkje slutninga

¬A → B A ∨ B

Fyrst finn vi negasjons normalform av ¬A → B og ¬(A ∨ B) og set dei opp under kvarandre:

      A ∨ B
     ¬A ∧ ¬B

Lat oss byrje med øvste utsegna, og nytte "eller"-regelen på ho. Då får vi

      A ∨ B *
     ¬A ∧ ¬B
     /     \ .
    A       B 

Når vi no nyttar "og"-regelen på utsegn nummer to må vi hugse at vi skal fortsette på alle greinene:

      A ∨ B *
     ¬A ∧ ¬B *
     /     \ .
    A       B
   ¬A      ¬A
   ¬B      ¬B
    X       X

Vi ser no at greina til venstre inneheld både A og ¬A, og greina til høgre inneheld både B og ¬B, så båe greinene lukkar seg og utsegna er gyldig.

Lat oss no freiste noko større:

A ∨ (B ∨ C) B → C C

Sjå om du kan følgje med på kva som skjer

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

⇒

A ∨ (B ∨ C) * ¬B ∨ C __ ¬C __ / \ . A B ∨ C

⇒

A ∨ (B ∨ C) * ¬B ∨ C * __ ¬C __ / \ . A B ∨ C / \ / \. ¬B C ¬B C X X

⇒

A ∨ (B ∨ C) * ¬B ∨ C * __ ¬C __ / \ . A B ∨ C * / \ / \. ¬B C ¬B C X / \ X B C X X

No har vi ei open grein, utan fleire utsegner å jobbe med, og det gjev oss eit moteksempel. For å finne moteksempelet samlar vi saman literalane i greina, nemleg A, ¬B og ¬C, og gjer desse sanne. Vi får då A = S, B = U og C = U. (Du kan no skjekke at om vi set dette inn i slutninga finn vi at alle premissane er sanne medan konklusjonen er usann.)

Kva er motivasjonen for å vise dette? I ein seinare tekst skal vi presentere eit dataprogram for å undersøkje slutningar ved hjelp av denne metoden, og dette dataprogrammet skal vi nytte som eksempel i diskusjonen av logikkmaskina Jevons bygde.

Kjelder

Richard Jeffrey. Formal logic, its scope and limits, tredje utgåve, McGraw-Hill, 1991.

Herman Ruge Jervell. Forelesninger i logikk. Universitetet i Oslo, 1993.