НГУ

Пусть M -- классическая модель упорядоченного поля вещественных чисел с экспонентой. (Имеется в виду модель в традиционном смысле, т.е. в рамках метаматематики.)

Пусть r(x) -- формула сигнатуры {\in}, формализующая (в ZFC) утверждение о том, что x является классическим упорядоченным полем вещественных чисел с экспонентой. (Т.е. r(x) фактически повторяет конструкцию модели M на формальном уровне.) Расширим ZFC константой R, определяемой (по Бету) формулой r(R).

Пусть Ф -- множество всех предложений сигнатуры {+,-,*,0,1,<,exp} (сложение, вычитание, умножение, ноль, единица, порядок, экспонента).

Положим
T(M) = {ф из Ф : M |= ф},
T(R) = {ф из Ф : ZFC |- (R |= ф)}.

Известно, что (в предположении о справедливости гипотезы Шануэля) теория T(M) разрешима. Не следует ли отсюда, что теории T(M) и T(R) совпадают? Или что теория T(R) полна? Или что теория T(R) разрешима?

P.S. Чегой-то заплутал я в этих двух соснах (M и R), а ответ, тем не менее, хочется получить поскорее.

Я не знаю исчерпывающего ответа на этот вопрос (откуда, понятно, никак не следует, что его не существует), но предложу несколько соображений.

1. Ясно, что если ZFC противоречива, то T(R) просто равна Ф, и всё неинтересно. Допустим, что ZFC непротиворечива.

2. Если мы будем рассматривать не вещественные числа, а произвольную модель M, то никакой ясной связи между T(M) и T(R) я не вижу. В качестве аргумента можно заметить, что T(R) - это всегда некоторая вычислимо перечислимая теория, в то время как T(M) может быть сколь угодно сложной.

3. Возвращаясь к нашей ситуации, рискну предположить, что в определении T(R) имело бы смысл заменить ZFC на ZFC + "Гипотеза Шануэля", так как иначе мы про T(M) априори ничего не знаем, и оказываемся в п.2.

4. Даже если мы сделаем эту замену, то мне кажется, что всё равно утверждать что-то определённое про T(R) сложно. Из текста поста мы имеем лишь чистую теорему существования: существует некая вычислимая функция, распознающая принадлежность предложений к T(M).

5. Но если, например, при доказательстве разрешимости T(M) мы построили явный алгоритм, приводящий предложения ф к какому-то хорошему виду, то его можно погрузить в ZFC и получить полноту и разрешимость T(R). То есть надо смотреть доказательство.

Точно, имеет смысл.

Опять-таки, верно подмечено. Мало ли каким манером там доказана разрешимость. Вполне может оказаться, что они умудрились получить ее как-то "неконструктивно".

Понял. Бум посмотреть.

Спасибо!

Мне кажется, можно уточнить эту идею так. Пусть мы в ходе доказательства явным образом построили машину Тьюринга (то есть указали способ выписать её программу), для которой доказано, что она выдаёт 1 на предложении ф тогда и только тогда, когда ф лежит в T(M). Тогда мы можем утверждать, что T(M) = T(R).

В общем случае это равенство неверно. Интересно, что мы можем сказать про включение T(R) в T(M)?

И есть ещё один любопытный вопрос, который меня давно интересует: известно ли что-нибудь про ситуацию, в которой ZFC непротиворечива, но при этом в ней доказуемо, что "ZFC|-"? Он в чём-то близок к предыдущему.

Последний раз близким кругом вопросов я интересовался в 2004 г.
Timothy Y. Chow (Ph.D., в то время сотрудник MIT, а ныне -- член Center for Communications Research, Princeton) любезно сообщил мне буквально следующее:
Никто не ожидает, что теория ZFC + Con(ZFC) противоречива.

Это, собственно, вопрос веры в ZFC. Никто не мешает нам построить теорию ZFC1, добавив к ZFC отрицание Con(ZFC), и эта новая теория тоже будет обладать массой замечательных свойств, в первую очередь тем, что в неё будут погружаться все математические рассуждения. При этом ZFC1 + Con(ZFC1) будет противоречивой.

Единственным её недостатком будет меньшая очевидность аксиом, по сравнению с ZFC. Возможно, что, отрицая понятие "очевидность аксиом" как псевдонаучное, мы на сможем увидеть между ними никакой разницы.