6.1 - należy ją jednak uzupełnić obrakujące spójniki i mały kwantyfikator).
Formuły następujących typów będą nazywane aksjomatami czystymi: podstawienia formuł do tautologii rachunku zdań, formuły postaci (gdzie to formuły), formuły postaci o ile jest wolna dla termu w formuły postaci gdzie zmienna nie jest wolna w formule formuły postaci
i
gdzie są (niekoniecznie różnymi) zmiennymi, formuły postaci
gdzie są zmiennymi a jest -arnym symbolem relacyjnym, formuły postaci
gdzie są zmiennymi a jest -arnym symbolem funkcyjnym.
Aksjomaty czyste i formuły postaci gdzie jest aksjomatem czystym, są nazywane aksjomatami logicznymi.
Reguła wnioskowania Jeśli są formułami języka oraz jest postaci to powiemy, że formuła może być wywnioskowana z w oparciu o regułę modus ponens.
Modus ponens to za mało. Brakuje reguły generalizacji:
Dowód Niech będzie jakimś zbiorem formuł języka (możliwie pustym).