Algoritminen ratkeavuus on muodollisen teorian ominaisuus, että sillä on algoritmi , joka määrittää tietyllä kaavalla , onko se johdettavissa tietyn teorian aksioomien joukosta vai ei. Teorian sanotaan olevan päätettävissä , jos tällainen algoritmi on olemassa, ja muutoin ratkaisemattomaksi . Kysymys johdettavuudesta muodollisessa teoriassa on erityinen, mutta samalla tärkein tapaus yleisemmässä päätettävyysongelmassa .
Algoritmin ja aksiomaattisen järjestelmän käsitteillä on pitkä historia. Molemmat ovat olleet tunnettuja antiikista lähtien . Riittää, kun muistetaan Euklidesin geometrian postulaatit ja algoritmi saman Eukleideen suurimman yhteisen jakajan löytämiseksi. Tästä huolimatta selkeää matemaattista määritelmää laskennalle ja erityisesti algoritmille ei ollut olemassa kovin pitkään. Ratkaisemattomuuden muodolliseen määritelmään liittyvän ongelman erikoisuus oli, että jonkin algoritmin olemassaolon osoittamiseksi riittää sen löytäminen ja esittely. Jos algoritmia ei löydy, on mahdollista, että sitä ei ole olemassa, ja sitten tämä on todistettava tiukasti. Ja tätä varten sinun on tiedettävä tarkalleen, mikä algoritmi on.
Hilbert ja hänen koulunsa saavuttivat suurta edistystä näiden käsitteiden virallistamisessa 1900-luvun alussa. Sitten ensin muodostettiin laskennan ja muodollisen johtamisen käsitteet, ja sitten Hilbert asetti kuuluisassa matematiikan perusteluohjelmassaan kunnianhimoiseksi tavoitteeksi formalisoida koko matematiikan. Ohjelma tarjosi muun muassa mahdollisuuden tarkistaa automaattisesti minkä tahansa matemaattisen kaavan totuuden. Hilbertin työn perusteella Gödel kuvasi ensin luokan niin kutsuttuja rekursiivisia funktioita , joilla hän todisti kuuluisat epätäydellisyyslauseensa . Myöhemmin otettiin käyttöön joukko muita formalismeja, kuten Turingin kone , λ-laskenta , joka osoittautui vastaavaksi rekursiivisia funktioita. Kutakin näistä pidetään nyt muodollisena vastineena laskettavan funktion intuitiiviselle käsitteelle. Tämän vastaavuuden olettaa Churchin teesi .
Kun laskennan ja algoritmin käsitteitä jalostettiin, seurasi sarja tuloksia eri teorioiden päättämättömyydestä. Yksi ensimmäisistä tällaisista tuloksista oli Novikovin todistama lause ryhmien sanojen ongelman ratkaisemattomuudesta . Ratkaisevia teorioita tunnettiin kauan ennen sitä.
Intuitiivisesti mitä monimutkaisempi ja ilmeisempi teoria on, sitä suurempi on mahdollisuus, että se osoittautuu ratkaisemattomaksi. Siksi karkeasti sanottuna "päättämätön teoria" on "monimutkainen teoria".
Muodollisen laskennan on yleensä määriteltävä kieli , termien ja kaavojen muodostamissäännöt, aksioomit ja päättelysäännöt. Siten jokaiselle lauseelle T on aina mahdollista rakentaa ketju A 1 , A 2 , … , A n = T , jossa jokainen kaava A i on joko aksiooma tai se voidaan johtaa edellisistä kaavoista jonkin johdosta säännöt. Ratkaisevuus tarkoittaa, että on olemassa algoritmi, joka jokaiselle hyvin muodostetulle lauseelle T äärellisessä ajassa antaa yksiselitteisen vastauksen: kyllä, tämä lause on johdettavissa laskennan puitteissa vai ei, se ei ole johdettavissa.
On selvää, että ristiriitainen teoria on päätettävissä, koska mikä tahansa kaava on johdettavissa. Toisaalta, jos laskulla ei ole rekursiivisesti numeroitavaa aksioomijoukkoa, kuten toisen asteen logiikka , se ei tietenkään voi olla pääteltävissä.
Päättävyys on erittäin vahva ominaisuus, ja useimmissa hyödyllisissä ja käytännöllisissä teorioissa sitä ei ole. Tämän yhteydessä otettiin käyttöön heikompi käsite semidecidability . Puoliratkettava tarkoittaa, että on algoritmi, joka aina vahvistaa äärellisessä ajassa, että lause on tosi, jos se on totta, mutta jos se ei ole totta, se voi toimia loputtomiin.
Puolitarkkuuden vaatimus vastaa kykyä laskea tehokkaasti kaikki tietyn teorian lauseet. Toisin sanoen lauseiden joukon on oltava rekursiivisesti numeroituva . Suurin osa käytännössä käytetyistä teorioista täyttää tämän vaatimuksen.
Tehokkaat puoli-permissiiviset proseduurit ensimmäisen asteen logiikkaa varten ovat käytännönläheisiä, koska niiden avulla voidaan (puoli)automaattisesti todistaa formalisoidut lausunnot erittäin laajasta luokkasta. Läpimurto tällä alalla oli Robinsonin vuonna 1965 löytämä resoluutiomenetelmä .
Matemaattisessa logiikassa käytetään perinteisesti kahta täydellisyyden käsitettä: varsinainen täydellisyys ja täydellisyys suhteessa johonkin tulkintojen (tai rakenteiden) luokkaan. Ensimmäisessä tapauksessa teoria on täydellinen, jos jokainen sen lause on joko tosi tai epätosi. Toisessa tapauksessa, jos jokin lause, joka on tosi kaikkien tulkintojen mukaan annetusta luokasta, on johdettavissa.
Molemmat käsitteet liittyvät läheisesti päätettävyyteen. Esimerkiksi jos täydellisen ensimmäisen asteen teorian aksioomien joukko on rekursiivisesti numeroituva, niin se on päätettävissä. Tämä seuraa Postin kuuluisasta lauseesta , jonka mukaan jos joukko ja sen komplementti ovat molemmat rekursiivisesti numeroituvia, ne ovat myös päätettävissä . Intuitiivisesti argumentti, joka osoittaa yllä olevan väitteen totuuden, on seuraava: jos teoria on täydellinen ja sen aksioomien joukko on rekursiivisesti luettavissa, niin minkä tahansa väitteen totuuden testaamiseen on olemassa semipermissive-menettelyjä, kuten myös sen kieltämistä. Jos suoritat molemmat menettelyt rinnakkain , teorian täydellisyyden vuoksi yhden niistä pitäisi joskus pysähtyä ja antaa myönteinen vastaus.
Jos teoria on täydellinen jonkin tulkintaluokan suhteen, sitä voidaan käyttää päätöksentekomenettelyn rakentamiseen. Esimerkiksi lauselogiikka on täydellinen totuustaulukoiden tulkinnan suhteen . Siksi totuustaulukon rakentaminen tämän kaavan mukaan on esimerkki propositiologiikan ratkaisualgoritmista.