Bevissteori - Proof theory

Bevissteori är en viktig gren av matematisk logik som representerar bevis som formella matematiska objekt , vilket underlättar deras analys med matematiska tekniker. Bevis presenteras vanligtvis som induktivt definierade datastrukturer som vanliga listor, boxade listor eller träd , som är konstruerade enligt axiomen och slutsatsreglerna för det logiska systemet. Som sådan är bevisteorin syntaktisk till sin natur, till skillnad från modellteorin , som är semantisk till sin natur.

Några av de viktigaste områdena för bevisteori inkluderar strukturell bevisteori , ordinalanalys , bevisbarhetslogik , omvänd matematik , bevisbrytning , automatiserad teorem bevisning och beviskomplexitet . Mycket forskning fokuserar också på applikationer inom datavetenskap, lingvistik och filosofi.

Historia

Även om formaliseringen av logiken var mycket avancerad av arbetet med sådana personer som Gottlob Frege , Giuseppe Peano , Bertrand Russell och Richard Dedekind , ses historien om modern bevisteori ofta som etablerad av David Hilbert , som initierade det som kallas Hilberts programmet i matematikens grunder . Den centrala tanken med detta program var att om vi kunde ge slutliga bevis på konsekvens för alla sofistikerade formella teorier som matematiker behöver, så kunde vi grunda dessa teorier med hjälp av ett metamatematiskt argument, som visar att alla deras rent universella påståenden (mer tekniskt sett är deras bevisbara meningar ) slutligen sanna; en gång så grundade bryr vi oss inte om den icke-slutliga innebörden av deras existentiella satser, betraktar dessa som pseudobetydliga villkor för existensen av ideala enheter. ${\ displaystyle \ Pi _ {1}^{0}}$

Misslyckandet av programmet framkallades av Kurt Gödel 's ofullständig satser , som visade att alla ω-konsekvent teori som är tillräckligt stark för att uttrycka vissa enkla aritmetiska sanningar, inte kan bevisa sin egen konsistens, som på Gödels formulering är en mening. Ändrade versioner av Hilberts program uppstod dock och forskning har gjorts om relaterade ämnen. Detta har särskilt lett till: ${\ displaystyle \ Pi _ {1}^{0}}$

• Förfining av Gödels resultat, särskilt J. Barkley Rossers förfining, vilket försvagar kravet på ω-konsistens ovan till enkel konsistens;
• Axiomatisering av kärnan i Gödels resultat när det gäller ett modalt språk, bevisbarhetslogik ;
• Transfinite iteration av teorier, på grund av Alan Turing och Solomon Feferman ;
• Upptäckten av självverifierande teorier , system som är tillräckligt starka för att prata om sig själva, men för svaga för att genomföra det diagonala argumentet som är nyckeln till Gödels oprovabilitetsargument.

Parallellt med uppkomsten och nedgången av Hilberts program grundades grunden för strukturell bevisteori . Jan Łukasiewicz föreslog 1926 att man kunde förbättra Hilberts system som grund för den axiomatiska presentationen av logik om man tillät att dra slutsatser från antaganden i logikens slutsatser. Som svar på detta gav Stanisław Jaśkowski (1929) och Gerhard Gentzen (1934) oberoende sådana system, kallade beräkningar av naturligt avdrag , med Gentzens tillvägagångssätt som introducerade symmetriidén mellan grunderna för att hävda propositioner, uttryckta i introduktionsregler , och konsekvenserna att acceptera påståenden i eliminationsreglerna , en idé som har visat sig vara mycket viktig inom bevisteorin. Gentzen (1934) introducerade vidare idén om den efterföljande kalkylen , en beräkning som utvecklats i en liknande anda som bättre uttryckte dualiteten i de logiska anslutningarna, och fortsatte med att göra grundläggande framsteg i formaliseringen av den intuitionistiska logiken och ge det första kombinatoriska beviset av Peano -aritmetikens konsistens . Tillsammans presenterade presentationen av naturligt avdrag och den efterföljande beräkningen den grundläggande idén om analytiskt bevis till bevisteori.

Strukturell bevisteori

Strukturell bevisteori är den subdisciplin av bevisteori som studerar detaljerna i bevisberäkningar . De tre mest kända stilarna för provkalkyler är:

• Den Hilbert calculi
• Den naturliga avdragsberäkningen
• Den Sequent calculi

Var och en av dessa kan ge en fullständig och axiomatisk formalisering av propositional eller predikatlogik för antingen den klassiska eller intuitionistiska smaken, nästan vilken modal logik som helst och många substrukturella logiker , såsom relevanslogik eller linjär logik . Det är faktiskt ovanligt att hitta en logik som motstår att representeras i en av dessa beräkningar.

Bevissteoretiker är vanligtvis intresserade av bevisberäkningar som stöder en uppfattning om analytiskt bevis . Begreppet analytiskt bevis infördes av Gentzen för den efterföljande beräkningen; där är de analytiska bevisen de som är avskurna . Mycket av intresset för skärfria bevis kommer från egenskapen subformel: varje formel i slutet av ett klippfritt bevis är en underformel för en av lokalerna. Detta gör att man enkelt kan visa konsekvensen i den sekventiella beräkningen; om den tomma sekvensen var härledbar skulle det behöva vara en subformel med någon förutsättning, vilket den inte är. Gentzens mittföljande sats, Craig-interpoleringssatsen och Herbrands teorem följer också som en följd av cut-eliminationssatsen.

Gentzens naturliga avdragsberäkning stöder också en uppfattning om analytiskt bevis, vilket visas av Dag Prawitz . Definitionen är något mer komplex: vi säger att de analytiska bevisen är de normala formerna , som är relaterade till begreppet normal form vid termskrivning. Mer exotiska säkra calculi såsom Jean-Yves Girard : s bevis nät stöder också en föreställning om analytisk bevis.

En särskild familj av analytiska bevis som uppstår i reduktiv logik är fokuserade bevis som kännetecknar en stor familj av målinriktade provsökningsförfaranden. Möjligheten att omvandla ett bevissystem till en fokuserad form är en bra indikation på dess syntaktiska kvalitet, på ett sätt som liknar hur tillåtet snitt visar att ett provsystem är syntaktiskt konsekvent.

Strukturell bevisteori är kopplad till typteori med hjälp av Curry -Howard -korrespondensen , som observerar en strukturell analogi mellan normaliseringsprocessen i den naturliga avdragsberäkningen och betareduktionen i den typade lambda -kalkylen . Detta utgör grunden för den intuitionistiska teorin som utvecklats av Per Martin-Löf och utvidgas ofta till en trevägskorrespondens, vars tredje ben är de kartesiska slutna kategorierna .

Andra forskningsämnen inom strukturteori inkluderar analytisk tablå, som tillämpar den centrala idén om analytisk bevisning från strukturell bevisteori för att tillhandahålla beslutsförfaranden och semi-beslutsförfaranden för ett brett spektrum av logiker och bevisteorin för substrukturella logiker.

Ordinarie analys

Ordinalanalys är en kraftfull teknik för att tillhandahålla kombinatoriska konsistensbevis för undersystem av aritmetik, analys och uppsättningsteori. Gödels andra ofullständighetsteorem tolkas ofta som att det visar att finitistiska konsistensbevis är omöjliga för teorier om tillräcklig styrka. Ordinalanalys gör att man kan mäta exakt det oändliga innehållet i teorins konsistens. För en konsekvent rekursivt axiomatiserad teori T kan man i finitistisk aritmetik bevisa att en viss transfinit ordinals välgrundande implicerar konsistensen i T. Godels andra ofullständighetsteorem innebär att en sådan ordals välgrundade grund inte kan bevisas i teorin T.

Konsekvenserna av ordinalanalys inkluderar (1) konsistens av delsystem av klassisk andra ordnings aritmetik och uppsättningsteori i förhållande till konstruktiva teorier, (2) kombinatoriska oberoende resultat och (3) klassificeringar av bevisligen totala rekursiva funktioner och bevisligen välgrundade ordinaler.

Ordinalanalysen härstammade från Gentzen, som bevisade att Peano Arithmetic var konsekvent med hjälp av transfinit induktion upp till ordinal ε ₀ . Ordinalanalys har utvidgats till många fragment av första och andra ordningens aritmetik och uppsättningsteori. En stor utmaning har varit den ordinarie analysen av impredikativa teorier. Det första genombrottet i denna riktning var Takeutis bevis på konsistensen av Π¹
₁-CA ₀ med metoden för ordinaldiagram.

Tillgänglighet logik

Tillgänglighetslogik är en modal logik , där boxoperatören tolkas som 'det kan bevisas att'. Poängen är att fånga uppfattningen om ett bevispredikat för en någorlunda rik formell teori . Som grundläggande axiom för provbarhetslogiken GL ( Gödel - Löb ), som fångar bevisbara i Peano Arithmetic , tar man modala analoger av Hilbert -Bernays härledningsförhållanden och Löbs sats (om det är bevisbart att bevisningen av A innebär A, då A är bevisbart).

Några av de grundläggande resultaten rörande ofullständigheten i Peano Arithmetic och relaterade teorier har analoger i bevisbarhetslogik. Till exempel är det en sats i GL att om en motsägelse inte kan bevisas så är det inte bevisbart att en motsägelse inte är bevisbar (Gödels andra ofullständighetssats). Det finns också modala analoger av fixpunktssatsen. Robert Solovay bevisade att den modala logiken GL är komplett med avseende på Peano Arithmetic. Det vill säga den propositionella teorin om bevisbarhet i Peano Arithmetic representeras helt av den modala logiken GL. Detta innebär helt enkelt att propositionella resonemang om bevisbarhet i Peano Arithmetic är fullständiga och avgörbara.

Annan forskning om provbarhetslogik har fokuserat på första ordningens provbarhetslogik, polymodal provbarhetslogik (med en modalitet som representerar bevisbarhet i objektteorin och en annan som representerar bevisbarhet i metateorin) och tolkbarhetslogik avsedd att fånga interaktionen mellan bevisbarhet och tolkbarhet . Viss mycket ny forskning har involverat tillämpningar av graderade provbarhetsalgebror till ordinalanalys av aritmetiska teorier.

Omvänd matematik

Omvänd matematik är ett program i matematisk logik som försöker bestämma vilka axiom som krävs för att bevisa matematikens satser. Fältet grundades av Harvey Friedman . Dess definierande metod kan beskrivas som att "gå bakåt från satserna till axiomen ", i motsats till den vanliga matematiska praxis att härleda satser från axiom. Det omvända matematikprogrammet förskuggades av resultat i uppsättningsteori, till exempel den klassiska satsen att valets axiom och Zorns lemma är likvärdiga med ZF -uppsättningsteorin . Målet med omvänd matematik är dock att studera möjliga axiom för vanliga matematiska satser snarare än möjliga axiom för uppsättningsteori.

I omvänd matematik börjar man med ett ramspråk och en grundteori - ett kärnaxiomsystem - som är för svagt för att bevisa de flesta satser man kan vara intresserad av, men ändå kraftfull nog att utveckla de definitioner som är nödvändiga för att ange dessa satser. Till exempel, för att studera satsen "Varje begränsad sekvens av reella tal har ett överordnat " är det nödvändigt att använda ett grundsystem som kan tala om reella tal och sekvenser av reella tal.

För varje sats som kan anges i bassystemet men som inte kan bevisas i bassystemet, är målet att bestämma det specifika axiomsystemet (starkare än bassystemet) som är nödvändigt för att bevisa att satsen. För att visa att ett system S krävs för att bevisa en sats T krävs två bevis. Det första beviset visar att T kan bevisas från S ; detta är en vanlig matematiska bevis tillsammans med en motivering att den kan utföras i systemet S . Det andra beviset, känt som en omvändning , visar att T själv innebär S ; detta bevis utförs i bassystemet. Reverseringsfastställer att ingen axiom systemet S ' som sträcker bassystemet kan vara svagare än S samtidigt bevisar  T .

Ett slående fenomen i omvänd matematik är robustheten hos de fem stora axiomsystemen. För att öka styrkan namnges dessa system av initialismen RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ och Π¹
₁-CA ₀ . Nästan varje sats i vanlig matematik som har matematiskt analyserats omvänd har visat sig motsvara ett av dessa fem system. Mycket ny forskning har fokuserat på kombinatoriska principer som inte passar in i denna ram, som RT²
₂ (Ramseys sats för par).

Forskning i omvänd matematik innehåller ofta metoder och tekniker från såväl rekursionsteori som bevisteori.

Funktionella tolkningar

Funktionella tolkningar är tolkningar av icke-konstruktiva teorier i funktionella. Funktionella tolkningar fortsätter vanligtvis i två steg. Först "reducerar" man en klassisk teori C till en intuitionistisk I. Det vill säga man tillhandahåller en konstruktiv kartläggning som översätter C -satserna till I. teorier. För det andra reducerar man den intuitionistiska teorin I till en kvantifieringsfri teori om functionals F. Dessa tolkningar bidrar till en form av Hilberts program, eftersom de bevisar att klassiska teorier är konsekventa i förhållande till konstruktiva. Framgångsrika funktionstolkningar har gett minskningar av infinitära teorier till finitära teorier och impredikerande teorier till predikativa teorier.

Funktionella tolkningar ger också ett sätt att extrahera konstruktiv information från bevis i den reducerade teorin. Som en direkt följd av tolkningen får man vanligtvis resultatet att varje rekursiv funktion vars totalitet kan bevisas antingen i I eller i C representeras av en term av F. Om man kan tillhandahålla en ytterligare tolkning av F i I, vilket ibland är möjligt, är denna karakterisering i själva verket oftast visad att vara exakt. Det visar sig ofta att villkoren för F sammanfaller med en naturlig klass av funktioner, till exempel de primitiva rekursiva eller polynomiska beräkningsbara funktionerna. Funktionella tolkningar har också använts för att tillhandahålla ordinarie analyser av teorier och klassificera deras bevisligen rekursiva funktioner.

Studiet av funktionella tolkningar började med Kurt Gödels tolkning av intuitionistisk aritmetik i en kvantifieringsfri teori om funktionaliteter av ändlig typ. Denna tolkning är allmänt känd som Dialectica -tolkningen . Tillsammans med dubbelnegationstolkningen av klassisk logik i intuitionistisk logik, ger den en minskning av klassisk aritmetik till intuitionistisk aritmetik.

Formellt och informellt bevis

De informella bevisen för daglig matematisk praxis är till skillnad från de formella bevisen för bevisteori. De är snarare som skisser på hög nivå som gör det möjligt för en expert att rekonstruera ett formellt bevis åtminstone i princip, med tillräckligt med tid och tålamod. För de flesta matematiker är det för pedantiskt och långdraget att skriva ett fullständigt formellt bevis för att vara vanligt.

Formella bevis skapas med hjälp av datorer i interaktivt teorem som bevisar . Betydligt kan dessa bevis kontrolleras automatiskt, även med dator. Att kontrollera formella bevis är vanligtvis enkelt, medan det i allmänhet är svårt att hitta bevis ( automatiserad teorem bevis ). Ett informellt bevis i matematiklitteraturen kräver däremot att veckors granskning kontrolleras och kan fortfarande innehålla fel.

Bevissteoretisk semantik

I lingvistik , typ-logiska grammatik , categorial grammatik och Montague grammatik gäller formalismer baserade på strukturella bevis teori för att ge en formell naturligt språk semantik .

Se även

• Mellanlig logik
• Modellteori
• Bevis (sanning)
• Bevissteknik
• Sekvensberäkning

Anteckningar

Referenser

• J. Avigad och EH Reck (2001). "'Förtydligande av det oändliga': utvecklingen av metamatematik och bevisteori ". Carnegie-Mellons tekniska rapport CMU-PHIL-120.
• J. Barwise , red. (1978). Handbok i matematisk logik . Nord-Holland.
• S. Buss, red. (1998) Handbook of Proof Theory . Elsevier.
• AS Troelstra och H. Schwichtenberg (1996). Basic Proof Theory , Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN  0-521-77911-1 .
• G. Gentzen (1935/1969). " Undersökningar av logiskt avdrag ". I ME Szabo, red. Samlade papper av Gerhard Gentzen . Nord-Holland. Översatt av Szabo från "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift v. 39, s. 176–210, 405 431.
• D. Prawitz (1965). Naturligt avdrag: En bevisteoretisk studie , Dover Publications, ISBN  978-0-486-44655-4
• SG Simpson (2010). Delsystem av andra ordningens aritmetik , andra upplagan. Cambridge University Press, ISBN  978-0521150149 .
• H. Wang (1981). Populära föreläsningar om matematisk logik , Van Nostrand Reinhold Company , ISBN  0-442-23109-1 .

externa länkar

• "Proof theory" , Encyclopedia of Mathematics , EMS Press , 2001 [1994]
• J. von Plato (2008). Utvecklingen av bevisteori . Stanford Encyclopedia of Philosophy .