Algoritmisk afgørelighed er en egenskab ved en formel teori til at have en algoritme , der bestemmer ved en given formel , om den kan afledes fra sættet af aksiomer i den givne teori eller ej. En teori siges at være afgørelig , hvis en sådan algoritme eksisterer, og uafgørlig ellers. Spørgsmålet om deducerbarhed i formel teori er et særligt, men samtidig det vigtigste tilfælde af et mere generelt problem med afgørelighed .
Begreberne algoritme og aksiomatisk system har en lang historie. Begge har været kendt siden antikken . Det er tilstrækkeligt at huske postulaterne af Euklids geometri og algoritmen til at finde den største fælles divisor for den samme Euklid. På trods af dette eksisterede en klar matematisk definition af calculus og især algoritmen ikke i meget lang tid. Det særlige ved problemet forbundet med den formelle definition af uafgørelighed var, at for at vise, at der eksisterer en eller anden algoritme, er det nok bare at finde og demonstrere det. Hvis algoritmen ikke findes, er det muligt, at den ikke eksisterer, og så skal dette strengt bevises. Og til dette skal du vide præcis, hvad en algoritme er.
Store fremskridt i formaliseringen af disse begreber blev opnået i begyndelsen af det 20. århundrede af Hilbert og hans skole. Derefter blev først begreberne calculus og formel afledning dannet, og derefter satte Hilbert i sit berømte program for at underbygge matematik det ambitiøse mål at formalisere hele matematikken. Programmet gav blandt andet mulighed for automatisk at kontrollere enhver matematisk formel for sandhed. Baseret på Hilberts arbejde beskrev Gödel først en klasse af såkaldte rekursive funktioner , hvormed han beviste sine berømte ufuldstændighedsteoremer . Efterfølgende blev der introduceret en række andre formalismer, såsom Turing-maskinen , λ-calculus , der viste sig at svare til rekursive funktioner. Hver af disse betragtes nu som den formelle ækvivalent til den intuitive forestilling om en beregnelig funktion. Denne ækvivalens postuleres af Kirkens afhandling .
Da begreberne calculus og algoritme blev forfinet, fulgte en række resultater om uafgøreligheden af forskellige teorier. Et af de første sådanne resultater var en sætning bevist af Novikov om uløseligheden af problemet med ord i grupper . Afgørlige teorier var kendt længe før det.
Intuitivt gælder det, at jo mere kompleks og udtryksfuld teorien er, jo større er chancen for, at den viser sig at være uafklarelig. Derfor er en "uafgørlig teori" groft sagt en "kompleks teori".
Formel beregning i det generelle tilfælde skal definere sproget , reglerne for konstruktion af udtryk og formler , aksiomer og inferensregler. For hver sætning T er det således altid muligt at konstruere en kæde A 1 , A 2 , … , A n = T , hvor hver formel A i enten er et aksiom eller kan udledes af de foregående formler ifølge en af afledningerne regler. Opløselighed betyder, at der er en algoritme, der for hver velformet sætning T i en endelig tid giver et entydigt svar: ja, denne sætning kan udledes inden for kalkulationens rammer eller ej, den er ikke afledbar.
Det er indlysende, at den modstridende teori kan afgøres, da enhver formel vil kunne udledes. På den anden side, hvis en kalkulus ikke har et rekursivt optalbart sæt af aksiomer, såsom andenordens logik , kan det naturligvis ikke afgøres.
Afgørelighed er en meget stærk egenskab, og de fleste nyttige og praktiske teorier har den ikke. I forbindelse hermed blev der indført en svagere forestilling om semidecidability . Semi-afgørlig betyder at have en algoritme, der altid vil bekræfte i en begrænset tid, at sætningen er sand, hvis den er sand, men hvis den ikke er det, kan den køre i det uendelige.
Kravet om semidecidability svarer til at være i stand til effektivt at opregne alle sætningerne i en given teori. Med andre ord skal sættet af sætninger være rekursivt talbare . De fleste teorier, der anvendes i praksis, opfylder dette krav.
Effektive semi-permissive procedurer for første-ordens logik er af stor praktisk betydning, da de tillader en (semi)automatisk at bevise formaliserede udsagn af en meget bred klasse. Et gennembrud på dette område var Robinsons opdagelse af opløsningsmetoden i 1965 .
I matematisk logik bruges traditionelt to begreber om fuldstændighed: egentlig fuldstændighed og fuldstændighed med hensyn til en eller anden klasse af fortolkninger (eller strukturer). I det første tilfælde er en teori komplet, hvis hver sætning i den er enten sand eller falsk. I det andet tilfælde, hvis en sætning, der er sand under alle fortolkninger fra den givne klasse, kan udledes.
Begge begreber er tæt forbundet med afgørelighed. For eksempel, hvis sættet af aksiomer for en komplet første-ordensteori er rekursivt talværdigt, så kan det afgøres. Dette følger af Posts berømte sætning , der siger, at hvis et sæt og dets komplement begge er rekursivt talbare, så kan de også bestemmes . Intuitivt er argumentet, der viser sandheden af ovenstående udsagn, følgende: hvis teorien er komplet, og sættet af dens aksiomer er rekursivt talrige, så er der semipermissive procedurer til at teste sandheden af ethvert udsagn, såvel som dets negation. Hvis du kører begge disse procedurer parallelt , så, i betragtning af teoriens fuldstændighed, bør en af dem en dag stoppe og give et positivt svar.
Hvis teorien er komplet med hensyn til en eller anden klasse af fortolkninger, kan denne bruges til at konstruere en beslutningsprocedure. For eksempel er propositionel logik komplet med hensyn til fortolkning på sandhedstabeller . Derfor vil konstruktionen af en sandhedstabel ifølge denne formel være et eksempel på en løsningsalgoritme for propositionel logik.