Bevisteori

Bevisteori  er et afsnit af matematisk logik , der præsenterer beviser i form af formelle matematiske objekter, der analyserer dem ved hjælp af matematiske metoder. Beviser præsenteres normalt som induktivt definerede datastrukturer , såsom lister og træer, skabt i henhold til aksiomer og inferensregler for formelle systemer. Således er bevisteori syntaktisk i modsætning til semantisk modelteori . Sammen med modelteori , aksiomatisk mængdelære og beregningsteori er bevisteori en af ​​de såkaldte "fire søjler" i matematikken [1] . Bevisteori bruger en præcis definition af begrebet bevis til at bevise umuligheden af ​​at bevise en bestemt påstand inden for en given matematisk teori. [2]

Bevisteori er vigtig for filosofisk logik , hvor ideen om bevisteoretisk semantik er af uafhængig interesse, en idé, der er baseret på gennemførligheden af ​​formelle logiske metoder til strukturel bevisteori.

Historie

Selvom formaliseringen af ​​logikken blev væsentligt fremskreden af ​​forfattere som H. Frege , J. Peano , B. Russell og R. Dedekind , anses historien for moderne bevisteori generelt for at være begyndt med D. Hilbert , som igangsatte det, der kaldes Hilberts program for matematikkens grundlag. Kurt Gödels originale arbejde med bevisteori førte først frem og tilbageviste dette program: hans fuldstændighedssætning virkede oprindeligt som et godt varsel for Hilberts mål om at præsentere al matematik som et endeligt formelt system; dog viste hans ufuldstændighedssætninger da , at dette mål var uopnåeligt. Alt dette arbejde blev udført med bevisregning kaldet Hilbert-systemer .

Sideløbende blev grundlaget for strukturbevisteorien udviklet . Jan Lukasiewicz foreslog i 1926, at man kunne forbedre Hilberts systemer som grundlag for den aksiomatiske repræsentation af logik ved at variere udledningen af ​​konklusioner fra antagelser ved hjælp af slutningsregler. I udviklingen af ​​denne idé skabte S. Yankovsky (1929) og G. Gentzen (1934) uafhængigt systemer kaldet naturlig deduktionskalkuli (naturlig inferens), der kombinerede dem med Gentzens tilgang, som introducerer ideen om symmetri mellem antagelser om udsagn i introduktionsregler og konsekvenserne af at acceptere påstande i sletteregler, en idé der har vist sig at være meget vigtig i bevisteori. Gentzen (1934) introducerede yderligere de såkaldte sequent calculi , som bedre udtrykte dualiteten af ​​logiske forbindelser, og fortsatte med at yde grundlæggende bidrag til formaliseringen af ​​intuitionistisk logik; han leverede også det første kombinatoriske bevis på konsistensen af ​​Peano-aritmetikken. Udviklingen af ​​naturlig deduktion og den efterfølgende beregning introducerede den grundlæggende idé om analytisk bevis i bevisteori.

Formelt og uformelt bevis

Uformelle beviser for dagligdags matematisk praksis er ikke som formelle beviser for teori. De er snarere som skitser på højt niveau, der giver en ekspert mulighed for at rekonstruere et formelt bevis, i det mindste i princippet, givet nok tid og tålmodighed. For de fleste matematikere er processen med at skrive et fuldt formelt bevis for pedantisk og omfattende til at blive brugt ofte.

Formelle beviser er bygget ved hjælp af en computer i et interaktivt teorembevissystem. Det er vigtigt, at disse beviser også kan verificeres automatisk. Det er normalt nemt at kontrollere formelle beviser, mens det generelt er svært at finde beviser (automatiseret teorembevis). Et uformelt bevis i en matematisk publikation kræver dog ugers omhyggelig analyse og verifikation og kan stadig indeholde fejl.

Typer af bevisregning

De tre mest berømte typer af bevisregning er:

• Hilbert beregning
• Naturlige fradragsberegninger
• Sekvensberegning

Hver af dem kan give en fuldstændig aksiomatisk formalisering af den klassiske eller intuitionistiske tilgangs propositionelle eller prædikatlogik, til næsten enhver modal logik og til mange substrukturelle logikker såsom relevant eller lineær logik. Faktisk er det ret svært at finde en logik, der ikke kunne repræsenteres i en af ​​disse beregninger.

Konsistensbeviser

Som allerede nævnt var drivkraften til den matematiske undersøgelse af beviser i formelle teorier Hilberts program. Den centrale idé med dette program var, at hvis vi kunne give endelige (endelige) beviser for konsistensen af ​​alle nøjagtige formelle teorier, der er nødvendige for matematikere, så kunne vi retfærdiggøre disse teorier med et metamatematisk argument, der viser, at alle deres universelle (generelt gyldige) udsagn (teknisk deres bevisbare sætninger) er endeligt sande; så når de er berettigede, bekymrer vi os ikke længere om de ikke-endelige implikationer af deres eksistentielle sætninger, idet vi betragter dem som pseudo-meningsfulde konventioner om eksistensen af ​​ideelle enheder.

Programmets fiasko var forårsaget af K. Gödels ufuldstændighedssætninger, som viste, at en eller anden teori, stærk nok til at udtrykke simple aritmetiske sandheder, ikke kan bevise sin egen konsistens. Siden da er der blevet forsket meget i dette emne, og der er opnået resultater, der især giver: svækkelse af konsistenskravet; aksiomatisering af kernen i Gödels resultat i form af modalt sprog, bevislighedslogik; transfinit iteration af teorier ifølge A. Turing og S. Feferman ; den nylige opdagelse af teorier om selvtestning – systemer, der er stærke nok til at hævde sig selv, men for svage over for det diagonale argument , Gödels nøgleargument for ubevisbarhed.

Strukturel bevisteori

Strukturel bevisteori er en gren af ​​bevisteori, der studerer de bevisregninger, der understøtter begrebet analytisk bevis . Begrebet analytisk bevis blev introduceret af Gentzen til beregning af sekventer. Hans beregning af naturlig deduktion understøtter også begrebet analytisk bevis. Vi siger, at analytiske beviser er normale former, relateret til forestillingen om en normal form i termomskrivningssystemer. Mere eksotiske bevisregninger, såsom I. Giros bevisnetværk, understøtter også begrebet analytisk bevis.

Strukturel bevisteori er relateret til typeteori gennem Curry-Howard-korrespondancen, som er baseret på den strukturelle analogi mellem normaliseringsprocessen i naturlig deduktionskalkyl og beta-reduktionen af ​​typebestemt lambda-regning . Denne korrespondance danner grundlag for den intuitionistiske typeteori udviklet af M.-Lef og udvides ofte til trepartskorrespondancen, hvis tredje støtte er kartesiske lukkede kategorier.

Bevisteoretisk semantik

Lingvistik, logisk-type grammatik, kategorisk grammatik og Montagu grammatik bruger formalisme baseret på strukturel bevisteori til at give formel semantik til naturligt sprog.

Tabelsystemer

Analytiske tabeller bruger den centrale idé om analytisk bevis fra strukturel bevisteori til at levere opløsningsprocedurer for en bred vifte af logikker.

Ordinalanalyse

Mange tilstrækkeligt ekspressive formelle teorier kan forbindes med deres karakteristiske ordinal, kendt som teoriens bevisteoretiske ordinal . Ordinalanalyse er et felt, hvis emne er beregningen af ​​bevisteoretiske ordinaler for teorier.

G. Gentzen beregnede ordinalen af ​​førsteordens Peano-aritmetik  - han fastslog, at konsistens kan bevises ved transfinit induktion til ordinalen . Yderligere undersøgelser viste, at princippet om transfinit induktion viser sig for ordinaler mindre end , men ikke for ordinalen selv , og at beregnelige funktioner, overalt - hvis bestemthed kan bevises i , falder sammen med -rekursive funktioner. Selvom analoger af disse resultater i det generelle tilfælde for andre teorier ikke behøver at finde sted samtidigt for den samme ordinal, for naturlige tilstrækkeligt stærke teorier, giver analoger af disse resultater som regel ikke forskellige ordinaler for den samme teori (samt andre tilgange til definitionen af ​​en bevisteoretisk ordinal).

Bevisteoretiske ordtal er blevet beregnet for en række fragmenter af andenordens aritmetik og udvidelser af Kripke-Platek mængdelære. Spørgsmålet om at beregne den bevisteoretiske ordinal for fuldstændig andenordens aritmetik og stærkere teorier, især Zermelo-Fraenkel-mængdeteorien , er stadig åben.

Analyse af bevisets logik (substrukturel logik)

Adskillige vigtige logikker er afledt af overvejelser om den logiske struktur, der opstår i strukturel bevisteori.

Se også

• Modelteori
• Bevis (sandt)
• Metoder til bevis
• Mellemlogik

Links

1. Hao Wang (1981) Populære forelæsninger om matematisk logik. ISBN 0-442-23109-1 .
2. D. Barwise (red., 1978). Handbook of Mathematical Logic, bind. fjorten.
3. G. Takeuchi. Bevisteorien. M., Mir, 1978
4. A. Troelstra (1996). Grundlæggende bevisteori. In Series: Cambridge Treatises on Theoretical Computer Science, University of Cambridge, ISBN 0-521-77911-1 .
5. D. von Plateau (2008). Udvikling af bevisteori. Stanford Encyclopedia of Philosophy.

Noter

1. ↑ F.eks. Wang (1981), s. 3-4 og Barwise (1978).
2. ↑ Proof Theory, 1978 , s. 5.

Litteratur

• Takeuchi G. Bevisteori. - M . : Mir, 1978. - 412 s.

Ordbøger og encyklopædier	Universalis Universalis
I bibliografiske kataloger BNF : 122670310 J9U : 987007541259805171 LCCN : sh85107437 , sh85107437 LNB : 000137654 NDL : 01190375 NKC : ph126551