"sekventsiaalne" - 1 õppematerjal

SML kordamisküsimustele vastused.

· korrektseks, kui iga teoorias T tuletatav valem on semantikas S tõene. · täielikuks, kui iga semantikas S tõene valem on teoorias T tuletatav. (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 , ..