Bevisteori

Bevisteori  är en del av matematisk logik som presenterar bevis i form av formella matematiska objekt, analyserar dem med matematiska metoder. Bevis presenteras vanligtvis som induktivt definierade datastrukturer , såsom listor och träd, skapade enligt axiom och slutledningsregler för formella system. Således är bevisteori syntaktisk , till skillnad från semantisk modellteori . Tillsammans med modellteori , axiomatisk mängdlära och beräkningsteori är bevisteori en av matematikens så kallade "fyra pelare" [1] . Bevisteori använder en exakt definition av begreppet bevis för att bevisa omöjligheten att bevisa en viss proposition inom en given matematisk teori. [2]

Bevisteori är viktig för filosofisk logik , där idén om bevisteoretisk semantik är av självständigt intresse, en idé som bygger på genomförbarheten av formella logiska metoder för strukturell bevisteori.

Historik

Även om formaliseringen av logik avsevärt har utvecklats av författare som H. Frege , J. Peano , B. Russell och R. Dedekind , anses historien om modern bevisteori allmänt ha börjat med D. Hilbert , som initierat det som kallas Hilberts program för matematikens grunder. Kurt Gödels ursprungliga arbete om bevisteori avancerade först och sedan tillbakavisade detta program: hans fullständighetsteorem verkade initialt vara ett gott omen för Hilberts mål att presentera all matematik som ett ändligt formellt system; emellertid visade hans ofullständighetssatser då att detta mål var ouppnåeligt. Allt detta arbete gjordes med beviskalkyler som kallas Hilbert-system .

Parallellt utvecklades grunderna för teorin om strukturella bevis . Jan Lukasiewicz föreslog 1926 att man kunde förbättra Hilberts system som grund för logikens axiomatiska representation genom att variera slutsatsernas härledning från antaganden genom slutledningsregler. Vid utvecklingen av denna idé skapade S. Yankovsky (1929) och G. Gentzen (1934) oberoende system som kallas naturliga deduktionskalkyler (naturlig inferens), och kombinerade dem med Gentzens tillvägagångssätt, som introducerar idén om symmetri mellan antaganden om påståenden i regler för introduktion, och konsekvenserna av att acceptera påståenden i raderingsregler, en idé som har visat sig vara mycket viktig i bevisteorin. Gentzen (1934) introducerade ytterligare de så kallade sequent calculi , som bättre uttryckte dualiteten av logiska kopplingar, och fortsatte med att ge grundläggande bidrag till formaliseringen av intuitionistisk logik; han gav också det första kombinatoriska beviset för Peanos aritmetiks konsistens. Utvecklingen av naturlig deduktion och den efterföljande kalkylen introducerade den grundläggande idén om analytiska bevis i bevisteori.

Formella och informella bevis

Informella bevis för vardaglig matematisk praktik är inte som formella bevis för teori. De är snarare som skisser på hög nivå som låter en expert rekonstruera ett formellt bevis, åtminstone i princip, med tillräckligt med tid och tålamod. För de flesta matematiker är processen att skriva ett helt formellt bevis för pedantisk och mångsidig för att användas ofta.

Formella bevis byggs med hjälp av en dator i ett interaktivt teorembevissystem. Det är viktigt att dessa bevis också kan verifieras automatiskt. Att kontrollera formella bevis är vanligtvis lätt, medan det i allmänhet är svårt att hitta bevis (automatiserad teorembevis). Ett informellt bevis i en matematisk publikation kräver dock veckor av noggrann analys och verifiering och kan fortfarande innehålla fel.

Typer av beviskalkyl

De tre mest kända typerna av beviskalkyl är:

• Hilbert kalkyl
• Naturliga avdragskalkyler
• Sekvenskalkyl

Var och en av dem kan ge en fullständig axiomatisk formalisering av den klassiska eller intuitionistiska metodens propositionella eller predikatlogik, till nästan vilken modal logik som helst och till många substrukturella logiker som relevant eller linjär logik. Det är faktiskt ganska svårt att hitta en logik som inte kunde representeras i någon av dessa kalkyler.

Konsistensbevis

Som redan nämnts var drivkraften för det matematiska studiet av bevis i formella teorier Hilberts program. Den centrala idén med detta program var att om vi kunde ge ändliga (ändliga) bevis på överensstämmelsen hos alla exakta formella teorier som behövs av matematiker, så kunde vi motivera dessa teorier med ett metamatematiskt argument som visar att alla deras universella (allmänt giltiga) påståenden (tekniskt sett deras bevisbara meningar) är ändligt sanna; Så när de väl är motiverade bryr vi oss inte längre om de icke-ändliga implikationerna av deras existentiella satser, och betraktar dem som pseudo-meningsfulla konventioner om existensen av idealiska enheter.

Misslyckandet i programmet orsakades av K. Gödels ofullständighetsteorem, som visade att någon teori, stark nog att uttrycka enkla aritmetiska sanningar, inte kan bevisa sin egen konsistens. Sedan dess har det gjorts mycket forskning kring detta ämne och resultat har erhållits som framför allt ger: försvagar konsekvenskravet; axiomatisering av kärnan i Gödels resultat i termer av modalt språk, bevisbarhetslogik; transfinit iteration av teorier enligt A. Turing och S. Feferman ; den senaste upptäckten av självtestande teorier – system starka nog att hävda sig men för svaga mot det diagonala argumentet , Gödels nyckelargument för obevisbarhet.

Strukturell bevisteori

Strukturell bevisteori är en gren av bevisteori som studerar de beviskalkyler som stöder begreppet analytiskt bevis . Begreppet analytiskt bevis introducerades av Gentzen för kalkylen av sekvenser. Hans kalkyl för naturlig deduktion stöder också begreppet analytiskt bevis. Vi säger att analytiska bevis är normala former, relaterade till föreställningen om en normal form i termomskrivningssystem. Mer exotiska beviskalkyler, som I. Giros bevisnätverk, stödjer också begreppet analytiskt bevis.

Strukturell bevisteori är relaterad till typteori genom Curry-Howard-korrespondensen, som bygger på den strukturella analogin mellan normaliseringsprocessen i naturlig deduktionskalkyl och beta-reduktionen av typad lambda-kalkyl . Denna korrespondens utgör grunden för den intuitionistiska typteori som utvecklats av M.-Lef, och utvidgas ofta till trepartskorrespondensen, vars tredje stöd är kartesiska slutna kategorier.

Bevisteoretisk semantik

Lingvistik, logisk typ grammatik, kategorisk grammatik och Montagu grammatik använder formalism baserad på strukturell bevisteori för att ge formell semantik till naturligt språk.

Tabellsystem

Analytiska tabeller använder den centrala idén med analytiskt bevis från strukturell bevisteori för att tillhandahålla upplösningsprocedurer för ett brett spektrum av logiker.

Ordinalanalys

Många tillräckligt uttrycksfulla formella teorier kan förknippas med deras karakteristiska ordinal, känd som teorins bevisteoretiska ordinal . Ordinalanalys är ett fält vars ämne är beräkningen av bevisteoretiska ordtal av teorier.

G. Gentzen beräknade ordinalen av första ordningens Peano-aritmetik  - han fastställde att konsistens kan bevisas genom transfinit induktion till ordningen . Ytterligare undersökningar visade att principen för transfinit induktion visar sig för ordinaler som är mindre än , men inte för ordinalen själv , och att beräkningsbara funktioner, överallt - vars bestämdhet kan bevisas i , sammanfaller med -rekursiva funktioner. Även om, i det allmänna fallet, för andra teorier, analoger av dessa resultat inte behöver äga rum samtidigt för samma ordinal, för naturliga tillräckligt starka teorier, ger analoger av dessa resultat som regel inte olika ordinal för samma teori (liksom andra förhållningssätt till definitionen av en bevisteoretisk ordinal).

Bevisteoretiska ordtal har beräknats för ett antal fragment av andra ordningens aritmetik och förlängningar av Kripke-Platek mängdlära. Frågan om att beräkna den bevisteoretiska ordinalen för fullständig andra ordningens aritmetik och starkare teorier, i synnerhet Zermelo-Fraenkels mängdteorin , är fortfarande öppen.

Analys av bevisets logik (substrukturell logik)

Flera viktiga logiker härleds från övervägande av den logiska struktur som uppstår i strukturell bevisteori.

Se även

• Modellteori
• Bevis (sant)
• Metoder för bevis
• Mellanlogik

Länkar

1. Hao Wang (1981) Populära föreläsningar om matematisk logik. ISBN 0-442-23109-1 .
2. D. Barwise (red., 1978). Handbook of Mathematical Logic, vols. fjorton.
3. G. Takeuchi. Bevisteorin. M., Mir, 1978
4. A. Troelstra (1996). Grundläggande bevisteori. I serien: Cambridge Treatises on Theoretical Computer Science, University of Cambridge, ISBN 0-521-77911-1 .
5. D. von Plateau (2008). Utveckling av bevisteori. Stanford Encyclopedia of Philosophy.

Anteckningar

1. ↑ Eg, Wang (1981), s. 3-4 och Barwise (1978).
2. ↑ Proof Theory, 1978 , sid. 5.

Litteratur

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

Ordböcker och uppslagsverk	Universalis Universalis
I bibliografiska kataloger BNF : 122670310 J9U : 987007541259805171 LCCN : sh85107437 , sh85107437 LNB : 000137654 NDL : 01190375 NKC : ph126551