О непротиворечивости арифметики, теореме Гёделя, etc.

[Padawan]

kp9r4d в сообщении #1169500 писал(а):

Мне кажется, вы слишком платонист и именно поэтому столь сильно упрощаете ситуацию.

kp9r4d в сообщении #1169599 писал(а):

Удивляет, опять же, потому, что это серьезный контраргумент против различного платонизма и математического реализма и по сути сильно компрометирует (по крайней мере для меня) такие несепарабельные конструкции как "модель", "истинность", "стандартная модель натуральных чисел", ...

kp9r4d в сообщении #1169599 писал(а):

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

Доказательство теоремы Гёделя о неполноте существенным образом использует содержательные свойства натуральных чисел "стандартной модели". Так что пытаться обойти представление о натуральных числах, которое формируются с детских лет и далее развивается постепенно до аксиом Пеано (с аксиомой индукции в логике второго порядка), просто невозможно. Говорить о теореме Гёделя и отрицать "платоническую реальность" натуральных чисел бессмысленно. Если у кого-то нет представления о "стандартной модели" натуральных чисел, то он просто не поймет доказательство теоремы Гёделя (а может и её формулировку!). Множество натуральных чисел существует (и единственно с точностью до изоморфизма). Это неформальная аксиома (и теорема). Теорема Гёделя - неформальное метаматематическое утверждение, и её доказательство - такое же. Её можно формализовать в рамках какой-либо формальной теории, но это ничего не добавит к её убедительности. Потому что возникнут вопрос, а какое отношение эта формализация имеет к тому, чт мы подразумеваем под теоремой Гёделя. Итог: все нельзя формализовать в математике, всегда будет оставаться содержательный неформализованный метауровень!

Кстати, в который раз вспоминаю Кронекера, который сказал: "Бог создал целые числа, всё остальное - творение человека".

[Padawan]

Возник такой вопрос, в продолжение моего поста http://dxdy.ru/post1198430.html#p1198430. Часто при формулировке теоремы Гёделя делается оговорка, мол, если арифметика Пеано не противоречива. Но как она может быть противоречива, если она имеет модель в виде обычных натуральных чисел? Оговорка получается лишней. А если кто-то сомневается в существовании системы натуральных чисел, то ему и теорема Гёделя вовсе не теорема. Ибо в ней эти числа существенно используются при доказательстве. В общем, не пойму я смысла этой оговорки. Может я чего-то не понимаю?

Вот оговорка про непротиворечивость теории множеств мне понятна. Кто их знает, эти множества, тем более прецеденты были. Если противоречивость вскроется, нужно будет подправить аксиомы.

[warlock66613]

Padawan в сообщении #1200954 писал(а):

Но как она может быть противоречива, если она имеет модель в виде обычных натуральных чисел?

А нам точно известно, что это именно модель, а не просто интерпретация?

-- 16.03.2017, 19:48 --

Padawan в сообщении #1200954 писал(а):

Ибо в ней эти числа существенно используются при доказательстве.

Существенно, но всё-таки ограниченно, так что доказательство можно аксиоматизировать (в другой аксиоматике, не Пеано).

[Padawan]

В чем разница между моделью и интерпретацией? В моем понимании модель для арифметики Пеано - это множество, на котором заданы операции $0,s,+,\cdot$, удовлеторяющие тем соотношениям, которые приняты в АП за аксиомы.

[arseniiv]

Ну да, модель теории — это интерпретация, в которой все теоремы теории истинны, и если теория аксиоматизирована каким-то множеством аксиом, достаточно, чтобы в этой интерпретации все они были истинны, как вы написали.

[warlock66613]

Вот и возникает вопрос ­— как проверить, что аксиомы в стандартной интерпретации истинны? Аксиом много, натуральных чисел тем более...

[Padawan]

warlock66613
Аксиомы Пеано. См., например Ландау Основы анализа. Там из них выводятся все свойства натуральных чисел. Какая именно из аксиом у Вас вызывает сомнение? Аксиома индукции? Да даже не в этом дело. Натуральные числа определяется как множество, с выделенным элементом и операцией следования, удовлетворяющих аксиомам Пеано. Существование натуральных чисел постулируется. На них основана вся математика, а не только теорема Геделя. Без натуральных чисел Вы даже не сможете определить что такое формула в каком либо формальном исчислении. В той же АП. Да даже что такое конечный набор символов алфавита.

[warlock66613]

Padawan в сообщении #1201077 писал(а):

Без натуральных чисел Вы даже не сможете определить что такое формула в каком либо формальном исчислении. В той же АП. Да даже что такое конечный набор символов алфавита.

Смогу. "Настоящие" натуральные числа можно заменить объектами из всё той же арифметики Пеано или любой другой аксиоматизации.

[arseniiv]

Ну, тут не так всё просто, т. к. у арифметики Пеано есть нестандартные модели с «числами», идущими после всех стандартных, и мы, разумеется, никак не можем отделить их средствами языка арифметики от стандартных, и если начнём определять вывод, у нас возникнут в такой модели выводы со счётным (и более, если мощность модели больше) числом шагов. И формулы с термами тоже.

[Toucan]

Выделено из темы «Опять о теореме Геделя»

[warlock66613]

Ну не знаю тогда. Есть интуитивное чувство, что ответ на загаданную Padawan загадку лежит за пределами теорий первого порядка.

[mihaild]

Может быть, проблема в том, что теоремой Гёделя можно называть как "настоящую" теорему арифметики $\exists \varphi: \varphi \leftrightarrow \neg \Box_{PA} \varphi$ (а 2й $Cons_{PA} \rightarrow \neg \Box_{PA} \ulcorner Cons_{PA}\urcorner$), так и неформальную "если арифметика непротиворечива, то она неполна"?

Формально у нас есть три варианта:
1) $PA$ непротиворечива, и у нее есть модель, соответствующая нашей "интуиции" про стандартную модель: оговорка не нужна
2) $PA$ противоречива: оговорка нужна
3) $PA$ непротиворечива, но у нее есть только "нестандартные" модели: всё очень плохо (непонятно, что вообще "значат" все наши формальные результаты про выводимость)

Тот, кто говорит "арифметика неполна" "прав" (на неформальном уровне) в 1м случае, тот, кто говорит "если непротиворечива, то неполна" - в 1 и 2.

Интересный вопрос, что мы будем делать, если окажется, что $PA \vdash \neg Cons_{PA}$...

[Padawan]

Думаю, что третий вариант невозможен. Т.к. если есть хотя бы одна модель, то в ней найдется подмножество, являющееся стандартной моделью. А именно, множество $0,0',0'',0''',...$, которое можно формально определить как наименьшее по включению множество, содержащее нуль и замкнутое относительно операции следования (правда на языке логике второго порядка). Но я еще раз говорю, если запрещено использовать натуральные числа, то что вообще разрешено?

[mihaild]

Padawan в сообщении #1201408 писал(а):

А именно, множество $0,0',0'',0''',...$, которое можно формально определить как наименьшее по включению множество, содержащее нуль и замкнутое относительно операции следования (правда на языке логике второго порядка).

Мало что знаю о логике второго порядка. Там будут какие-то принципиальные отличия от аналогичного определения в $ZF$ ($\mathbb{N}$ - наименьшее индуктивное множество)?
Если мы вводим какую-то метатеорию, в которой будем отличать стандартные модели от нестандартных, то что нас спасет от "нестандартных" моделей этой метатеории?

В конечном итоге, видимо, разрешено использовать "интуицию" про операции со строчками.

Что значит "запрещено использовать натуральные числа"? Формализация неформальных утверждений - операция неформальная:-) И она опирается на неформальную интуицию "стандартной модели". А получившуюся штуку уже можно доказывать формально.

[george66]

Непротиворечивость арифметики простым глазом не видна. Никакой физический опыт нас не убеждает в существовании числа $10^{10^{100}}$. По поводу единственности: в настоящее время придуманы содержательные комбинаторные утверждения о натуральных числах, не доказуемые и не опровержимые в ZF (содержательные в отличии от малонаглядных неразрешимых формул Гёделя), их в огромном количестве производит Харви Фридман и выкладывает на FOM
http://www.cs.nyu.edu/pipermail/fom/
вот его свежая похвальба
http://www.cs.nyu.edu/pipermail/fom/201 ... 20392.html
Таким образом, никакой единственности натурального ряда больше нет - есть разные натуральные ряды, в которых выполнены разные комбинаторные утверждения, как есть разные геометрии. Как вообще устроен "реальный" натуральный ряд (ряд километров, уходящий в космос), мы мало знаем.