Loogika aine ja ajalugu
lahendust omavate probleemide jaoks eksisteerib lahendamise algoritm. Selleks piisas Turingi veendumust mööda
Turingi masina kui universaalse masina teoreetiliste võimaluste uurimisest. Turing tõestas, et tema masina abil ei ole
võimalik alati otsustada, kas suvaline predikaatarvutuse keeles kirjutatud väide on õige ja seega predikaatarvutuse
reeglitest mehaaniliselt tuletatav või ei. Predikaatarvutus ei ole lahenduv. Mittelahenduvus laieneb predikaatarvutuselt
muidugi kõigile süsteemidele, mille kaudu predikaatarvutust esitada saab. Predikaatarvutusest oluliselt lihtsamad
loogikasüsteemid on sageli lahenduvad. Juba enne Turingit oli teada, et näiteks klassikaline lausearvutus on lahenduv.
On olemas algoritmid, mis suudavad (kui neile piisavalt aega anda) iga lausearvutuse keeles kirjutatud väite kohta
öelda, kas see väide on õige ja tuletatav, või vale ja ei ole tuletatav.
annaabi.ee 
