mingitest ühtedest valemitest on võimalik saada teisi (esimestest tuletatud) valemeid: • Kõigepealt peavad meil olema valemid, mille tähised olgu vastavalt X ning Y • Moodustame valemi XÉY, mis esitab niisugust järeldamist, mille eelduseks on X ning järelduseks on Y. • Kui lähtume nüüd valemitest X ning XÉY, siis on nendest valemitest tuletatud valemiks valem Y. Reegli modus ponens ehk lühemalt MP kohast tuletussammu esitatakse järgmise kirjutisega: X XÉY Y Selgitus: õigest eeldusest ja õigest järeldamisest tuleneb õige järeldus Mõned tuletusreeglid. Modus tollens. Reegel modus tollens paneb paika veel ühe lubatud viisi, kuidas lähtudes mingitest ühtedest valemitest on võimalik saada teisi (esimestest tuletatud) valemeid: • Kõigepealt peavad meil olema valemid, mille tähised olgu vastavalt X
terminid formaalne aksiomaatiline süsteem; arvutus; tõestussüsteem. Tuletus koosneb 2 tuletussammudest. Üks tuletussamm on mingi konkreetse väite tuletamine eelduste või varem saadud vahetulemuste põhjal. Tuletusreeglid näitavad, mida saab mingi kujuga lausena esitatud väitest (oletusest) või väidetest selles tuletussammus järeldada, milline on sammu tulem. Tuletusreegleid ei tohi kasutada asenduste tegemiseks tuletussammu eeldustes või tulemites, selleks saab kasutada teisendusreegleid ehk asendusreegleid. Teisendusreegel lubab mingi sümboli või valemi asendada teise sümboli või valemiga. Asendusi saab teha ka valemi sees. Nt koolialgebra valemites võib valemi (a + a) asendada sümboliga 2a, lausearvutuses võib valemis (¬A ˅ B) & (A → ¬A ˅ B) iga disjunktsiooni kujul ¬A ˅ B asendada implikatsiooniga A → B (vt lausearvutuse teisendusreeglite tabelit). Teisendusreeglit saab
Tuletus koosneb 2 tuletussammudest. Üks tuletussamm on mingi konkreetse väite tuletamine eelduste või varem saadud vahetulemuste põhjal. Tuletusreeglid näitavad, mida saab mingi kujuga lausena esitatud väitest (oletusest) või väidetest selles tuletussammus järeldada, milline on sammu tulem. Tuletusreegleid ei tohi kasutada asenduste tegemiseks tuletussammu eeldustes või tulemites, selleks saab kasutada teisendusreegleid ehk asendusreegleid. Teisendusreegel lubab mingi sümboli või valemi asendada teise sümboli või valemiga. Asendusi saab teha ka valemi sees. Nt koolialgebra valemites võib valemi (a + a) asendada sümboliga 2a, lausearvutuses võib valemis (¬A B) & (A ¬A B) iga disjunktsiooni kujul ¬A B asendada implikatsiooniga A B (vt lausearvutuse teisendusreeglite tabelit). Teisendusreeglit saab
1) A 2) A B 3) B C Esimesest kahest saab järeldusreegli abil formaalselt tuletada väite B, ning B ja väide (3) annavad järeldusreegli abil lõpuks väite C. Viimase tuletussammu formaalseks läbiviimiseks asendasime järeldusreeglis muutujad A ja B muutujatega B ning C. Enamik loogikaharusid kasutab lausearvutuse keele rikastatud variante, mis lubavad kirja panna märksa keerulisemaid väiteid, kui puhas lausearvutus võimaldab. Olulisem neist rikkamatest formaalsetest keeltest on predikaatarvutuse keel, milles saab rääkida objektidest, nende omadustest ja omavahelistest suhetest.