Re: Раз уж зашёл, обозначу присутствие
А я вот не вполне понимаю, почему в случае действительного существования списка натуральных чисел в Haskell проблема нечётных совершенных чисел до сих пор числится открытой. Список-то допускает полный перебор!

Список бесконечный - и перебор соотвественно получится бесконечный. Что тут удивительного - даже многие конечные алгоритмы "всегда завершаются" сугубо теоретически - например я Вам на два счета заставлю любой из известных мне компиляторов java транслировать коротенькую программку до второго пришествия. Хотя там все разрешимо в теории.

А [0..] - это просто сокращение для кода вроде:
let nat n = n:nat (n+1) in nat 1
a:b - это список с головой a и хвостом b

По машинному представлению ничем не отличается от прочих списков.

Честно говоря, не очень понятно, как её "кодировать в машине". Было бы очень неплохо это уточнить

Ну там содержательный смысл ее в том, что объектами модели являются формулы теории вида "существует и единственное X, такое что ...". Точнее - классы эквивалентностей этих формул. А у Барвайса - обобщенная теорема, на случай теорий не со счетным, как у ZF множеством аксиом, а произвольным.

А вот это правильно! Теория о сношениях человека с дьяволом имела практические применения в избытке: ведьм реально жгли по всей Европе. Следовательно, каждое слово в «Malleus maleficarum» истинно.

Я хоть слово говорил об истинности?