Senter for Marxistiske og Matematiske Studium, Enschede (SMMSE)

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.