AGu писал(а):
хотелось бы понять, чем плох "тюремный" подход. Не откажетесь покритиковать?
Pavel E. Alaev писал(а):
Ну, собственно, мы его в некотором смысле используем - когда мы говорим, что формула
nat(x) <=> U_{n} En(x)
считается верной, мы тем самым ограничиваем класс моделей ZFC, которые хотим рассматривать.
Да, какая-то аналогия тут есть. Впрочем, в тюремном подходе класс моделей ZFC никак не ограничивается: класс ZFC-узников в определенном смысле совпадает с классом всех моделей ZFC, поскольку любая модель ZFC единственным образом обогащается до ZFC-узника и, наоборот, обеднение любого ZFC-узника является моделью ZFC. В этом смысле тюремная теория не дает ничего нового для ZFC, ибо она консервативно расширяет ZFC, добавляя к ее теоремам новые предложения (тюремы), содержащие новый предикат fin.
Если же ввести то ограничение (которое в тюремных терминах означает совпадение натуральных и внатуральных чисел), то в результате получится теория, состоящая из всех предложений, истинных в моделях ZFC c "истинными" натуральными числами.
Цитата:
тюремный подход слишком сильный - условие ограниченности класса моделей надо как-то "спускать на землю", превращая его в конкретные методы доказательства
Согласен. Хочется как-то регламентировать класс "законных" рассуждений на синтаксическом уровне. В случае успеха тут неизбежно возникнет какое-то необычное понятие доказательства, так как в классическом смысле ни тюремная теория, ни теория моделей с "истинными" натуральными числами не аксиоматизируемы.
Цитата:
С другой стороны, он слишком слаб. Когда мы говорим об аксиомах для какой-то области математики, мы всегда должны стремиться к максимальной полноте - чтобы всё, что нас интересует, либо выводилось из наших аксиом, либо опровергалось ими.
Опять согласен. По сравнению с ZFC тюремная теория "еще более неполная": имеется еще больше таких формул \phi, что ни \phi, ни ~\phi не являются тюремами.
Цитата:
аксиома о существовании множества натуральных чисел, о которой Вы говорили,
\exists X \forall x [x \in X <=> P(x)],
конечно же должна у нас быть.
Т.е. речь идет все же о теории, состоящей из предложений, истинных в моделях с "истинными" натуральными числами?
Верно ли, что в качестве основной задачи выдвигается разработка синтаксического аппарата для этой (или какой-то аналогичной) теории? Если так, то в данный момент я тут вижу такой густой туман, что он мне представляется глухой стеной.