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 =); ¬ – eitus; & – konjunktsioon; ∨ – disjunktsioon; → – implikatsioon; ↔ – ekvivalents; ∀ – üldisuskvantor; ∃ – olemasolukvantor; ∴ – järelikult (postuleeritav lõppjäreldus); ∈ – kuuluvusseos; (), [], – kirjavahemärgid. Tuletus koosneb tuletussammudest. Üks tuletussamm on mingi konkreetse väite tuletamine eelduste või varem saadud vahetulemuste põhjal. Tuletussamm viiakse läbi tuletusreeglit kasutades. Esitatav tuletussüsteem põhineb lauseloogikal, milles sõnu ,,lause”, ,,väide” ja ,,propositsioon” kasutatakse sünonüümidena, kuigi silmas peetakse alati objekti, mis on tõene või väär, st propositsiooni
.., 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 =); ¬ eitus; & konjunktsioon; disjunktsioon; implikatsioon; ekvivalents; üldisuskvantor; olemasolukvantor; järelikult (postuleeritav lõppjäreldus); kuuluvusseos; (), [], kirjavahemärgid. Tuletus koosneb tuletussammudest. Üks tuletussamm on mingi konkreetse väite tuletamine eelduste või varem saadud vahetulemuste põhjal. Tuletussamm viiakse läbi tuletusreeglit kasutades. Esitatav tuletussüsteem põhineb lauseloogikal, milles sõnu ,,lause", ,,väide" ja ,,propositsioon" kasutatakse sünonüümidena, kuigi silmas peetakse alati objekti, mis on tõene või väär, st propositsiooni
annaabi.ee 
