Formelt system
Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 31. august 2021; checks kræver 3 redigeringer .Et formelt system ( formel teori , aksiomatisk teori , aksiomatik , deduktivt system ) er resultatet af en streng formalisering af teorien , som forudsætter en fuldstændig abstraktion fra betydningen af ordene i det anvendte sprog, og alle de betingelser, der styrer brugen af disse ord i teorien er eksplicit angivet gennem aksiomer og regler, der gør det muligt at udlede en sætning fra andre [1] .
Et formelt system er en samling abstrakte objekter, der ikke er relateret til omverdenen, hvor reglerne for at operere med et sæt symboler præsenteres i en strengt syntaktisk fortolkning uden at tage hensyn til det semantiske indhold, det vil sige semantikken. Strengt beskrevne formelle systemer dukkede op efter Hilbert-problemet blev stillet . Den første FS dukkede op efter udgivelsen af bøgerne af Russell og Whitehead "Formal Systems"[ angiv ] . Disse FS blev præsenteret med visse krav.
Grundlæggende
En formel teori anses for at være defineret, hvis [2] :
- Et endeligt eller tælligt sæt af vilkårlige symboler er givet. Finite sekvenser af symboler kaldes teoriudtryk .
- Der er en delmængde af udtryk kaldet formler .
- En delmængde af formler, kaldet aksiomer , er blevet udpeget .
- Der er et begrænset sæt af relationer mellem formler, kaldet slutningsregler .
Der er normalt en effektiv procedure, der tillader et givet udtryk at bestemme, om det er en formel. Ofte er et sæt formler givet ved en induktiv definition . Som regel er dette sæt uendeligt. Sæt af symboler og sæt af formler definerer tilsammen sproget eller signaturen for en formel teori.
Oftest er det muligt effektivt at finde ud af, om en given formel er et aksiom; i et sådant tilfælde siges teorien at være effektivt aksiomatiseret eller aksiomatisk . Sættet af aksiomer kan være endeligt eller uendeligt. Hvis antallet af aksiomer er endeligt, siges teorien at være endeligt aksiomatiserbar . Hvis sættet af aksiomer er uendeligt, så specificeres det som regel ved hjælp af et begrænset antal aksiomskemaer og reglerne for generering af specifikke aksiomer fra aksiomskemaet. Sædvanligvis opdeles aksiomer i to typer: logiske aksiomer (fælles for en hel klasse af formelle teorier) og ikke- logiske eller egentlige aksiomer (der bestemmer specifikationer og indhold af en bestemt teori).
For hver slutningsregel R og for hver formel A er spørgsmålet om, hvorvidt det valgte formlsæt står i forhold til R med formlen A , effektivt løst , og i så fald kaldes A for en direkte konsekvens af disse formler iht. regel R.
En afledning er en hvilken som helst sekvens af formler, således at enhver formel i sekvensen enten er et aksiom eller en direkte konsekvens af nogle tidligere formler ifølge en af afledningsreglerne.
En formel kaldes en sætning, hvis der er en afledning, hvor denne formel er den sidste.
En teori, for hvilken der er en effektiv algoritme, der giver dig mulighed for ud fra en given formel at finde ud af, om dens afledning eksisterer, kaldes afgørelig ; ellers siges teorien at være uafklarelig .
En teori, hvor ikke alle formler er sætninger, siges at være absolut konsistente .
Definition og varianter
En deduktiv teori anses for givet, hvis:
- Et alfabet ( sæt ) og regler for dannelsen af udtryk ( ord ) i dette alfabet er givet.
- Reglerne for dannelsen af formler (velformede, korrekte udtryk) er givet.
- Fra mængden af formler vælges en delmængde T af sætninger ( bevisbare formler ) på en eller anden måde.
Variationer af deduktive teorier
Afhængigt af metoden til at konstruere et sæt sætninger:
Angivelse af aksiomer og inferensregler
I formlsættet udskilles en delmængde af aksiomer, og et begrænset antal inferensregler er specificeret - sådanne regler ved hjælp af hvilke (og kun ved hjælp af dem) nye sætninger kan dannes ud fra aksiomer og tidligere afledt teoremer. Alle aksiomer indgår også i antallet af sætninger. Nogle gange (for eksempel i Peanos aksiomatik ), indeholder en teori et uendeligt antal aksiomer, der er specificeret ved hjælp af et eller flere aksiomskemaer . Aksiomer kaldes undertiden "skjulte definitioner". På denne måde specificeres en formel teori ( formel aksiomatisk teori , formel (logisk) regning ).
Spørger kun aksiomer
Kun aksiomer er givet, slutningsreglerne anses for at være velkendte.
Med en sådan specifikation af sætninger siger man, at der er givet en semi-formel aksiomatisk teori . EksemplerAngivelse af kun slutningsregler
Der er ingen aksiomer (sættet af aksiomer er tomt), kun slutningsregler er givet.
Faktisk er den således definerede teori et specialtilfælde af den formelle, men den har sit eget navn: teorien om naturlig inferens .Egenskaber ved deduktive teorier
Konsistens
En teori, hvor sættet af sætninger dækker hele sættet af formler (alle formler er sætninger, "sande udsagn") kaldes inkonsistent . Ellers siges teorien at være konsistent . Belysning af inkonsistensen i en teori er en af den formelle logiks vigtigste og nogle gange sværeste opgaver.
Fuldstændighed
En teori kaldes komplet , hvis der for en sætning (lukket formel) enten sig selv eller dens negation kan udledes . Ellers indeholder teorien ubeviselige udsagn (udsagn, der hverken kan bevises eller modbevises ved hjælp af teorien selv), og kaldes ufuldstændige .
Uafhængighed af aksiomer
Et individuelt aksiom for en teori siges at være uafhængigt , hvis dette aksiom ikke kan udledes fra resten af aksiomerne. Det afhængige aksiom er i det væsentlige overflødigt, og dets fjernelse fra systemet af aksiomer vil ikke påvirke teorien på nogen måde. Hele systemet af aksiomer i en teori kaldes uafhængigt , hvis hvert aksiom i den er uafhængigt.
Opløselighed
En teori kaldes afgørbar , hvis begrebet en sætning er effektiv i den , det vil sige, at der er en effektiv proces (algoritme), der gør det muligt for enhver formel at bestemme i et begrænset antal trin, om det er en sætning eller ej.
Nøgleresultater
- I 30'erne. I det 20. århundrede viste Kurt Gödel , at der er en hel klasse af førsteordensteorier, der er ufuldstændige. Desuden kan formlen, der angiver en teoris konsistens, heller ikke udledes ved hjælp af selve teorien (se Gödels ufuldstændighedssætninger ). Denne konklusion var af stor betydning for matematikken, da formel aritmetik (og enhver teori, der indeholder det som en underteori) netop er sådan en førsteordensteori, og derfor ufuldstændig.
- På trods af dette er teorien om reelle lukkede felter med addition, multiplikation og ordensrelation komplet ( Tarski-Seidenberg-sætningen ).
- Alonzo Church beviste, at problemet med at bestemme gyldigheden af enhver vilkårlig prædikatlogikformel er algoritmisk uløselig .
- Propositionsregningen er en konsistent, komplet, afgørelig teori.
Se også
- Autoformalisering
- mængdeteori
- formel logik
- Formalisme (matematik)
- Kodesystem
- Termodynamikkens aksiomatik
Eksempler på formelle systemer
- propositionsregning
- Første ordens teorier (første ordens logik)
- Højere ordensteorier (højere ordens logik)
- lambdaregning
- Lambdaregning med typer
- Konstruktionsberegning
- Beregning af induktive konstruktioner
Noter
- ↑ Kleene S.K. Introduktion til metamathematics . - M. : IL, 1957. - S. 59-60. Arkiveret 1. maj 2013 på Wayback Machine
- ↑ Mendelssohn E. Introduktion til matematisk logik . - M . : "Nauka", 1971. - S. 36. Arkivkopi dateret 1. maj 2013 på Wayback Machine
Litteratur
- Galiev Sh. I. Matematisk logik og teori om algoritmer. - Kazan: KSTUs forlag opkaldt efter. A. N. Tupolev. 2002.
- Kleene S. K. Introduktion til metamatematik . - M. : IL, 1957. - 526 s.
- Kleene S. K. Matematisk logik . - M . : "Mir", 1973. - 480 s.
- Mendelsohn E. Introduktion til matematisk logik . - M . : "Nauka", 1971. - 320 s.
- Novikov F. A. Diskret matematik for programmører. - Sankt Petersborg: Peter, 2000. - 304 s.: ill. ISBN 5-272-00183-4 .
- Yanovskaya S. A. Fra aksiomatikkens historie // Historisk og matematisk forskning . - M. : GITTL, 1958. - Nr. 11 . - S. 63-96 .
 Ordbøger og encyklopædier |
|---|
| Logikker | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Filosofi • Semantik • Syntaks • Historie | |||||||||
| Logiske grupper |
| ||||||||
| Komponenter |
| ||||||||
| Liste over booleske symboler | |||||||||