". Gödeli täielikkuse teoreem ja mittetäielikkuse teoreemid. Gödeli teoreem on formaalse aritmeetika mittetäielikkuses. Gödel väitis, et igas formaalses aritmeetikas leidub tõene lause, mis ei ole antud formaalses aritmeetikas tõestatav. Täielikkuse teoreem; http://cs.ttu.ee/kursused/itv0010/various/lrttyld.html : ,,1930. aastal tõestas Gödel, et loogika baaskeel, Fregest lähtuv ja Russelli, Whiteheadi, Hilberti, Tarski, Gentzeni töödes kaasaegse kuju saanud esimest järku predikaatarvutus on täielik: iga tegelikult õige väide, mida saab predikaatarvutuses kirja panna, on predikaatarvutuse formaalsete reeglite abil tõestatav. Siinkohal toetub ``õigsuse'' mõiste Tarski, poolt rajatud teooriale semantikast ja mudelitest." Esmapilgul tundub teoreem täielikkusest olevat vastuolus järgmises lõigus vaadeldava teoreemiga formaalse aritmeetika mittetäielikkusest, kuid see vastuolu
(Def 1. Tuletuseks ehk formaalseks tõestuseks nim valemite jada 1 , 2 , ... , , milles iga valem on kas aksioom või saadud mingi tuletusreegliga mõnedest temale eelnevatest valemitest. Valemist F nim tuletatavaks, kui leidub tuletus, mille viimane liige on valem F) Sekventsiaalne lausearvutus. Tuletamine lausearvutuses. Eesmärk on formuleerida lausearvutuse jaoks aksiomaatika, mis on korrektne ja täielik samaselt tõesuse semantika suhtes. Kasutame Gentzeni-tüüpi süsteemi, mis vastab matemaatiliste väidete tõestamisel esinevatele arutluskäikudele paremini kui ajalooliselt vanemad Hilberti-tüüpi süsteemid. Lugeda lk. 88-96 Lausearvutuse korrektsus, mittevastusrääkivus (tõestustega). Teoreem 1. (korrektsuse teoreem) Kui sekvents 1 , 2 , ... , G on tuletatav, siis tema valemkuju on samaselt tõene. Tõestus lk. 91 Teoreem 2.(mittevasturääkivuse teoreem) Sekventsiaalne lausearvutus on mittevasturääkiv. Tõestus lk. 93
kirjeldada, st nende struktuur võib olla sõna otses mõttes kirjeldamatult keeruline. 2.5.5 Täielikkus, mittetäielikkus ja Kurt Gödel Nagu Albert Einstein füüsikas, nii on Austria-USA loogik Kurt Gödel (1906-1978) üks neid väheseid, keda võib ülepingutamist kartmata geeniuseks nimetada. 1930. aastal tõestas Gödel, et praegusaegse loogika baaskeel, Fregest lähtuv ja Russelli, Whiteheadi, Hilberti, Tarski, Gentzeni töödes kaasaegse kuju saanud esimest järku predikaatarvutus on täielik: iga tegelikult õige väide, mida saab predikaatarvutuses kirja panna, on predikaatarvutuse formaalsete reeglite abil tõestatav. Siinkohal toetub ``õigsuse'' mõiste Tarski poolt rajatud teooriale semantikast ja mudelitest. Esmapilgul tundub teoreem täielikkusest olevat vastuolus järgmises lõigus vaadeldava teoreemiga formaalse aritmeetika
annaabi.ee 
