.. , G valemkuju on samaselt tõene, siis sekvents on tuletatav. Selle teoreemi tõestas austria loogik ja matemaatik Kurt Gödel aastal 1930. Omal ajal oli see matemaatilise loogika üks silmapaistvamaid tulemusi. Meie seda teoreemi käesolvas kursuses ei tõesta. Võrdusega predikaatarvutus. Sümmeetrilisuse ja transitiivsuse tuletamine võrdusega predikaatarvutuses. Korrektsus, mittevasturääkivus, täielikkus (neist viimane tõestuseta). Esimest järku aksiomaatilised teooriad. Teoreemid nende korrektsuse, mittevasturääkivuse ja täielikkuse kohta. Formaalne aritmeetika. Gödeli tulemused (mittetäielikkus, mittevasturääkivuse tõestamatus). Teoreem 8. (korrektsuse teoreem) Kui sekvents 1 , 2 , ... , G on esimest järku teoorias tuletatav, siis ta on tõene teooria omaaksioomide kõikides mudelites. Tõestus lk. 105 Teoreem 9.(mittevasturääkivuse teoreem) Kui esimest järku teooria omaaksioomidel leidub mudel, siis on see teooria mittevasturääkiv.
4. TÕESTUSTAKTIKAD Teoreemi üldkuju: kui on täidetud eeldused E1, ..., Ne, siis kehtib väide V Väide on kujul B&C Eeldus on kujul B&C Väide on kujul BvC Eeldus on kujul BvC Väide on kujul B->C Eeldus on kujul B->C Väide on kujul B Eeldus on kujul B Väide on kujul B<->C Eeldus on kujul B<->C Väide on kujul () Eeldus on kujul () Väide on kujul () Eeldus kujul () 5. AKSIOMAATILISED TEOORIAD Mitteformaalse aksiomaatilise teooria skeem: o Fikseeritakse mingi hulk antud teoorias uuritavaid objekte, nendel defineeritud funktsioone ja seoseid ning sümboolika nende tähistamiseks o Teatud hulk väiteid loetakse tõesteks a priori (ilma tõestuseta). Neid väiteid nimetatakse selle teooria aksioomideks o Teooria arendamine seisneb nn. teoreemide tõestamises.
annaabi.ee 
