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

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

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

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