Coheni õpikus (2009) esitatud loomulik tuletussüsteem (system of natural deduction). Esitatav süsteem on lauseloogika seisukohalt täielik, selle abil saab tuletada kõik lauseloogika kehtivad samasused. Loomuliku tuletuse süntaks on lausearvutuse süntaks, selle järgi formuleeritakse ka tuletusreeglid. Süllogistiliste arutluste kehtivuse tõestamiseks läheb tarvis ka predikaatloogika tuletussüsteemist pärinevaid, üldisuskvantoriga ja olemasolukvantoriga seotud reegleid, kuid selline süsteem ei ole predikaatloogika seisukohalt täielik. 9.1. LOOMULIK TULETUSSÜSTEEM Sümboleid: G – eelduste komplekt ehk väidete hulk või väidetesüsteem {p1, p2, p3, …, pn}; G ⊢ p – eeldustest G saab tuletada p;⊢⊬ ⊨⊭ G ⊬ p – eldustest G ei saa tuletada p; G ⇒Q (G ⊨ Q) – eeldustest G järeldub Q, st väide või väidetesüsteem {q1, q2, …, qn};1 G ⊭ Q – eeldustest G ei järeldu Q, ⇔ – vastastikune järeldumine;
Coheni õpikus (2009) esitatud loomulik tuletussüsteem (system of natural deduction). Esitatav süsteem on lauseloogika seisukohalt täielik, selle abil saab tuletada kõik lauseloogika kehtivad samasused. Loomuliku tuletuse süntaks on lausearvutuse süntaks, selle järgi formuleeritakse ka tuletusreeglid. Süllogistiliste arutluste kehtivuse tõestamiseks läheb tarvis ka predikaatloogika tuletussüsteemist pärinevaid, üldisuskvantoriga ja olemasolukvantoriga seotud reegleid, kuid selline süsteem ei ole predikaatloogika seisukohalt täielik. 9.1. LOOMULIK TULETUSSÜSTEEM Sümboleid: G eelduste komplekt ehk väidete hulk või väidetesüsteem {p1, p2, p3, ..., pn}; G p eeldustest G saab tuletada p; G p eldustest G ei saa tuletada p; G Q (G Q) eeldustest G järeldub Q, st väide või väidetesüsteem {q1, q2, ..., qn};1 G Q eeldustest G ei järeldu Q, vastastikune järeldumine; samasus (loogiline samaväärsus, ka =);