Может, разумеется. Но ведь нам предлагают не доказательство, а идею.
Для
множество доказуемых (и соответственно опровержимых) утверждений перечислимо, но не разрешимо. Т.е. алгоритма, который берет утверждение, и говорит, доказуемо ли оно - нет (но есть алгоритм, который берет утверждение, и если оно доказуемо, говорит что оно доказуемо, а если нет - то не отвечает).
Ну, не факт. Если мы берём одно из недоказуемых аксиомой, меняется последовательность — что-то становится доказуемым, что-то вообще опровергаемым.
Ладно, давайте я напишу построже (хотя кажется сказанное ранее формализуется однозначно).
Мы берем и нумеруем все формулы нашей сигнатуры (будем считать ее не более чем счетной):
. Строим последовательность теорий
.
- это наша начальная теория, считаем, что непротиворечивая.
, если в
или
, иначе
. В этом случае
- полная непротиворечивая теория.