Algoritmisk avgörbarhet är en egenskap hos en formell teori att ha en algoritm som avgör med en given formel huruvida den kan härledas från uppsättningen av axiom för den givna teorin eller inte. En teori sägs vara avgörbar om en sådan algoritm existerar, och oavgörbar annars. Frågan om deducerbarhet i formell teori är ett särskilt, men samtidigt det viktigaste fallet av ett mer generellt problem med beslutbarhet .
Begreppen algoritm och axiomatiska system har en lång historia. Båda har varit kända sedan antiken . Det räcker med att påminna om postulaten av Euklids geometri och algoritmen för att hitta den största gemensamma divisorn för samma Euklid. Trots detta fanns det inte en tydlig matematisk definition av kalkyl och speciellt algoritmen på väldigt länge. Det speciella med problemet i samband med den formella definitionen av obestämbarhet var att för att visa att någon algoritm existerar räcker det bara att hitta och demonstrera den. Om algoritmen inte hittas är det möjligt att den inte existerar, och då måste detta noggrant bevisas. Och för detta måste du veta exakt vad en algoritm är.
Stora framsteg i formaliseringen av dessa begrepp uppnåddes i början av 1900-talet av Hilbert och hans skola. Sedan bildades först begreppen kalkyl och formell härledning, och sedan satte Hilbert, i sitt berömda program för att underbygga matematik , det ambitiösa målet att formalisera all matematik. Programmet gav bland annat möjlighet att automatiskt kontrollera vilken matematisk formel som helst för sanning. Baserat på Hilberts arbete beskrev Gödel först en klass av så kallade rekursiva funktioner , med vilka han bevisade sina berömda ofullständighetsteorem . Därefter introducerades en rad andra formalismer, som Turingmaskinen , λ-kalkyl , som visade sig vara likvärdig med rekursiva funktioner. Var och en av dessa anses nu vara den formella motsvarigheten till den intuitiva uppfattningen om en beräkningsbar funktion. Denna likvärdighet postuleras av kyrkans avhandling .
När begreppen kalkyl och algoritm förfinades följde en rad resultat om olika teoriers obestämbarhet. En av de första sådana resultat var ett teorem bevisat av Novikov om olösligheten av problemet med ord i grupper . Avgörbara teorier var kända långt innan dess.
Intuitivt, ju mer komplex och uttrycksfull teorin är, desto större är chansen att den kommer att visa sig vara obestämbar. Därför, grovt sett, är en "oavgörlig teori" en "komplex teori".
Formell kalkyl i det allmänna fallet måste definiera språket , reglerna för att konstruera termer och formler , axiomen och reglerna för slutledning. För varje teorem T är det alltså alltid möjligt att konstruera en kedja A 1 , A 2 , … , An = T , där varje formel A i antingen är ett axiom eller kan härledas från de föregående formlerna enligt en av härledningarna regler. Upplösningsförmåga innebär att det finns en algoritm som för varje välformad mening T i en ändlig tid ger ett entydigt svar: ja, denna mening är härledbar inom ramen för kalkylen eller inte, den är inte härledbar.
Det är uppenbart att den motsägelsefulla teorin kan avgöras, eftersom vilken formel som helst kommer att kunna härledas. Å andra sidan, om en kalkyl inte har en rekursivt uppräknad uppsättning axiom, såsom andra ordningens logik , kan den uppenbarligen inte avgöras.
Beslutbarhet är en mycket stark egenskap, och de flesta användbara och praktiska teorier har det inte. I samband med detta infördes en svagare föreställning om halvavgörbarhet . Semi-beslutbar betyder att ha en algoritm som alltid kommer att bekräfta inom en begränsad tid att meningen är sann om den är sann, men om den inte är det kan den köras i all oändlighet.
Kravet på halvavgörbarhet är likvärdigt med att effektivt kunna räkna upp alla satser i en given teori. Med andra ord måste uppsättningen av satser vara rekursivt uppräknad . De flesta teorier som används i praktiken uppfyller detta krav.
Effektiva semi-permissiva procedurer för första ordningens logik är av stor praktisk betydelse, eftersom de tillåter en att (halv)automatiskt bevisa formaliserade påståenden av en mycket bred klass. Ett genombrott på detta område var Robinsons upptäckt av upplösningsmetoden 1965 .
Inom matematisk logik används traditionellt två begrepp om fullständighet: korrekt fullständighet och fullständighet med avseende på någon klass av tolkningar (eller strukturer). I det första fallet är en teori komplett om varje mening i den är antingen sann eller falsk. I det andra fallet, om någon mening som är sann under alla tolkningar från den givna klassen är härledbar.
Båda begreppen är nära besläktade med beslutbarhet. Till exempel, om uppsättningen av axiom för en komplett första ordningens teori är rekursivt uppräknad, då är den avgörbar. Detta följer av Posts berömda teorem , som säger att om en mängd och dess komplement är båda rekursivt uppräknade, så är de också avgörbara . Intuitivt är argumentet som visar sanningen i ovanstående påstående följande: om teorin är komplett och uppsättningen av dess axiom är rekursivt uppräknad, så finns det semipermissiva procedurer för att testa sanningen av varje påstående, såväl som dess negation. Om du kör båda dessa procedurer parallellt , då, med tanke på teorins fullständighet, borde en av dem någon gång stanna upp och ge ett positivt svar.
Om teorin är komplett med avseende på någon klass av tolkningar, kan denna användas för att konstruera ett beslutsförfarande. Till exempel är propositionell logik komplett med avseende på tolkning på sanningstabeller . Därför kommer konstruktionen av en sanningstabell enligt denna formel att vara ett exempel på en lösningsalgoritm för propositionell logik.