SML kordamisküsimustele vastused.
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
Lausearvutuse täielikkuse teoreemi põhilemma ja täilekkuse teoreem
(tõestustega)
Teoreem 4. Kui sekventsi 1 , 2 , ... , G valemkuju on samaselt tõene, siis sekvents on
tuletatav.
Tõestus lk. 96
II. Turingi masinad
Turingi masin. Arvuliste funktsioonide arvutamine Turingi masinal.
annaabi.ee 
