Formellt system
Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 31 augusti 2021; kontroller kräver 3 redigeringar .Ett formellt system ( formell teori , axiomatisk teori , axiomatik , deduktivt system ) är resultatet av en strikt formalisering av teorin , som förutsätter en fullständig abstraktion från betydelsen av orden i det använda språket, och alla villkor som styr användningen av dessa ord i teorin anges uttryckligen genom axiom och regler som gör det möjligt att härleda en fras från andra [1] .
Ett formellt system är en samling abstrakta objekt som inte är relaterade till omvärlden, där reglerna för att arbeta med en uppsättning symboler presenteras i en strikt syntaktisk tolkning utan att ta hänsyn till det semantiska innehållet, det vill säga semantiken. Strikt beskrivna formella system dök upp efter att Hilbert-problemet ställdes . Den första FS dök upp efter publiceringen av böckerna av Russell och Whitehead "Formal Systems"[ specificera ] . Dessa FS presenterades med vissa krav.
Grunderna
En formell teori anses definierad om [2] :
- En ändlig eller räknebar uppsättning godtyckliga symboler ges. Finita sekvenser av symboler kallas teoriuttryck .
- Det finns en delmängd av uttryck som kallas formler .
- En delmängd av formler, kallade axiom , har pekats ut .
- Det finns en ändlig uppsättning relationer mellan formler, kallade slutledningsregler .
Det finns vanligtvis en effektiv procedur som gör att ett givet uttryck kan avgöra om det är en formel. Ofta ges en uppsättning formler av en induktiv definition . Som regel är denna uppsättning oändlig. Uppsättningen av symboler och uppsättningen formler definierar tillsammans språket eller signaturen för en formell teori.
Oftast är det möjligt att effektivt ta reda på om en given formel är ett axiom; i ett sådant fall sägs teorin vara effektivt axiomatiserad eller axiomatisk . Uppsättningen av axiom kan vara ändlig eller oändlig. Om antalet axiom är ändligt, sägs teorin vara ändligt axiomatiserbar . Om uppsättningen av axiom är oändlig, så specificeras den som regel med ett ändligt antal axiomscheman och reglerna för att generera specifika axiom från axiomschemat. Vanligtvis delas axiom in i två typer: logiska axiom (vanligt för en hel klass av formella teorier) och icke- logiska eller egentliga axiom (som bestämmer detaljerna och innehållet i en viss teori).
För varje slutledningsregel R och för varje formel A löses frågan om den valda formleruppsättningen står i relation till R med formeln A effektivt , och om så är fallet kallas A för en direkt konsekvens av dessa formler enligt regel R.
En härledning är vilken sekvens av formler som helst så att vilken formel som helst i sekvensen antingen är ett axiom eller en direkt följd av några tidigare formler enligt en av härledningsreglerna.
En formel kallas ett sats om det finns en härledning där denna formel är den sista.
En teori för vilken det finns en effektiv algoritm som låter dig ta reda på en given formel om dess härledning existerar kallas avgörbar ; annars sägs teorin vara obeslutbar .
En teori där inte alla formler är satser sägs vara absolut konsekvent .
Definition och varianter
En deduktiv teori anses vara given om:
- Ett alfabet ( set ) och regler för bildandet av uttryck ( ord ) i detta alfabet anges.
- Reglerna för bildandet av formler (välformade, korrekta uttryck) ges.
- Från formleruppsättningen väljs en delmängd T av satser ( bevisbara formler ) på något sätt.
Variationer av deduktiva teorier
Beroende på metoden för att konstruera en uppsättning satser:
Specificering av axiom och slutledningsregler
I formleruppsättningen pekas en delmängd av axiom ut, och ett ändligt antal inferensregler specificeras - sådana regler med hjälp av vilka (och endast med hjälp av dem) nya satser kan bildas från axiom och tidigare härledas satser. Alla axiom ingår också i antalet satser. Ibland (till exempel i Peanos axiomatik ) innehåller en teori ett oändligt antal axiom som specificeras med ett eller flera axiomscheman . Axiom kallas ibland "dolda definitioner". På så sätt specificeras en formell teori ( formell axiomatisk teori , formell (logisk) kalkyl ).
Frågar bara axiom
Endast axiom ges, slutledningsreglerna anses vara välkända.
Med en sådan specifikation av satser, säger man att en semi-formell axiomatisk teori ges . ExempelSpecificerar endast inferensregler
Det finns inga axiom (uppsättningen av axiom är tom), endast slutledningsregler ges.
I själva verket är den sålunda definierade teorin ett specialfall av den formella, men den har sitt eget namn: teorin om naturlig slutledning .Egenskaper för deduktiva teorier
Konsistens
En teori där uppsättningen satser täcker hela formleruppsättningen (alla formler är satser, "sanna påståenden") kallas inkonsekvent . Annars sägs teorin vara konsekvent . Att klargöra inkonsekvensen i en teori är en av den formell logikens viktigaste och ibland svåraste uppgifter.
Fullständighet
En teori kallas komplett om i den för någon mening (sluten formel) antingen sig själv eller dess negation är härledbar . I övrigt innehåller teorin obevisbara påståenden (påståenden som varken kan bevisas eller motbevisas med hjälp av själva teorin), och kallas ofullständig .
Axiomens oberoende
Ett individuellt axiom för en teori sägs vara oberoende om det axiomet inte kan härledas från resten av axiomen. Det beroende axiomet är väsentligen överflödigt, och dess borttagande från systemet av axiom kommer inte att påverka teorin på något sätt. Hela systemet av axiom i en teori kallas oberoende om varje axiom i den är oberoende.
Lösbarhet
En teori kallas avgörbar om begreppet ett teorem är effektivt i det , det vill säga det finns en effektiv process (algoritm) som gör det möjligt för vilken formel som helst att i ett ändligt antal steg avgöra om det är ett teorem eller inte.
Nyckelresultat
- På 30-talet. På 1900-talet visade Kurt Gödel att det finns en hel klass av första ordningens teorier som är ofullständiga. Dessutom är formeln som anger en teoris konsistens inte heller härledbar med hjälp av själva teorin (se Gödels ofullständighetsteorem ). Denna slutsats var av stor betydelse för matematiken, eftersom formell aritmetik (och varje teori som innehåller den som en delteori) är just en sådan första ordningens teori, och därför ofullständig.
- Trots detta är teorin om verkliga slutna fält med addition, multiplikation och ordningsrelation komplett ( Tarski-Seidenbergs sats ).
- Alonzo Church bevisade att problemet med att bestämma giltigheten av en godtycklig predikatlogikformel är algoritmiskt oavgörbart .
- Propositionskalkylen är en konsekvent, komplett, avgörbar teori.
Se även
- Autoformalisering
- mängdteori
- formell logik
- Formalism (matematik)
- Kodsystem
- Termodynamikens axiomatik
Exempel på formella system
- propositionskalkyl
- Första ordningens teorier (första ordningens logik)
- Högre ordningsteorier (logik av högre ordning)
- lambda kalkyl
- Lambdakalkyl med typer
- Konstruktionskalkyl
- Beräkning av induktiva konstruktioner
Anteckningar
- ↑ Kleene S.K. Introduktion till metamatematik . - M. : IL, 1957. - S. 59-60. Arkiverad 1 maj 2013 på Wayback Machine
- ↑ Mendelssohn E. Introduktion till matematisk logik . - M . : "Nauka", 1971. - S. 36. Arkivexemplar daterad 1 maj 2013 på Wayback Machine
Litteratur
- Galiev Sh. I. Matematisk logik och teori för algoritmer. - Kazan: KSTUs förlag uppkallat efter. A.N. Tupolev. 2002.
- Kleene S. K. Introduktion till metamatematik . - M. : IL, 1957. - 526 sid.
- Kleene S. K. Matematisk logik . - M . : "Mir", 1973. - 480 sid.
- Mendelsohn E. Introduktion till matematisk logik . - M . : "Nauka", 1971. - 320 sid.
- Novikov F. A. Diskret matematik för programmerare. - St Petersburg: Peter, 2000. - 304 s.: ill. ISBN 5-272-00183-4 .
- Yanovskaya S. A. Från axiomatikens historia // Historisk och matematisk forskning . - M. : GITTL, 1958. - Nr 11 . - S. 63-96 .
 Ordböcker och uppslagsverk |
|---|
| Logik | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Filosofi • Semantik • Syntax • Historia | |||||||||
| Logiska grupper |
| ||||||||
| Komponenter |
| ||||||||
| Lista över booleska symboler | |||||||||