Senter for Marxistiske og Matematiske Studium, Enschede (SMMSE)

Det er ikkje så ofte Enschede er omtalt i norske medium, så vi rettar merksemda mot ei lita melding.

Her på senteret er vi vane med snø og kom oss greitt gjennom helga, sjølv om eit middagsbesøk måtte utsetjast frå fredag til sundag.

I del II av teksten om logikkmaskina Jevons bygde hevda vi at ho ikkje gjev oss svar på dei problema vi er interesserte i. Som regel er gyldigheita til ei gjevi utsegn eller slutning det vi ønskje å undersøkje, ikkje kva som er dei moglege konklusjonane frå ei mengd premissar. Men at logikkmaskina ikkje kan hjelpe oss med dei interessante problema er ei sanning med modifikasjonar. I denne teksten skal vi sjå på korleis vi kan løyse dei problema vi er interesserte i ved å nytte logikkmaskina til Jevons på ein lur måte.

Vi hugsar at ei (gyldig) slutning er ei mengd premissar og ein konklusjon sånn at kvar gong alle premissane er sanne til same tid må òg konklusjonen sann. (Sidan ei utsegn er gyldig (alltid sann) om ho kan sluttast frå null premissar, skal vi halde oss til slutningar.) Vi skal kalle premissane for P₁, P₂,…,P_n og konklusjonen for K, og skrive ei slutning slik:

P1 P2 · · · Pn K

Kva skjer så om slutning ikkje er gyldig? Då finst det ein måte å gjere alle premissane sanne til same tid som samtidig gjer konklusjonen usann. Dette kallar vi eit moteksempel. Ta til dømes slutninga

A → B B A

Om vi set A = U and B = S ser vi at båe premissane vert sanne, medan konklusjonen vert usann. Vi har funni eit moteksempel, så slutninga kan ikkje vere gyldig. Så det vi skal gjere er å leite etter moteksempel til ei slutning, og om vi ikkje kan finne nokre tyder det at slutninga er gyldig. Enkelt og greitt, no treng vi berre ein måte å leite etter moteksempel på.

Vi hugsar at Jenons sitt logikkpiano gjev oss utsegner om er konsistente med ei mengd premissar, og det skal vi utnytte no. Tenk no at eit moteksempel gjer alle premissane sanne og konklusjonen usann; det er det same som å seie at det gjer alle premissane sanne og det motsette av konklusjonen (negasjonen av konklusjonen) sann til same tid. Tenk vidare at eit moteksempel kan uttrykkjast som ei utsegn. Moteksempelet over kan uttrykkjast som ¬A ∧ B. Det vil seie at vi finn igjen moteksempelet ved å gjere utsegna ¬A ∧ B sann.

No ser du sikkert kor vi vil hen. Lat oss seie vi har ei slutning frå P₁, P₂,…, P_n til K, og vi har funni eit moteksempel som vi kan representere med utsegna M. Sidan moteksempelet representert av M gjer premissane og negasjonen av konklusjonen sann, er M konsistent med mengda {P₁, P₂,…, P_n, ¬K} (det er mogleg å gjere P₁, P₂,…, P_n, ¬K og M sanne på ein gong)! Alt vi treng å gjere er å skrive inn mengda {P₁, P₂,…, P_n, ¬K}, og alle utsegnene vi får tilbake er moteksempel. Om vi ikkje får nokre utsegner tilbake tyder det at det ikkje finst nokre moteksempel og slutninga er gyldig.

Lat oss ta eit par eksempel. Fyrst eksempelet over. Vi skriv inn A → B, B og ¬A, og får tilbake

¬A ∧ B ∧ C ∧ D
¬A ∧ B ∧ C ∧ ¬D
¬A ∧ B ∧ ¬C ∧ D
¬A ∧ B ∧ ¬C ∧ ¬D

Med andre ord har vi A = U, B = S, og kva som helst for C og D som moteksempel, akkurat som vi hadde over. Lat oss no freiste slutninga

¬A → ¬B B A

No skriv vi ¬A → ¬B, B og ¬A, og denne gongen får vi inga utsegner tilbake. Vi veit då at slutninga er gyldig.

Dette er vel og bra. No vil vi sjå om (A ∧ (A → B)) → B er ei gyldig utsegn. Då treng vi berre å skrive ¬((A ∧ (A → B)) → B) på pianoet. Men det er ikkje berre berre, for utsegna er på feil form og kan ikkje skrivast inn. Kva skal vi då gjere? Det finst ei rekkje regler vi kan nytte til å skrive om utsegna til den ønskte forma. I tabellen under kan du sjå korleis vi gjer dette, med utsegna til venstre og reglane vi nyttar til høgre. (For å overtyde deg sjølv om at reglane stemmer kan du setje opp ein sanningstabell for kvar av dei.)

¬((A ∧ (A → B)) → B)	P → Q = ¬P ∨ Q
¬((A ∧ (¬A ∨ B)) → B)	P → Q = ¬P ∨ Q
¬(¬(A ∧ (¬A ∨ B)) ∨ B)	¬(P ∨ Q) = ¬P ∧ ¬Q
¬¬(A ∧ (¬A ∨ B)) ∧ ¬B	¬¬P = P
(A ∧ (¬A ∨ B)) ∧ ¬B	P ∧ (Q ∨ R) = (P ∧ Q) ∨ (P ∧ R)
((A ∧ ¬A) ∨ (A ∧ B)) ∧ ¬B	(P ∨ Q) ∧ R = (P ∧ R) ∨ (Q ∧ R)
((A ∧ ¬A) ∧ ¬B) ∨ ((A ∧ B) ∧ ¬B)	(P ∧ Q) ∧ R = P ∧ Q ∧ R
(A ∧ ¬A ∧ ¬B) ∨ (A ∧ B ∧ ¬B)	.

No, (A ∧ ¬A ∧ ¬B) ∨ (A ∧ B ∧ ¬B) kan vi skrive på pianoet. (Gjer det og sjå kva som skjer.) Denne forma kallest for disjunktiv normalform. Med bruk av desse og nokre reglar til kan faktisk alle utsegner skrivast om til disjunktiv normalform, så med pianoet kan vi skjekke alle utsegner (med inntil fire grunnutsegner) på denne måten.

Nytta så Jevons pianoet sitt på den måten? Det er vel lite truleg. For det fyrste ser vi at det kan vere ganske mykje jobb å skrive ei utsegn om til disjunktiv normalform, såpass mykje at vi like gjerne kunne gått rett på problemet. For det andre har vi sett at om ei utsegn er på disjunktiv normalform nyttar vi berre tangentane på høgresida av pianoet og då har Cop.IS-tangenten (for implikasjon) inga funksjon. Så viss dette var måten å nytte pianoet på kunne Jevons ha lage ein, om ikkje mykje enklare, så i alle høve mindre konstruksjon.

I ein seinare tekst skal vi sjå korleis ein kan nytte dei same prinsippa til å lage ein enkel utsegnskalkyle som er lett å mekanisere.

I del I såg vi på korleis ein opererer logikkmaskina som William Stanley Jevons bygde i 1869. Maskina finst no ved Museum of the History of Science, University of Oxford. Om du vil sjå bilete av ho kan du gå hit og søkje etter "jevons". For oss er det no på tide å ta ein titt inni maskina.

Som vi såg vil pianoet (som det ofte vert kalla) vise alle dei utsegnslogiske formlane på forma

A ∧ B ∧ C ∧ D

(kor A er anten A eller ¬A, osb., og A, B, C og D er grunnutsegner) som er konsistente med premissane ein skriv inn. Kvar av desse formlane er inni maskina representert av ein stav som kan verte flytta opp og ned. Langsetter stavane er det seksjonar for alle dei åtte literalane A, ¬A, B, ¬B, C, ¬C, D og ¬D, og ein gjevi formel er representert av ein stav med ein pinne i seksjonen for negasjonen av kvar av literalane i formelen. Til dømes er formelen A ∧ ¬B ∧ C ∧ ¬D representert med staven:

A

¬A

B

¬B

C

¬C

D

¬D

•

•

•

•

(Dette er ei lita forenkling; eigentleg er kvar formel representert av to stavar forbundi med ein streng. Men kvar av desse stavane har pinnar i dei same seksjonane, så det er ikkje så viktig for denne presentasjonen). I tillegg har stavane pinnar for kvar av operasjonane OR, Cop. IS, Full Stop og Finis.

Ein stav kan vere i ein av fire posisjonar. Posisjon 1 tydar at formelen representert av staven er konsistent med premissane vi har skrivi inn i pianoet og posisjon 4 tyder at formelen ikkje er konsistent med premissane. Posisjonane 2 og 3 vert nytta til "mellomrekning". På framsida av pianoet er det hòl inn mot stavane og stavane er merka sånn at ein kan sjå formlane gjennom hòla, men berre for dei stavane som er i posisjon 1.

Kvar av tangentane er forbundi med ein hevarm som går på tvers av stavane. Når ein tangent vert pressa ned vil hevarmen lyfte seg. Hevarmen vil då slå borti pinnane og flytte på stavane. På den måten kan posisjonen til ein stav verte endra (du kan sjå Jevons sin illustrasjon av hevarmane her). For at vi skal få ei kjensle av korleis dette verkar, skal vi gå gjennom eit lite eksempel.

Vi vil skrive inn premissen A → B. I del I såg vi at vi då må skrive

A Cop.IS B FullStop

på pianoet. I utgangspunktet er alle stavane i posisjon 1. Når vi pressar tangenten A (på venstresida) vil ein hevarm lyfte seg og slå borti alle stavane som har ein pinne i seksjon A og flytte dei til posisjon 2. Av di pinnane er plassert i seksjonen for negasjonen til literalane vil det seie at alle formlane som inneheld ¬A no vil vere i posisjon 2 medan formlane som inneheld A vil vere igjen i posisjon 1. No pressar vi tangenten Cop.IS, og den bringer alle stavar i posisjon 3 tilbake til posisjon 1. (Men sidan ingen stavar er i posisjon 3 skjer det ingenting; denne tangenten har berre ein funksjon om ein har nytta OR-tangenten. Vi skal ikkje seie noko meir om dette.) Tangenten B (på høgresida) flyttar alle stavar i posisjon 1 med pinne i seksjon B (formlar med ¬B) til posisjon 3, men let stavane i posisjon 2 vere i fred. No har vi altså formlar med A og B i posisjon 1, formlar med ¬A i posisjon 2 og formlar med A og ¬B i posisjon 3. Full Stop bringer stavane i posisjon 2 tilbake til posisjon 1 og stavane i posisjon 3 til posisjon 4. Etter Full Stop har vi med andre ord dei formlane med A og ¬B i posisjon 4 (og der vert dei verande til vi pressar Finis) og det er akkurat dei formalen som ikkje er konsistente med A → B. Resten av formlane er i posisjon 1, og dei er alle konsistente med premissen.

Kva har skjedd? Jo, alle formlar med ¬A er konsistente med A → B. Difor vert dei "gøymt bort" i posisjon 2, sånn at berre formlar med A kan verte flytta til posisjon 3 (og vidare til posisjon 4) når vi pressar på B-tangenten. Formlane i posisjon 4 er ute av spelet, så dei vil ikkje verte flytta på om vi skriv inn fleire premissar. På den måten kan vi fjerne fleire og fleire formlar ved å skrive inn fleire premissar. Om vi pressar Finis vert sjølvsagt alle formlane dytta tilbake i posisjon 1, og vi kan starte på nytt.

Vi avslutta del I av denne teksten med å seie at logikkpianoet til Jevons i seg sjølv ikkje er veldig interessant. Kvifor det? For det fyrste (med berre fire grunnutsegner og med dei restriksjonane pianoet har på forma til formlane) kan ein ikkje nytte det til å løyse oppgåver/problem som ein ikkje raskt kan løyse på baksida av ein konvolutt. Jevons sjølv forsvara seg med å seie at hensikta eigentleg ikkje var å løyse kompliserte problem, men at maskina var nyttig når han underviste i logikk.

Kunne ikkje Jevons ha laga ei større maskin med fleire grunnutsegner? Kanskje, men ikkje veldig mange fleir. Til saman utgjer stavane i maskina ein sanningstabell for utsegna A∧B∧C∧D kor kvar stav representerer ein rad i tabellen. (Prøv å overtyd deg sjølv om at dette stemmer.) Om vi ser på sanningstabellen for utsegna, er han allereie ganske lang

A	B	C	D
S	S	S	S
S	S	S	U
S	S	U	S
S	S	U	U
S	U	S	S
S	U	S	U
S	U	U	S
S	U	U	U
U	S	S	S
U	S	S	U
U	S	U	S
U	S	U	U
U	U	S	S
U	U	S	U
U	U	U	S
U	U	U	U

og for kvar ny grunnutsegn vil lengda verte fordobla. Men andre ord veks lengda av tabellen eksponentielt med talet på grunnutsegner. Sidan maskina er basert på at ho har ein (fysisk) sanningstabell inni seg vil òg storleiken på maskina vekse eksponentielt med talet på grunnutsegner. Det seier då seg sjølv at det er grenser for kor mange grunnutsegner ei sånn maskin kan tillate.

For det andre løyser ikkje maskina det problemet vi eigentleg er interesserte i. Som regel ønskjer ein ikkje å finne, til dømes, alle moglege konklusjon frå ei mengd med premissar. Det vi heller er interesserte i er å finne ut om ei gjevi utsegn er gyldig (ho er gyldig om ho alltid er sann) eller kva for premissar ho forutset om ho ikkje er gyldig. Difor er dei fleste logikkalkylar og logikkprogram basert på at ein startar med ein mogleg konklusjon og arbeider seg bakover til premissane og aksioma, i motsetnad til maskina til Jevons kor ein startar med nokre premissar og ser kva som skjer. (Vi må hugse at dette var tidleg i historia til den moderne logikken, så Jevons viste ikkje alt det vi veit om logikk.)

Det er openbert feil, som nokon vil hevde, at maskina Jevons bygde var ei slags tidleg datamaskin eller noko liknande. Det er ikkje ein gong sikkert at det går ei historisk line frå Jevons til dei datamaskinene vi har i dag. Kvifor hevdar vi då at logikkpianoet har (ein slags) signifikans i historia til den moderne datamaskina?

Det skal vi kome tilbake til i del III av denne teksten.

Kjelder

William Aspray. Logic machines. I, William Asprey (red.), Computing before computers, side 99-121, Iowa State University Press/Ames, 1990.

William Stanley Jevons. On the mechanical performance of logical inference. Philosophical Transactions of the Royal Society of London, 160:497-518, 1870.

Museum of the History of Science, University of Oxford. (13. november 2005)

I januar 1870 presenterte William Stanley Jevons, på den tida professor i politisk økonomi, logikk og mental- og moralfilosofi i Manchester, ei "logikkmaskin" for The Royal Socitety of London. Denne maskina har seinare vorti kalla Jevons sitt logikkpiano på grunn av utsjånaden (du kan sjå eit bilete her). I denne teksten vil vi presentere logikkmaskina til Jevons og bruken av ho. I del II vil vi forklare korleis maskina fungerar på innsida, og kvifor vi meiner ho har ein slags signifikans i historia som leidde fram til den moderne datamaskina. Men fyrst litt om utsegnslogikk.

I utsegnslogikk har vi utsegner (vi vil kalle dei A, B, C osb.) som kan ha ein av to sanningsverdiar "sann" eller usann"(S eller U). Vi skal ikkje bry oss om kva utsegnene står for, men merkje oss at dei kan vere grunnutsegner eller samansette utsegner. Ei samansett utsegn er sett saman av grunnutsegner og konnektiva "ikkje" (negasjon), "og" (konjunksjon), "eller" (disjunksjon) og "viss-så" (implikasjon). Vi skal nytte symbola ¬, ∧, ∨ og → sånn at vi skjønar ¬A som "ikkje A", A∧B som "A og B", A∨B som "A eller B" og A→B som "viss A, så B". Det er vanleg å definere konnektiva ved hjelp av sanningstabellar. Sanningstabellen for "ikkje" er

A	¬A
S	U
U	S

og vi les denne sånn at ¬A er usann når A er sann og ¬A er sann når A er usann.

Tilsvarande for "og", "eller" og "viss-så" er

A B A∧B S S S S U U U S U U U U

A B A∨B S S S S U S U S S U U U

A B A→B S S S S U U U S S U U S

Tabellen for "og" skal vere ganske grei. Når det gjeld "eller" er det verdt å merkje seg at dette er såkalla "inklusive eller" (i motsetnad til "eksklusive eller") og skal tolkast som "og/eller" og ikkje som "anten eller". "Viss-så" er det nokre som har problem med. Kvifor er det sånn at "viss A, så B" blir sann når A er usann og B er sann? Den enklaste forklaringa er kanskje at vi vil at utsegna "viss A, så B" skal kunne vere sann sjølv når A er usann og difor bryr vi oss ikkje om sanningsverdien til B i det tilfellet. Ta til dømes utsegna "viss det regnar, så vert det vått på bakken". Då kan vi seie at om det ikkje regnar så bryr vi oss ikkje om resten av utsegna. Eller vi kan tenkje at om vi ser ut av vindauget og oppdagar at det ikkje regnar men likevel er vått på bakken, vert ikkje utsegna mindre sann, det kan jo hende nokon har sett på ein vasspreiar.

Det vi manglar no er omgrepa slutning og konsistens. Ei slutning er ei mengd premissar og ein konklusjon som er sånn at premissane og konklusjonen er utsegner og konklusjonen følgjer logisk frå premissane. "Følgjer logisk" tyder her at kvar gong alle premissane er sanne, må også konklusjonen vere sann. Lat oss ta eit lite eksempel.

A → B A B

Utsegnene over streken er premissane og utsegna under streken er konklusjonen. Om vi vil gjere begge premissane sanne set vi fyrst A = S (dette er jo ein av premissane). For å gjere A → B sann til same tid må vi òg setje B = S (sjå tabellen for "viss-så"). På grunn av dette vert konklusjonen (som berre er B) sann, så dette er ei slutning. (Dei som har teki ex.phil. vil kanskje kjenne ho igjen som modus ponens.)

Konsistens er litt meir komplisert. Lat Γ (den greske bokstaven store gamma) vere ei mengd utsegner. Vi seier at Γ er konsistent om det er mogleg å gjere alle utsegnene i Γ sanne samtidig. Til dømes er menga {A, B, A → B} konsistent medan mengda {A, ¬B, A →B} er inkonsistent. Vidare seier vi at ei utsegn Q er konsistent med ei mengd Γ om det er mogleg å gjere alle utsegnene i Γ og Q sanne på ein gong. Det vil seie at B er konsistent med mengda {A, A → B} medan ¬B ikkje er det. (Merk at både B∧C og B∧¬C er konsistente med {A, A → B}; dette vil få relevans.)

No har vi den bakgrunnen vi treng for å forstå korleis logikkpianoet verkar.

Jevons ønskte å analysere slutningar, men klara ikkje lage ei maskin som kunne slutte ein konklusjonen frå ei mengd premissar. Det logikkpianoet hans gjer i staden er å gje oss alle utsegner på ei bestemt form som er konsistente med ei mengd premissar, kor premissane kan ha inntil fire grunnutsegner.

Til å byrje med viser pianoet oss alle utsegner på forma

A ∧ B ∧ C ∧ D

kor A er anten A eller ¬A (vi kallar dette for literalar), osb.; 16 utsegner i alt. Etter kvart som ein skriv inn premissar, vil dei utsegnene som ikkje er konsistente med det ein skriv inn verte borte. Om ein til dømes skriv inn A→B og A vil ein sitje igjen med

A ∧ B ∧ C ∧ D
A ∧ B ∧ C ∧ ¬D
A ∧ B ∧ ¬C ∧ D
A ∧ B ∧ ¬C ∧ ¬D

av di ingen kombinasjonar som inneheld ¬A eller ¬B kan vere konsistente med premissane.

Premissane må òg skrivast inn på ei bestemt form: Dei må ha nøyaktig ei pil, båe sidene av pila må vere ein disjunksjon med null eller fleire disjunktar, og kvar disjunkt ein konjunksjon av ein eller fleire literalar. Kva tyder så dette? Til dømes kan vi skrive inn

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

Venstresida er ein disjunksjon med dei tre disjunktane A, B∧¬C og D. A og D er konjunksjonar av berre éin literal, medan B ∧ ¬C er ein konjunksjon av to literalar. Høgresida av pila er ein disjunksjon med éin disjunkt og denne disjunkten er ein konjunksjon av éin literal. Korleis skal ein då skrive inn til dømes berre A som i eksempelet? Ein disjunksjon med null disjunktar er det same som sanningsverdien S. (Prøv å sjølv finne ut kvifor S→A er det same som A og A→S er det same som S.)

Om du no har lyst til å spele på pianoet til Jevons, finn du ein simulator her. Men før du byrjar: denne simulatoren nyttar notasjonen til Jevons, som er annleis enn den vi har nytta i denne teksten. Literalane A, B, C og D er dei same, men Jenovs nyttar dei små bokstavane a, b, c og d i staden for ¬A, ¬B, ¬C og ¬D. I staden for ∨ nyttar han OR, og han har ikkje noko symbol for "og". Det vil seie at i notasjonen til Jevons er AB det same som A∧B. Tangenten i midten, som er merka "Cop. IS", er implikasjonspila.

Vidare er det sånn at tangentane til venstre for Cop. IS er for å skrive inn det før pila og tangentane til høgre for det etter pila. Kvar premiss skal avsluttast med tangenten "Full Stop", og "Finis" bringer deg tilbake til start. Utsegnene vert vist fram ovanfrå og ned, så til å byrje med ser du

A A A A A A A A a a a a a a a a
B B B B b b b b B B B B b b b b
C C c c C C c c C C c c C C c c
D d D d D d D d D d D d D d D d

Til dømes vil då kolonnen lengst til venstre representere

A ∧ B ∧ C ∧ D

og kolonnen lengst til høgre representerer

¬A ∧ ¬B ∧ ¬C ∧ ¬D

Om du vil freiste det fyrste eksempelet skriv du:

A Cop.IS B FullStop
Cop.IS A FullStop

Resultatet vert då

A A A A
B B B B
C C c c
D d D d

I det andre eksempelet skriv du

A OR B c OR D Cop.IS d FullStop

(Prøv no å finne ut kvifor vi får dette litt keisame resultatet.)

I del II av denne teksten skal vi sjå på korleis logikkpianoet fungerar på innsida. Vi skal òg sjå på kvifor logikkpianoet i seg sjølv ikkje er veldig interessant, men likevel kan seiast å ha ein slags signifikans i datamaskina si historie.

Referansar

William Aspray. Logic machines. I, William Asprey (red.), Computing before computers, side 99-121, Iowa State University Press/Ames, 1990.

William Stanley Jevons. On the mechanical performance of logical inference. Philosophical Transactions of the Royal Society of London, 160:497-518, 1870.

Wikipedia. William Stanley Jevons. (13. november 2005)

Påstandane til ml-LTLD manglar fullstendig truverd inntil formlane vert presentert.

Senter for Marxistiske og Matematiske Studium, Enschede