Formellt system

Wikipedia

	Denna artikel innehåller ifrågasatta faktauppgifter.
	Se diskussionssidan, eller historiken, för mer information. Rätta gärna felaktigheter.

Ett formellt system eller en logik (pluralis logi´ker) är en uppsättning axiom och ett antal härledningsregler. Axiomen är strängar som är sanna (utan härledning) i systemet.

Härledningsreglerna är regler som säger hur strängarna får modifieras för att ge nya strängar. Alla strängar som kan fås ur axiomen via ett antal härledningsregler kallas teorem.

Exempel på logiker: första ordningens logik, satslogik, modallogik, relationell logik etc.

[redigera] Exempel

Axiom:

Härledningsregler:

På alla ställen där det står B får man lägga till B direkt efter.
Man får ta bort C var man vill.

Teorem:

BBB

Härledning:

CB -(H1)-> CBB -(H1)-> CBBB -(H2)-> BBB

Vilket skulle visas

[redigera] Om matematik som formellt system

Tanken att hela matematikan kan beskrivas som ovan kallas formalism. Kurt Gödel visade med sitt ofullständighetsteorem att detta inte är möjligt. Mer exakt uttryckt: Det finns satser i matematiken som varken kan bevisas vara sanna eller falska. Formella system är dock fortfarande användbara för att beskriva system som inte är fullständiga men tillräckligt uttrycksfulla för att beskriva användbara modeller. Det Kurt Gödel visade i sitt teorem var, mer precist, att varje formellt system tillräckligt komplicerat för att hantera aritmetik alltid innehåller oavgörbara satser och sanningar som inte går att bevisa. Om man kan bevisa att systemet är konsistent så finns det sådana satser, och systemet är alltså ofullständigt. Om man däremot har ett inkonsistent system, så kan man undvika denna typ av satser, priset man får betala är dock stort, systemet är totalt oanvändbart eftersom alla satser är bevisbara i ett sådant system. Slutsats: det finns (bevisligen) obevisbara men likväl sanna satser i varje formellt system som omfattar elementär aritmetik förutsatt att systemet i fråga är konsistent. Ett system tillräckligt rikt för att omfatta aritmetik kan inte vara både konsistent och fullständigt.