існує алгоритм, який для будь-якої формули будує виведення цієї формули

існує алгоритм, який для логічно істинних формул доводить, що вони є теоремами, а для всіх інших – може не давати відповідь

існує процедура, яка може працювати нескінченно та визначає чи є будь-яка формула системи теоремою, чи ні

 існує алгоритм, який для будь-якої формули системи визначає чи є вона теоремою, чи ні