Formella system

 

Formella system är uppbyggda i tre nivåer.

 

·       Tecken som t ex →, ~ eller X  som kan sättas samman i strängar, t ex  ~ ~ Χ → X  eller XXXXXXXX

·       Regler som bestämmer hur strängar kan sättas ihop och som därmed är välformade strängar

·       Meta-regler som bestämmer vilka av de välformade strängarna som har en särskild status, som är det formella systemets satser (=teorem)

 

Vi exemplifierar med ett mycket enkelt formellt system som hittats på av Hofstadter.[1] Här följer definitionen:

 

·       Tecken som används är p, q och –

·       Välformade strängar är strängar som innehåller tre grupper av tecknet – åtskiljt av exakt ett p och ett q (exempelvis – p – q – –)

·       Särskild status som axiom har alla strängar av formen x p – q x – där x står för ett eller flera – och en enda produktionsregel  ger alla övriga teorem.

 

 

Produktionsregeln

 

Om x p y q z är ett teorem, där x, y och z står för ett eller flera – , så är också x p y – q z – ett teorem.

 

Hofstadter hittade på just detta formella system för att simulera addition av två positiva heltal. Var och en kan försäkra sig om det genom att producera teorem och tolka dem på detta sätt:

 

Tecknet p utläses som plus.

Tecknet q utläses som "är lika med" (engelskans equal).

Tecknet – utläses som ett.

Teckensträngen – – utläses som två.

Teckensträngen – – – som tre, – – – – som fyra o s v

 

Vårt exempel på en välformad sträng (som också råkar vara ett teorem såsom varande ett axiom) – p – q – – utläses alltså; ett plus ett är lika med två.

Men observera! Strängen – p – p – – q – – – – som du kära läsare säkert nu lätt översätter till ett plus ett plus två är lika med fyra, finns inte med som teorem, varken som axiom eller härledd via axiom och aldrig så många upprepningar av produktionsregeln. I själva verket ser vi det direkt, eftersom den strängen inte ens är välformad enligt systemets regler (det får inte finnas mer än ett p).

Med den tolkning av symbolerna i systemet som vi anlagt är det uppenbart att det finns många strängar som skulle vara korrekta men som helt enkelt inte är med i systemet.

Det är meta-reglerna som gör formella system intressanta. Det finns ett formellt system,  Booleansk algebra, som har en speciell status i den oändliga mängden formella system. Vi bygger upp det med hjälp av de nu välkända tre nivåerna på följande vis:

 

·       Tecken som används kan vara ~ , V, [ , ] samt vissa bokstäver exempelvis  x, y, z som  benämns variabler

·       Regler som bestämmer hur strängar kan sättas ihop som välformade strängar är för det första att en ensam variabel är en välformad sträng, samt, för det andra att om strängarna S och T är välformade strängar så är strängarna [~S] samt [SVT] också välformade strängar.

·       Meta-reglerna ger vissa välformade strängar enligt ovan en särskild status som teorem, dels genom att lista fyra strängar som systemets axiom, och dels genom substitutionsregeln och regeln för modus ponens

 

Naturligtvis kan andra tecken användas. Det går t ex att klara sig med färre tecken med hjälp av förkortningar. En praktisk variant är att förkorta en sträng som [~x]Vy till x→y. Med dessa noteringar kan Booleansk algebra ges följande definition på metanivån.

 

 

Axiom

 

1.    [[xVx]→x]

2.    [x→[xVy]]

3.    [[xVy]→[yVx]]

4.    [[x→y]→[[zVx]→[zVy]]]

 

 

Substitutionsregeln

 

Om strängen S är en välformad sträng och strängen T är ett teorem som innehåller en variabel, så är också den sträng om erhålls om man byter ut variabeln mot S ett teorem.

 

 

Modus ponens

 

Om strängen [S→T] är ett teorem och S är ett teorem, så är T ett teorem.

 

Booleansk algebra är ett komplett formellt system, vilket innebär att för varje välformad sträng, S, kan antingen S själv eller [~S] härledas. Dessa två strängvarianter tolkas därför vanligtvis som motsatser. Att systemet är komplett betyder också att lägger man till andra välformade strängar som axiom kan de antingen redan härledas och är därför onödiga, eller så kan de inte härledas vilket också innebär att både S och [~S] kan härledas. I det senare fallet tappar hela systemet i tolkningsmöjligheter och kollapsar till de båda första nivåerna. Meta-regeln blir då att alla välformade strängar är teorem. Däremot kan ytterligare axiom hänförande till nyinförda tecken och produktionsregler användas för att bygga upp alla de vanliga logiska och matematiska strukturerna.