**GEB, стр. 72–73**
Следствие: существуют формальные системы без алгоритма разрешения.
Алгоритм разрешения отличает теоремы от не-теорем.
Если бы он был — можно было бы выводить не-теоремы.
Но для некоторых систем это невозможно.
🌀 Простые числа — можно вывести позитивно (через неделимость).
Но не всё так удачно.