Теорема Лёба

[Someone]

epros писал(а):

Но просто сравните этот подход с тем, как понятие об арифметике вводится критикуемыми Вами конструктивистами:
1. Натуральное число - это строка из вертикальных чёрточек.
2. Операция инкремента - это добавление к строке одной чёрточки.

Не вижу здесь никакого введения понятия об арифметике. Вам ещё много чего придётся к этому добавить, прежде чем можно будет говорить об арифметике.

epros писал(а):

Скажите теперь, кто ближе к "прикладным вопросам"?

От прикладных вопросов сформулированное Вами бесконечно далеко. Если, конечно, не понимать под прикладными вопросами рисование палочек.

epros писал(а):

Вспомним то самое пресловутое Гёделевское высказывание $G$, которое, будучи по своему синтаксису арифметическим выражением, эквивалентно собственной недоказуемости в арифметике. Как известно, Гёдель с помощью мета-теоретического рассуждения доказал его истинность. Т.е. мы имеем две теоремы метатеории:
1. $G$
2. $\neg (A \vdash G)$

Я давал ссылку на Клини. И формулировки теорем приводил. Специально для Вас. Из текста Клини чётко видно, что ничего подобного Гёдель не делал.

[epros]

nikov писал(а):

epros писал(а):

Как известно, Гёдель с помощью мета-теоретического рассуждения доказал его истинность.

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

http://en.wikipedia.org/wiki/G%C3%B6del ... s_theorems

"Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory."

Обратите внимание на слова "that is true, but not provable in the theory".

маткиб писал(а):

В принципе, исключить этого нельзя, но разумно предположить, что в данном случае этого не произойдёт. На каком-то уровне всё равно придётся пользоваться подобными предположениями об одинаковости понимания (например, что такое строка из вертикальных чёрточек).
...
Ну тут можно сколько угодно перегибать палку. Что значит "сказанное можно формализовать"? Что такое формализация? Где гарантия, что формализацию все поймут одинаково? Формализация здесь нужна только для того, чтобы свести "плохие" понятия (с большой опасностью неоднозначного понимания) к "хорошим" (которые опытные образованные люди, как правило, понимают одинаково).

То, что Вы говорите, в принципе правильно, но недостаточно конкретно. Вот Вы говорите: "На каком-то уровне придётся пользоваться ...", не уточняя что за "уровень". А в итоге - у каждого своё понимание этого уровня и не факт, что одинаковое. А значит неизбежны ситуации, когда мы с Вами неверно оценим уровни формализации, подразумеваемые друг другом.

Я же имею в виду вполне конкретный уровень формализации, дальше которого можно было бы опуститься, но "не нужно". Речь идёт об уровне, на котором каждое математическое понятие сводится к строке символов. Т.е. глубже базовых понятий о символах, алфавите, составлении строк из символов и базовых операций со строками мы не опускаемся. Но до этого уровня мы формализацию довести должны.

маткиб писал(а):

epros писал(а):

Вы слишком плохо думаете о конструктивистах.

Я вообще плохо думаю о людях, которые прикидываются дураками, хотя на самом деле таковыми не являются.

Раз Вы всерьёз думаете, что они "прикидываются дураками", то Вы действительно плохо о них думаете. Ваша позиция сейчас похожа на позицию школьника, который считает, что математики "прикидываются дураками", когда всерьёз доказывают какие-то теоремы из геометрии, когда всё это можно было бы наглядно продемонстрировать с помощью ножниц и бумаги. Речь идёт о серьёзных вещах - о математической строгости, которая, конечно, в 99% случаев может быть и не нужна, но именно в оставшемся 1% может обнаружится, что всё наше коллективное знание построено на фундаменте непонимания друг друга и, начиная с некоторого уровня технологий, просто перестанет работать (хотя до сих пор, казалось бы, прекрасно работало).

маткиб писал(а):

Ни в коем случае она не понятна абсолютно всем. Чтобы её понимать, нужно иметь опыт. А чтобы поиметь опыт, нужно и в младшей школе порешать задачи про сложение и вычитание кучек с яблоками, и с логикой ознакомиться немного, и потратить время на осмысление всего этого. И никакой гарантии нет, что это даст правильное понимание. Но нормального соображающего человека вполне возможно научить такому пониманию.

Да, да. С яблоками, счётными палочками или со строками вертикальных чёрточек.

маткиб писал(а):

epros писал(а):

Но просто сравните этот подход с тем, как понятие об арифметике вводится критикуемыми Вами конструктивистами:
1. Натуральное число - это строка из вертикальных чёрточек.
2. Операция инкремента - это добавление к строке одной чёрточки.

1. Это не является определением натурального числа.
2. При наличии опыта этого "определения" вполне достаточно для понимания, что такое натуральное число.
3. К конструктивистам это не имеет никакого отношения (это появилось за не одну тысячу лет до конструктивистов).

1. Вы просто не заметили, что сюда уже заложены все аксиомы Пеано.
2. Вполне согласен и добавлю: а больше ничего и не нужно.
3. Я не утверждаю, что конструктивисты это первыми придумали, но они следуют именно такому определению. По-моему, полезно напомнить математикам, с чего начиналось понятие о натуральном числе. Погрязнув в абстрактных рассуждениях, многие из них, похоже, просто забыли, что операция счёта заключается в добавлении палочек к строке, а аксиомы Пеано возникли не из воздуха.

маткиб писал(а):

Тогда уж буду придираться (хотя сам не люблю, когда этим занимаются): не определено понятие алфавита, грамматики, что значит определять одни понятия на основе других. Да и вообще в таком определении неявно присутствует представление о рекурсии (или индукции), которое предполагает некоторое представление о натуральных числах.

Здесь, конечно, нет полного определения, но кое-что есть:
Алфавит: должен содержать символ "|" (остальное можно добавить по вкусу).
Грамматика: строка из символов "|" является допустимым словом языка и должна интерпретироваться как "натуральное число" (остальные правила можно добавить по вкусу).
И т.д.
Естественно понятия "алфавит", "символ", "строка" и т.п. мы не определяем, считая их базовыми.

Касательно "неявного представления о рекурсии или индукции" не стану с Вами спорить, ибо оно, возможно, и присутствует ровно настолько, насколько оно присутствует в базовом понятии о "строке символов". Но, как я уже отметил выше, это относится к тому уровню формализации, ниже которого мы не опускаемся (ибо нужды в этом нет: все достаточно чётко представляют, что такое "строки символов" и умеют их различать, уж в этом-то мы можем быть в достаточной мере уверены).

маткиб писал(а):

epros писал(а):

Вероятно я не "здравомыслящий", поскольку мне непонятно. Нет, я понимаю, что утверждение оказалось бы "ложным", найди мы опровергающий пример. И я даже с некоторым усилием верю в то, что кем-то это утверждение как-то доказано (хотя и не представляю как именно), а стало быть его следует, наверное, считать "истинным". Но я совершенно не представляю, что мы должны были думать о его "истинности" или "ложности" до тех пор, пока у нас не было ни того, ни другого.

Сложно судить об этом Вашем высказывании. Возможно, Вы действительно не понимаете, а, возможно, подобно конструктивистам прикидываетесь дурачком.

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

маткиб писал(а):

Чтобы доказать $G$, Гёдель использовал дополнительно аксиому о корректности арифметики Пеано (если быть точным, в языке арифметики это будет схема аксиом), которая выглядит как $\mathrm{Prf}_{\mathrm{PA}}(\Phi)\rightarrow\Phi$.

Конечно же, в самой теории не может быть такой схемы аксиом. Но, принимая теорию, мы автоматически принимаем и это. Теории существуют для того, чтобы судить об истинности. А делать это они могут только если мы признаем, что доказательство является способом определения истинности. Так что ничего существенного эта схема аксиом с моей точки зрения не добавляет. С моей точки зрения существенным скорее является способность метатеории судить о высказываниях теории (чего сама теория не может). Это способность не может быть приобретена без, как минимум, расширения алфавита теории.

Someone писал(а):

Не вижу здесь никакого введения понятия об арифметике. Вам ещё много чего придётся к этому добавить, прежде чем можно будет говорить об арифметике.

Что именно добавить? Аксиомы Пеано отсюда выводимы, а это разве уже не "арифметика"?

Someone писал(а):

От прикладных вопросов сформулированное Вами бесконечно далеко. Если, конечно, не понимать под прикладными вопросами рисование палочек.

Рисование палочек в том числе. А также загибание пальцев, рисование строк из десятичных цифр на бумаге или запись строк из двоичных цифр в памяти компьютера - всё это "прикладные вопросы", которые отсюда прекрасно выводятся.

Someone писал(а):

epros писал(а):

Вспомним то самое пресловутое Гёделевское высказывание $G$, которое, будучи по своему синтаксису арифметическим выражением, эквивалентно собственной недоказуемости в арифметике. Как известно, Гёдель с помощью мета-теоретического рассуждения доказал его истинность. Т.е. мы имеем две теоремы метатеории:
1. $G$
2. $\neg (A \vdash G)$

Я давал ссылку на Клини. И формулировки теорем приводил. Специально для Вас. Из текста Клини чётко видно, что ничего подобного Гёдель не делал.

За ссылку Вам большое спасибо. Я убедился, что существование неразрешимого в любом расширении арифметики высказывания доказано. Однако повторюсь, что это не та же самая первая теорема о неполноте, которую первоначально доказал Гёдель. Существование неразрешимого высказывания само по себе конечно интересно, но не настолько. Более интересен как раз вывод Гёделя о том, что это высказывание не только неразрешимо, но и "истинно". Иногда об этом говорят: "содержательно истинно".

[AGu]

epros писал(а):

Существование неразрешимого высказывания само по себе конечно интересно, но не настолько. Более интересен как раз вывод Гёделя о том, что это высказывание не только неразрешимо, но и "истинно". Иногда об этом говорят: "содержательно истинно".

Я не слежу за дискуссией (просто времени нет, хотя было бы интересно), но... От первого до второго -- вроде бы, крохотный шажок?
Для любого предложения $\varphi$ мы имеем $\mathbb N\vDash\varphi$ или $\mathbb N\vDash\neg\varphi$. Стало быть, если $\varphi$ неразрешимо, то либо $\varphi$, либо $\neg\varphi$ -- искомое предложение (т.е. неразрешимое и истинное).

P.S. Если в пропущенной мной дискуссии "истинность" стала пониматься уже в каком-то ином смысле, то прошу прощения.

[epros]

AGu писал(а):

От первого до второго -- вроде бы, крохотный шажок?
Для любого предложения $\varphi$ мы имеем $\mathbb N\vDash\varphi$ или $\mathbb N\vDash\neg\varphi$. Стало быть, если $\varphi$ неразрешимо, то либо $\varphi$, либо $\neg\varphi$ -- искомое предложение (т.е. неразрешимое и истинное).

Во-первых, такой "маленький шажок" меня не вполне устраивает, поскольку в моей аксиоматике нет закона исключённого третьего.

А во-вторых, насколько я понимаю, если рассматриваемая теория неконструктивна (т.е. использует закон исключённого третьего), то как раз $\varphi \vee \neg \varphi$ не будет в ней неразрешимым, несмотря на неразрешимость $\varphi$. Оно будет доказуемым (с использованием закона исключённого третьего).

AGu писал(а):

P.S. Если в пропущенной мной дискуссии "истинность" стала пониматься уже в каком-то ином смысле, то прошу прощения.

А как Вы понимаете "истинность"? Например, что Вы можете сказать об истинности этого самого неразрешимого $\varphi$? (Только не говорите, что оно "либо истинно, либо ложно", я хотел бы услышать конкретный ответ).

[Someone]

epros в сообщении #170223 писал(а):

Однако повторюсь, что это не та же самая первая теорема о неполноте, которую первоначально доказал Гёдель.

Someone писал(а):

Цитата:

Теорема 28. Если арифметическая формальная система гл. IV (просто) непротиворечива, то не $\vdash A_p(p)$; если эта система $\omega$-непротиворечива, то не $\vdash\neg A_p(p)$. Таким образом, если эта система $\omega$-непротиворечива, то она (просто) неполна, и $A_p(p)$ служит примером неразрешимой формулы. (Теорема Гёделя в первоначальной форме.)

epros в сообщении #170223 писал(а):

1. Вы просто не заметили, что сюда уже заложены все аксиомы Пеано.

epros в сообщении #170223 писал(а):

Что именно добавить? Аксиомы Пеано отсюда выводимы, а это разве уже не "арифметика"?

Да? Покажите.

epros в сообщении #170223 писал(а):

Рисование палочек в том числе. А также загибание пальцев, рисование строк из десятичных цифр на бумаге или запись строк из двоичных цифр в памяти компьютера - всё это "прикладные вопросы", которые отсюда прекрасно выводятся.

Это всё то же рисование палочек, и не более того. Мы интересуемся, главным образом, не рисованием палочек.

[AGu]

epros писал(а):

AGu писал(а):

От первого до второго -- вроде бы, крохотный шажок?
Для любого предложения $\varphi$ мы имеем $\mathbb N\vDash\varphi$ или $\mathbb N\vDash\neg\varphi$. Стало быть, если $\varphi$ неразрешимо, то либо $\varphi$, либо $\neg\varphi$ -- искомое предложение (т.е. неразрешимое и истинное).

Во-первых, такой "маленький шажок" меня не вполне устраивает, поскольку в моей аксиоматике нет закона исключённого третьего.

Виноват, не знал.

epros писал(а):

А во-вторых, насколько я понимаю, если рассматриваемая теория неконструктивна (т.е. использует закон исключённого третьего), то как раз $\varphi \vee \neg \varphi$ не будет в ней неразрешимым, несмотря на неразрешимость $\varphi$. Оно будет доказуемым (с использованием закона исключённого третьего).

Я имел в виду, что либо $\varphi$ является искомым, либо $\neg\varphi$ является искомым.
Впрочем, если в Вашей метааксиоматике нет закона исключенного третьего, то и это метаутверждение Вас вряд ли устроит.

epros писал(а):

А как Вы понимаете "истинность"?

Под $\mathbb N\vDash\varphi$ я понимаю метаутверждение об истинности $\varphi$ в классической модели арифметики $\mathbb N$, определяемое рекурсивно по сложности формулы $\varphi$.

epros писал(а):

Например, что Вы можете сказать об истинности этого самого неразрешимого $\varphi$? (Только не говорите, что оно "либо истинно, либо ложно", я хотел бы услышать конкретный ответ).

Именно это я и хотел было сказать, но теперь лишь скажу, что неверно, что неверно, что $\varphi$ истинно или $\varphi$ не истинно.
Ну а если $\varphi$ -- чиста конкретное предложение, то в одних случаях можно чиста конкретно метадоказать, что $\varphi$ истинно, а в других -- нельзя.

А об чем спор, собсно? О том, опирался ли Гёдель на закон исключенного третьего? (Я всегда думал, что опирался.)

[nikov]

epros писал(а):

nikov писал(а):

epros писал(а):

Как известно, Гёдель с помощью мета-теоретического рассуждения доказал его истинность.

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

http://en.wikipedia.org/wiki/G%C3%B6del ... s_theorems

"Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory."

Обратите внимание на слова "that is true, but not provable in the theory".

К сожалению, это одно из немногих мест, где википедия ошибается (там, правда, в сноске написано оправдание, что речь идет не об обычной истинности, а о дисквотационной истинности). Никак не дойдут руки исправить это. Вот на этом сайте есть хорошее разъяснение: http://www.sm.luth.se/~torkel/eget/godel/system.html
Можно еще здесь взглянуть (Five Great Blunders About Mathematics): http://www.ltn.lv/~podnieks/gt.html

[epros]

Someone писал(а):

epros в сообщении #170223 писал(а):

Однако повторюсь, что это не та же самая первая теорема о неполноте, которую первоначально доказал Гёдель.

Someone писал(а):

Цитата:

Теорема 28. Если арифметическая формальная система гл. IV (просто) непротиворечива, то не $\vdash A_p(p)$; если эта система $\omega$-непротиворечива, то не $\vdash\neg A_p(p)$. Таким образом, если эта система $\omega$-непротиворечива, то она (просто) неполна, и $A_p(p)$ служит примером неразрешимой формулы. (Теорема Гёделя в первоначальной форме.)

Я вижу, что здесь заявлено, что это "теорема Гёделя в первоначальной форме", однако, как я понимаю, автор этого заявления Клини, а не Гёдель, так что это всего лишь его интерпретация. А я встречал и другие интерпретации.

Someone писал(а):

epros в сообщении #170223 писал(а):

1. Вы просто не заметили, что сюда уже заложены все аксиомы Пеано.

epros в сообщении #170223 писал(а):

Что именно добавить? Аксиомы Пеано отсюда выводимы, а это разве уже не "арифметика"?

Да? Покажите.

Разве предвидятся какие-либо трудности?

1. 1 является натуральным числом: "|" = 1 (это просто определение единицы)
2. Число, следующее за натуральным, также является натуральным: Добавление вертикальной чёрточки к строке вертикальных чёрточек даёт строку вертикальных чёрточек.
3. 1 не следует ни за каким натуральным числом: Добавлением вертикальной чёрточки к произвольной непустой строке нельзя получить "|".
4. Если натуральное число a непосредственно следует как за числом b, так и за числом c, то b и c тождественны: Равенство строк b+"|" и c+"|" означает равенство любых соответствующих подстрок, в том числе b и c.
5. Схема индукции - единственная здесь нетривиальная вещь. Но она скорее относится к логике, чем собственно к арифметике. Отказ от неё, насколько я понимаю, просто позволяет расширениям арифметики быть омега-противоречивыми (но не буквально противоречивыми).

Someone писал(а):

Это всё то же рисование палочек, и не более того. Мы интересуемся, главным образом, не рисованием палочек.

А чем Вы интересуетесь?

AGu писал(а):

Я имел в виду, что либо $\varphi$ является искомым, либо $\neg\varphi$ является искомым.
Впрочем, если в Вашей метааксиоматике нет закона исключенного третьего, то и это метаутверждение Вас вряд ли устроит.

Метаутверждение меня бы в любом случае не устроило, даже если бы я принял закон исключённого третьего. Мы ведь искали конкретное высказывание теории, истинное и неразрешимое в ней, а не формулу, утверждающую что это либо такое высказывание, либо такое.

AGu писал(а):

epros писал(а):

А как Вы понимаете "истинность"?

Под $\mathbb N\vDash\varphi$ я понимаю метаутверждение об истинности $\varphi$ в классической модели арифметики $\mathbb N$, определяемое рекурсивно по сложности формулы $\varphi$.

"Метаутверждение об истинности" - это я понимаю, но что значит "определяемое рекурсивно по сложности формулы" и насколько это нас приблизит к получению оного метаутверждения, ежели его взять неоткуда - этого я не понимаю.

AGu писал(а):

Именно это я и хотел было сказать, но теперь лишь скажу, что неверно, что неверно, что $\varphi$ истинно или $\varphi$ не истинно.

Одно другого стОит.
Как я понимаю, это тоже ни на шаг нас не приближает к конкретному значению истинности конкретного высказывания.

AGu писал(а):

Ну а если $\varphi$ -- чиста конкретное предложение, то в одних случаях можно чиста конкретно метадоказать, что $\varphi$ истинно, а в других -- нельзя.

Угу. А ещё в некоторых случаях нельзя мета-мета-доказать, что этого нельзя мета-доказать.

AGu писал(а):

А об чем спор, собсно? О том, опирался ли Гёдель на закон исключенного третьего? (Я всегда думал, что опирался.)

Я тоже раньше думал, но потом понял, что практически всё сказанное (включая утверждение об истинности пресловутого $G$) можно доказать конструктивно (при соответствующих предположениях, естественно). Но спор, в общем, не об этом. Да и спор ли это?

nikov писал(а):

К сожалению, это одно из немногих мест, где википедия ошибается (там, правда, в сноске написано оправдание, что речь идет не об обычной истинности, а о дисквотационной истинности). Никак не дойдут руки исправить это. Вот на этом сайте есть хорошее разъяснение: http://www.sm.luth.se/~torkel/eget/godel/system.html
Можно еще здесь взглянуть (Five Great Blunders About Mathematics): http://www.ltn.lv/~podnieks/gt.html

Бегло заглянул по Вашей ссылке (по крайней мере первой) и понял, что с доброй половиной сказанного готов поспорить. Кстати, википедия - не единственный источник, в котором я встречал заявления об "истинности" $G$.

Особенно мне не понравилось вот это:
"...the fact that G states that it is not provable in T is not something that requires "stepping outside the system" to see".

[маткиб]

epros писал(а):

То, что Вы говорите, в принципе правильно, но недостаточно конкретно. Вот Вы говорите: "На каком-то уровне придётся пользоваться ...", не уточняя что за "уровень". А в итоге - у каждого своё понимание этого уровня и не факт, что одинаковое. А значит неизбежны ситуации, когда мы с Вами неверно оценим уровни формализации, подразумеваемые друг другом.

Я же имею в виду вполне конкретный уровень формализации, дальше которого можно было бы опуститься, но "не нужно". Речь идёт об уровне, на котором каждое математическое понятие сводится к строке символов. Т.е. глубже базовых понятий о символах, алфавите, составлении строк из символов и базовых операций со строками мы не опускаемся. Но до этого уровня мы формализацию довести должны.

Во-первых, мы не только должны довести формализацию до такого уровня, но и объяснить пользователю, что означают (какое отношение они имеют к объективной реальности) эти строки символов, и чтобы пользователь понял это однозначно. К сожалению, это объяснение уже не может быть формальным. А, во-вторых, мы должны уметь определять каким-то образом адекватность нашей формализации (что тоже не может быть полностью формальным).

epros писал(а):

маткиб писал(а):

epros писал(а):

Вы слишком плохо думаете о конструктивистах.

Я вообще плохо думаю о людях, которые прикидываются дураками, хотя на самом деле таковыми не являются.

Раз Вы всерьёз думаете, что они "прикидываются дураками", то Вы действительно плохо о них думаете. Ваша позиция сейчас похожа на позицию школьника, который считает, что математики "прикидываются дураками", когда всерьёз доказывают какие-то теоремы из геометрии, когда всё это можно было бы наглядно продемонстрировать с помощью ножниц и бумаги. Речь идёт о серьёзных вещах - о математической строгости, которая, конечно, в 99% случаев может быть и не нужна, но именно в оставшемся 1% может обнаружится, что всё наше коллективное знание построено на фундаменте непонимания друг друга и, начиная с некоторого уровня технологий, просто перестанет работать (хотя до сих пор, казалось бы, прекрасно работало).

Вы в очередной раз сильно перегибаете палку. А Вы знаете, что такое математическая строгость? Вы понимаете, что если доказывать те же самые теоремы из геометрии, то на каком-то уровне придётся объяснить, какое отношение выписываемые строки символов имеют к геометрическим фигурам, и это объяснение в принципе не может быть формальным?

Иными словами, никакой абсолютной формальности не бывает. Нужно выбрать тот уровень формальности, который при условии вменяемости пользователя не позволит сделать ошибку, но и который при этом позволяет узнать хоть какие-то факты о реальности. Представляете ли Вы себе, что математика очень редко занимается какими-либо вопросами о строках символов? Как правило математика изучает совершенно различные вымышленные сущности, такие, как числа, геометрические фигуры, множества, отображения и т.п.

epros писал(а):

маткиб писал(а):

epros писал(а):

Но просто сравните этот подход с тем, как понятие об арифметике вводится критикуемыми Вами конструктивистами:
1. Натуральное число - это строка из вертикальных чёрточек.
2. Операция инкремента - это добавление к строке одной чёрточки.

1. Это не является определением натурального числа.
2. При наличии опыта этого "определения" вполне достаточно для понимания, что такое натуральное число.
3. К конструктивистам это не имеет никакого отношения (это появилось за не одну тысячу лет до конструктивистов).

1. Вы просто не заметили, что сюда уже заложены все аксиомы Пеано.

Аксиомы Пеано сюда никаким местом не заложены.

epros писал(а):

маткиб писал(а):

Тогда уж буду придираться (хотя сам не люблю, когда этим занимаются): не определено понятие алфавита, грамматики, что значит определять одни понятия на основе других. Да и вообще в таком определении неявно присутствует представление о рекурсии (или индукции), которое предполагает некоторое представление о натуральных числах.

Здесь, конечно, нет полного определения, но кое-что есть:
Алфавит: должен содержать символ "|" (остальное можно добавить по вкусу).
Грамматика: строка из символов "|" является допустимым словом языка и должна интерпретироваться как "натуральное число" (остальные правила можно добавить по вкусу).
И т.д.
Естественно понятия "алфавит", "символ", "строка" и т.п. мы не определяем, считая их базовыми.

А почему не считать базовым понятие множества? Тогда без проблем можно строго определить понятие истинности в арифметике, и не называть истинными доказуемые формулы, как это делаете Вы.

epros писал(а):

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

Скорее, его не следует считать дураком, а либо провокатором (прикидывающимся дураком), либо несчастным человеком, загипнотизированным чужими (или своими) идеями об отсутствии какого-либо объективного смысла в математических построениях. Не вижу ничего противоестественного в том, что, например, теорема Ферма либо истинна, либо ложна (вне зависимости от нашего знания об этом). Аналогично тому, как вне зависимости от нашего знания, например, негры а африке голодают.

epros писал(а):

маткиб писал(а):

Чтобы доказать $G$, Гёдель использовал дополнительно аксиому о корректности арифметики Пеано (если быть точным, в языке арифметики это будет схема аксиом), которая выглядит как $\mathrm{Prf}_{\mathrm{PA}}(\Phi)\rightarrow\Phi$.

Конечно же, в самой теории не может быть такой схемы аксиом. Но, принимая теорию, мы автоматически принимаем и это.

Нет уж, если уж пользоваться Вашим представлением об истинности ($\Phi$ истинна в $T$ тогда и только тогда (по определению), когда $T\vdash\Phi$), то никакого такого автоматического принимания не происходит. Или же уточните, что Вы понимаете под метатеорией.

epros писал(а):

Теории существуют для того, чтобы судить об истинности. А делать это они могут только если мы признаем, что доказательство является способом определения истинности. Так что ничего существенного эта схема аксиом с моей точки зрения не добавляет. С моей точки зрения существенным скорее является способность метатеории судить о высказываниях теории (чего сама теория не может). Это способность не может быть приобретена без, как минимум, расширения алфавита теории.

Уточните, что Вы подразумеваете под метатеорией. А то я Вас совсем перестаю понимать.

[Someone]

epros в сообщении #170366 писал(а):

1. 1 является натуральным числом: "|" = 1 (это просто определение единицы)
2. Число, следующее за натуральным, также является натуральным: Добавление вертикальной чёрточки к строке вертикальных чёрточек даёт строку вертикальных чёрточек.
3. 1 не следует ни за каким натуральным числом: Добавлением вертикальной чёрточки к произвольной непустой строке нельзя получить "|".
4. Если натуральное число a непосредственно следует как за числом b, так и за числом c, то b и c тождественны: Равенство строк b+"|" и c+"|" означает равенство любых соответствующих подстрок, в том числе b и c.
5. Схема индукции - единственная здесь нетривиальная вещь. Но она скорее относится к логике, чем собственно к арифметике. Отказ от неё, насколько я понимаю, просто позволяет расширениям арифметики быть омега-противоречивыми (но не буквально противоречивыми).

Этому мешает, в частности, Ваше отношение к понятию слова (строки символов) как неопределяемому (первичному) понятию. Вам сначала нужно фомализовать это понятие и операции над словами. Без этого, например, непонятно, почему, добавляя к строке палочек ещё одну палочку, мы всегда получаем один и тот же результат (в соответствующей аксиоме сказано "для каждого натурального числа следует единственное, следующее за ним"). Боюсь, что такая формализация будет существенно опираться на представления о натуральных числах и натуральном ряде.

По поводу роли схемы индукции. Она вовсе не сводится к $\omega$-непротиворечивости. У Вас исчезнет практически вся арифметика. Вы даже не сможете определить арифметические операции. И ниоткуда не следует, что всякую строку палочек можно получить, приписывая палочки к строке "|".

epros в сообщении #170366 писал(а):

Я вижу, что здесь заявлено, что это "теорема Гёделя в первоначальной форме", однако, как я понимаю, автор этого заявления Клини, а не Гёдель, так что это всего лишь его интерпретация.

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

Разыскал английский перевод работы Гёделя.

The Undesidable. Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. Edited by Martin Davis.

В первой работе Гёделя в этом сборнике теорема сформулирована так (стр. 24):

Theorem VI. For every $\omega$-consistent recursive class $\varkappa$ of formulas, there exists a recursive class expression $r$ such that neither $v\ Gen\ r$ nor $Neg(v\ Gen\ r)$ belongs to $Flg(\varkappa)$ (where $v$ is free variable of $r$).

Надеюсь, с Гёделем Вы не будете спорить о том, какую именно теорему он доказал?

[epros]

маткиб писал(а):

Во-первых, мы не только должны довести формализацию до такого уровня, но и объяснить пользователю, что означают (какое отношение они имеют к объективной реальности) эти строки символов, и чтобы пользователь понял это однозначно.

Не согласен. Как я уже говорил, не нужно смешивать математику с вопросами её применения (т.е. с тем, какое отношение имеют её утверждения к тем или иным "фактам реальности"). Математика оперирует только символами, а не их "физическим смыслом". Например, в математике достаточно продемонстрировать (доказать), что натуральные числа (в частности, понимаемые как строки вертикальных чёрточек) обладают соответствующими свойствами, а уж вопрос проявления этого свойства при работе с теми или иными физическими объектами касается применения теории, т.е. не относится к математике.

маткиб писал(а):

К сожалению, это объяснение уже не может быть формальным.

Применение любой теории, сколь бы подробно мы ни пытались его описать для пользователя, всегда останется процессом творческим. Достаточно посмотреть, сколько школьников всегда путали и продолжают путать давление с импульсом при решении физических задач, а всё только потому, что они обозначаются одинаковыми буквами.

маткиб писал(а):

А, во-вторых, мы должны уметь определять каким-то образом адекватность нашей формализации (что тоже не может быть полностью формальным).

Что Вы имеете в виду под "адекватностью" формализации? С моей точки зрения формализация (и однозначная) либо есть, и это значит что у нас есть теория, либо её пока нет и это означает, что пока у нас есть только философские рассуждения, из которых ещё неизвестно что может получиться.

маткиб писал(а):

Вы в очередной раз сильно перегибаете палку. А Вы знаете, что такое математическая строгость? Вы понимаете, что если доказывать те же самые теоремы из геометрии, то на каком-то уровне придётся объяснить, какое отношение выписываемые строки символов имеют к геометрическим фигурам, и это объяснение в принципе не может быть формальным?

А что такое "геометрические фигуры"? Нечто, вырезанное ножницами из бумаги? С моей точки зрения - нет. Я полагаю, что геометрическая фигура - это абстрактное понятие, содержанием которого является ровно то, как она определена в теории. А рисунки на бумаге - это всего лишь иллюстрация (или, если хотите, - физическая реализация) геометрических фигур.

маткиб писал(а):

Иными словами, никакой абсолютной формальности не бывает.

Так я ж не спорю.

маткиб писал(а):

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

И это тоже правильно.

маткиб писал(а):

Представляете ли Вы себе, что математика очень редко занимается какими-либо вопросами о строках символов?

Конечно же представляю. "Вопросы о строках символов" предлагаются всего лишь в качестве универсального фундамента для формализации. Далеко не каждое рассуждение должно "упираться в фундамент". И математические доказательства зачастую содержат большое количество человеческих слов, а не состоят из одних только формул в языке логики первого порядка.

маткиб писал(а):

Как правило математика изучает совершенно различные вымышленные сущности, такие, как числа, геометрические фигуры, множества, отображения и т.п.

Да это пожалуйста. Главное, чтобы эти "вымышленные сущности" могли получить однозначное определение. Вон Кантор измыслил сущность: "множество всех множеств", но оказалось, что для неё никак не удаётся дать непротиворечивого определения.

маткиб писал(а):

Аксиомы Пеано сюда никаким местом не заложены.

Не знаю, что Вы хотели сказать Вашим возражением, но я своим утверждением хотел сказать простую вещь: Аксиомы Пеано представляют собой свойства натуральных чисел, а для строк вертикальных чёрточек эти свойства непосредственно удовлетворяются.

маткиб писал(а):

А почему не считать базовым понятие множества? Тогда без проблем можно строго определить понятие истинности в арифметике, и не называть истинными доказуемые формулы, как это делаете Вы.

Ничего себе базовое понятие, для адекватного понимания которого требуется куча нетривиальных аксиом. И я не понимаю, как это помогает строго определить понятие истинности в арифметике? Разумеется, арифметика - часть теории множеств, но разве отюда следует, что в теории множеств множно найти конкретное значение истинности для любого конкретного арифметического высказывания? Конечно же сам факт, что арифметика - часть теории множеств, означает, что с позиции веры в состоятельность теории множеств мы должны автоматически считать арифметику состоятельной. Но обоснование состоятельности теории с позиций более сложной (более содержательной) теории представляется мне абсолютно неубедительным. Сложные вещи должны обосновываться простыми (и очевидными в силу своей простоты), а не наоборот.

маткиб писал(а):

Скорее, его не следует считать дураком, а либо провокатором (прикидывающимся дураком), либо несчастным человеком, загипнотизированным чужими (или своими) идеями об отсутствии какого-либо объективного смысла в математических построениях.

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

маткиб писал(а):

Не вижу ничего противоестественного в том, что, например, теорема Ферма либо истинна, либо ложна

А я вижу это утверждение не "противоестественным", а просто бессодержательным, т.е.ничего не утверждающим. Почему-то на вопрос: "Каково значение истинности у такого-то утверждения", мы в таких случаях получаем ответ: "Либо истинно, либо ложно", который на самом деле ответом на этот вопрос явно не является.

Вот я спрошу Вас: "Не упадёт ли на мой дом завтра метеорит, т.е. не нужно ли мне строчно эвакуировать семью"? А Вы мне ответите: "Я точно знаю, что либо упадёт, либо нет". Замечательно. Но я-то хотел не этого. Для меня вопрос важен: он жизни моей семьи касается. Если не знаете, то не морочьте голову и просто признайтесь в этом, я тогда поищу ответ в другом месте.

маткиб писал(а):

(вне зависимости от нашего знания об этом). Аналогично тому, как вне зависимости от нашего знания, например, негры а африке голодают.

Вот именно: Вы берётесь рассуждать о чём-то, существующем "вне зависимости от Вашего знания", на самом деле не зная об этом ничего. А я берусь рассуждать только о том, что знаю (не исключая возможности ошибок, конечно).

маткиб писал(а):

Нет уж, если уж пользоваться Вашим представлением об истинности ($\Phi$ истинна в $T$ тогда и только тогда (по определению), когда $T\vdash\Phi$), то никакого такого автоматического принимания не происходит. Или же уточните, что Вы понимаете под метатеорией.

Под метатеорией по отношению к теории $T$ я понимаю теорию, способную судить (формулировать утверждения) о высказываниях в синтаксисе $T$, в том числе об их доказуемости (в $T$) и/или истинности (вне зависимости от $T$).

Ваше возражение я не понял. Я не говорил, что $\Phi$ "истинно в $T$" тогда и только тогда, когда $T\vdash\Phi$. Я говорил, что из $T\vdash\Phi$ следует $\Phi$, если теория $T$ принята. Если она сомнительна, то нет.

Добавлено спустя 1 час 16 минут 6 секунд:

Someone писал(а):

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

Это вопрос равенства строки самой себе. Ответ на него я предлагаю считать очевидным как раз в силу базовости понятия строки символов: вряд ли найдётся индивид, который будет утверждать, что могут быть принципиально неразличимые (но объективно "разные") строки.

Так что с моей точки зрения это формализации не требует.

Someone писал(а):

По поводу роли схемы индукции. Она вовсе не сводится к $\omega$-непротиворечивости. У Вас исчезнет практически вся арифметика. Вы даже не сможете определить арифметические операции. И ниоткуда не следует, что всякую строку палочек можно получить, приписывая палочки к строке "|".

Хм. Я полагал, что отсутствие схемы индукции приводит лишь к тому, что, имея $(\forall k \in \mathbb{N})(\vdash \phi(k))$, мы не можем получить $\vdash (\forall k \in \mathbb{N})(\phi(k))$. Т.е. на примере Вашего замечания: Зная, что мы можем получить всякую строку палочек приписыванием по одной палочке, мы не можем утверждать, что это утверждение относится к арифметике. С моей точки зрения это проблема не арифметики, а логики. Насколько я понимаю, в конструктивном анализе она решается принятием т.н. "абстракции потенциальной реализуемости", т.е. отсутствие технической возможности проверить это на строке достаточно большой длины не является препятствием для того, чтобы утвержать, что это верно для строки любой длины.

Someone писал(а):

Надеюсь, с Гёделем Вы не будете спорить о том, какую именно теорему он доказал?

Нет, с Гёделем спорить не буду. Собственно, суть вопроса состояла не в том, кому именно принадлежит авторство, а в том, есть ли вообще такая теорема, которая утверждает не только неразрешимость $G$, но и его "истинность".

[Someone]

epros в сообщении #170827 писал(а):

Это вопрос равенства строки самой себе. Ответ на него я предлагаю считать очевидным как раз в силу базовости понятия строки символов: вряд ли найдётся индивид, который будет утверждать, что могут быть принципиально неразличимые (но объективно "разные") строки.

Почему неразличимые? Вполне себе различимые. Один раз приписали к строке $n$ палочку - получили один результат. Другой раз проделали то же самое - получили другой результат.

Вы, конечно, ведёте себя подобно другим интуиционистам. Они заявляют о достигнутом ими уровне строгости, совершенно недоступном и даже невообразимом для тех, кто занимается классической математикой, и тут же объявляют, что не желают как либо формализовать применяемые средства доказательства, считая допустимым использовать всё, что им кажется "интуитивно убедительным".

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

Тем не менее, если Вы явно не сформулируете аксиому, что приписываие символа даёт всегда однозначный результат, то однозначности и не будет.

epros в сообщении #170827 писал(а):

Зная, что мы можем получить всякую строку палочек приписыванием по одной палочке, мы не можем утверждать, что это утверждение относится к арифметике.

Не сформулировав явно в виде аксиомы, что любую строку можно получить последовательным приписыванием (по одному символу) к пустой строке (или, если Вы не хотите рассматривать пустую строку - к односимвольным строкам), Вы это доказать не сможете, несмотря ни на какую "интуитивную убедительность". А это и есть аксиома индукции, причём, в первоначальном теоретико-множественном варианте. Если же Вы не захотите впутывать в это дело теорию множеств и сформулируете схему аксиом индукции, то "вылезут" нестандартные модели (даже несчётные), которые, честно говоря, противоречат моим интуитивным представлениям о натуральном ряде. А нестандартные модели натурального ряда порождают такие же нестандартные модели вычислительного процесса.

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

epros в сообщении #170827 писал(а):

Собственно, суть вопроса состояла не в том, кому именно принадлежит авторство, а в том, есть ли вообще такая теорема, которая утверждает не только неразрешимость $G$, но и его "истинность".

Ну, Вы, кажется, утверждали, что только такая теорема и есть.
Гёдель об этом говорит (в указанном сборнике - на странице 9), но в доказательстве никак не использует и в формулировку теоремы не включает. Вероятно, потому, что истинность предполагает некоторую (стандартную) интерпретацию теории с определёнными свойствами.

Цитата:

From the remark that $[R(q);q]$ usserts its own unprovability it follows immediately that $[R(q);q]$ is true, since $[R(q);q]$ is indeed unprovable (because it is undecidable).

[маткиб]

epros писал(а):

маткиб писал(а):

Во-первых, мы не только должны довести формализацию до такого уровня, но и объяснить пользователю, что означают (какое отношение они имеют к объективной реальности) эти строки символов, и чтобы пользователь понял это однозначно.

Не согласен. Как я уже говорил, не нужно смешивать математику с вопросами её применения (т.е. с тем, какое отношение имеют её утверждения к тем или иным "фактам реальности"). Математика оперирует только символами, а не их "физическим смыслом".

Математика не оперирует с физическим смыслом, но зато оперирует с математическим. Строки символов должны быть не просто взятыми с потолка, а отражать свойства некоторого созданного в мышлении мира вымышленных сущностей.

epros писал(а):

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

Вот именно, что нужно доказать, что натуральные числа обладают некоторыми свойствами, либо сформулировать таковые свойства в виде аксиом, но ни в коем случае не выписать набор аксиом произвольно, и выводить из них следствия.

epros писал(а):

Что Вы имеете в виду под "адекватностью" формализации?

Под адекватностью я понимаю её соответствие тому миру вымышленных сущностей, который мы с помощью этой формализации собираемся описать.

epros писал(а):

А что такое "геометрические фигуры"? Нечто, вырезанное ножницами из бумаги? С моей точки зрения - нет. Я полагаю, что геометрическая фигура - это абстрактное понятие, содержанием которого является ровно то, как она определена в теории. А рисунки на бумаге - это всего лишь иллюстрация (или, если хотите, - физическая реализация) геометрических фигур.

В принципе, Вы правы. Но надо не забывать, что сначала у людей появилось некоторое представление о геометрических фигурах (как о формах предметов окружающего мира), затем люди пытались это понятие как-то формализовать, и лишь потом появились определения. Вообще, геометрические фигуры - это плохой пример, потому что без определения это понятие реально понимается людьми неоднозначно. Лучше здесь в качестве примера приводить натуральные числа (строки из вертикальных палочек, как Вы выражаетесь). Например, увидев Ваше определение через вертикальные палочки нормальный человек начинает понимать, что такое натуральное число (причём разные люди одинаково), но из этого Вашего опредедения практически никаких свойств этих чисел не следует, эти свойства люди придумывают уже после, и выписывают их в виде аксиом. Некоторые свойства очень даже нетривиальные. Например, аксиоматику ZFC можно переписать как аксиоматику натуральных чисел. Я категорически не согласен с тем, что задача выдумывания таких аксиом не относится к математике.

epros писал(а):

маткиб писал(а):

Аксиомы Пеано сюда никаким местом не заложены.

Не знаю, что Вы хотели сказать Вашим возражением, но я своим утверждением хотел сказать простую вещь: Аксиомы Пеано представляют собой свойства натуральных чисел, а для строк вертикальных чёрточек эти свойства непосредственно удовлетворяются.

Они выполняются для натуральных чисел, но я не согласен с тем, что они выполняются непосредственно. Никакой непосредственности тут нет. Аксиомы Пеано - это результат длительного размышления математиков о натуральных числах. Вот, допустим, Вы видите только Ваше определение через вертикальные чёрточки. Как из этого определения Вы получили аксиомы Пеано? Или это, по-Вашему, не относится к математике? Как, по-Вашему, из Вашего определения получить следующее:
1) Догадаться, что можно на строках вертикальных палочек ввести сложение, умножение и предикат равенства?
2) Догадаться, что для сложения и умножения выполняются аксиомы Пеано (кроме индукции)?
3) Догадаться, что выполняется аксиома индукции $P(0)\&(\forall x)(P(x)\rightarrow P(x+1))\rightarrow P(x)$, где P - любая формула первого порядка с функциональными символами сложения, умножения, прибавления единицы и предикатом равенства? Между прочим, расширив язык для P, мы можем сильно увеличить возможности аксиоматики по доказательству теорем (в том числе, записанных в старом языке). Кстати, из-за неочевидности (неконструктивности) этой схемы индукции, часто рассматривают её ограниченные варианты, например, такие, в которых P имеет вид $(\exists x_1)\ldots(\exists x_n)\Phi$, где $\Phi$ - бескванторная формула.

Если подумать, то можно аксиоматику сформулировать как теорию о натуральных числах и множествах натуральных чисел, тогда она будет значительно сильнее аксиоматики Пеано, в частности, позволять доказывать свойства натуральных чисел, которые можно сформулировать, но нельзя доказать в арифметике Пеано. Или же можно подумать и догадаться, что схема аксиом $\mathrm{Prf}_{\mathrm{ZFC}}(\Phi)\rightarrow\Phi$ тоже является свойством строк вертикальных палочек. Добавив её, мы получим возможность не расширяя языка доказывать всё то (из того, что можно в этом языке сформулировать), что доказуемо в ZFC, и даже чуть-чуть больше, а это значительно расширяет арифметику Пеано. Но как это следует из Вашего определения на основе палочек, ума не приложу.

epros писал(а):

маткиб писал(а):

А почему не считать базовым понятие множества? Тогда без проблем можно строго определить понятие истинности в арифметике, и не называть истинными доказуемые формулы, как это делаете Вы.

Ничего себе базовое понятие, для адекватного понимания которого требуется куча нетривиальных аксиом.

Множество можно считать таким же базовым понятием, как Ваши строки вертикальных палочек (если особо не заморачиваться).

epros писал(а):

И я не понимаю, как это помогает строго определить понятие истинности в арифметике? Разумеется, арифметика - часть теории множеств, но разве отюда следует, что в теории множеств множно найти конкретное значение истинности для любого конкретного арифметического высказывания?

А никто и не просит это значение находить, достаточно только дать ему определение.

epros писал(а):

Но обоснование состоятельности теории с позиций более сложной (более содержательной) теории представляется мне абсолютно неубедительным. Сложные вещи должны обосновываться простыми (и очевидными в силу своей простоты), а не наоборот.

Если множество вообще - это сложное понятие (в принципе, я с этим согласен), то можно рассматривать множества натуральных чисел, которые настолько же очевидны, насколько сами числа (строки палочек). На основе множеств натуральных чисел без проблем можно строго определить понятие истинности в языке арифметики первого порядка.

epros писал(а):

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

Аксиомы не берутся с потолка, они всегда являются следствием попытки описать некоторый вымышленный мир. Бывали, конечно, случаи, когда аксиомы придумывались без достаточно ясного представления об объекте, который нужно было описать, тогда и получались "парадоксы Рассела". Но это скорее указание на то, что не нужно пытаться описывать аксиомами "то, не знаю что".

epros писал(а):

маткиб писал(а):

Не вижу ничего противоестественного в том, что, например, теорема Ферма либо истинна, либо ложна

А я вижу это утверждение не "противоестественным", а просто бессодержательным, т.е.ничего не утверждающим.

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

[epros]

Someone писал(а):

Почему неразличимые? Вполне себе различимые. Один раз приписали к строке $n$ палочку - получили один результат. Другой раз проделали то же самое - получили другой результат.

Каким же образом? a+"|" = a+"|" уже потому, что равенство строк определяется посимвольным сравнением, а раз a=a, то как могут возникнуть "разные результаты" мне просто непонятно.

Someone писал(а):

Вы, конечно, ведёте себя подобно другим интуиционистам. Они заявляют о достигнутом ими уровне строгости, совершенно недоступном и даже невообразимом для тех, кто занимается классической математикой, и тут же объявляют, что не желают как либо формализовать применяемые средства доказательства, считая допустимым использовать всё, что им кажется "интуитивно убедительным".

Ну нет. Во-первых, я говорю не о "невообразимом" уровне строгости, а просто о предварительно оговоренном. Во-вторых, касательно "интуитивной убедительности" я с интуиционистами как раз расхожусь. Я считаю возможным признавать очевидными только те вещи, которые лежат глубже того самого предварительно оговоренного уровня строгости.

Someone писал(а):

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

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

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

Что касается представлений о "натуральном ряде как совокупности всех натуральных чисел", то тут я с Вами не согласен. Из представлений о том, что такое строки, не следует никаких представлений о том, что такое "совокупность всех строк" или "совокупность всех строк определённого вида".

Someone писал(а):

Тем не менее, если Вы явно не сформулируете аксиому, что приписываие символа даёт всегда однозначный результат, то однозначности и не будет.

Не понял, что мешает нам сформулировать такую аксиому, раз это относится к сфере наших базовых представлений о строках?

Someone писал(а):

epros в сообщении #170827 писал(а):

Зная, что мы можем получить всякую строку палочек приписыванием по одной палочке, мы не можем утверждать, что это утверждение относится к арифметике.

Не сформулировав явно в виде аксиомы, что любую строку можно получить последовательным приписыванием (по одному символу) к пустой строке (или, если Вы не хотите рассматривать пустую строку - к односимвольным строкам), Вы это доказать не сможете, несмотря ни на какую "интуитивную убедительность".

Ну так сформулируем. Как часть аксиоматики Пеано, следующую из наших базовых представлений о строках.

Someone писал(а):

А это и есть аксиома индукции, причём, в первоначальном теоретико-множественном варианте.

Я не возражаю против того, что в этом заложены представления об индукции. Но я не понял, в чём тут их "теоретико-множественный вариант".

Someone писал(а):

Если же Вы не захотите впутывать в это дело теорию множеств и сформулируете схему аксиом индукции, то "вылезут" нестандартные модели (даже несчётные), которые, честно говоря, противоречат моим интуитивным представлениям о натуральном ряде. А нестандартные модели натурального ряда порождают такие же нестандартные модели вычислительного процесса.

М-мм. Это я как-то пока не осмыслил.

Someone писал(а):

Ну, Вы, кажется, утверждали, что только такая теорема и есть.
Гёдель об этом говорит (в указанном сборнике - на странице 9), но в доказательстве никак не использует и в формулировку теоремы не включает. Вероятно, потому, что истинность предполагает некоторую (стандартную) интерпретацию теории с определёнными свойствами.

Цитата:

From the remark that $[R(q);q]$ usserts its own unprovability it follows immediately that $[R(q);q]$ is true, since $[R(q);q]$ is indeed unprovable (because it is undecidable).

Ну так вывод какой? Можно утверждать, что существует $G$, не только неразрешимое, но и "истинное", или Гёдель это сгоряча брякнул и теоремы из этого не получится?

Добавлено спустя 2 часа 4 минуты 2 секунды:

маткиб писал(а):

epros писал(а):

маткиб писал(а):

Во-первых, мы не только должны довести формализацию до такого уровня, но и объяснить пользователю, что означают (какое отношение они имеют к объективной реальности) эти строки символов, и чтобы пользователь понял это однозначно.

Не согласен. Как я уже говорил, не нужно смешивать математику с вопросами её применения (т.е. с тем, какое отношение имеют её утверждения к тем или иным "фактам реальности"). Математика оперирует только символами, а не их "физическим смыслом".

Математика не оперирует с физическим смыслом, но зато оперирует с математическим. Строки символов должны быть не просто взятыми с потолка, а отражать свойства некоторого созданного в мышлении мира вымышленных сущностей.

Выше Вы говорили об отношении к "объективной реальности", а теперь - об отношении к "миру вымышленных сущностей", с чем я в ещё большей степени не согласен. Конечно же строки не нужно брать "с потолка". Приоритет в развитии должны получать те теории, у которых более очевидны перспективы применения. Но это не отменяет того факта, что математика оперирует символами, а не "смыслом" ("физический" он или "математический"). Хотя, возможно, что под "смыслом" Вы здесь как раз и понимаете предполагаемые перспективы применения (против чего у меня нет возражений).

маткиб писал(а):

epros писал(а):

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

Вот именно, что нужно доказать, что натуральные числа обладают некоторыми свойствами, либо сформулировать таковые свойства в виде аксиом, но ни в коем случае не выписать набор аксиом произвольно, и выводить из них следствия.

Я не уловил разницы между "сформулировать свойства в виде аксиом" и "выписать набор аксиом произвольно". Я совершенно согласен, что аксиомы не должны вводиться "произвольно". Соответствующие свойства рассматриваемых математических объектов должны либо непосредственно следовать из наших базовых представлений о математических объектах (коими по моим понятиям являются строки символов), либо должны быть мета-выводимыми для соответствующего типа объектов, которые рассматриваются в рамках соответствующей частной теории.

маткиб писал(а):

epros писал(а):

Что Вы имеете в виду под "адекватностью" формализации?

Под адекватностью я понимаю её соответствие тому миру вымышленных сущностей, который мы с помощью этой формализации собираемся описать.

Насколько я понял, "мир вымышленных сущностей" неформализуем, а стало быть Ваше понятие об адекватности также неформализуемо. И это было бы ничего, если бы понятие "адекватности" было общеочевидным (подобно понятию о строке символов). Но так ведь нет же: я на 99% уверен, что практически у всех, включая математиков, специализирующихся в одной и той же области, представления об этом весьма различны.

маткиб писал(а):

Например, увидев Ваше определение через вертикальные палочки нормальный человек начинает понимать, что такое натуральное число (причём разные люди одинаково), но из этого Вашего опредедения практически никаких свойств этих чисел не следует, эти свойства люди придумывают уже после, и выписывают их в виде аксиом.

Как это не следует? То, что добавлением чёрточки к строке чёрточек мы получим строку чёрточек, следует из наших базовых представлений о строках. Остаётся только зафиксировать это в форме аксиомы. Тут ничего не нужно "придумывать": базовые представления уже существуют и они очевидным образом одинаковы у всех.

маткиб писал(а):

Некоторые свойства очень даже нетривиальные. Например, аксиоматику ZFC можно переписать как аксиоматику натуральных чисел. Я категорически не согласен с тем, что задача выдумывания таких аксиом не относится к математике.

Нетривиальные свойства с моей точки зрения следует доказывать, а не "выдумывать" и сразу после этого закладывать в аксиоматику. Если Вы хотите создать частную теорию, оперирующую объектами только определённого типа (т.е. обладающими определёнными свойствами), то Вы, конечно, можете заложить соответствующие свойства в аксиоматику этой частной теории, но если Вы не хотите, чтобы это была теория ни о чём, то неплохо было бы для начала доказать (в метатеории) , что объекты с такими свойствами существуют.

маткиб писал(а):

Они выполняются для натуральных чисел, но я не согласен с тем, что они выполняются непосредственно. Никакой непосредственности тут нет. Аксиомы Пеано - это результат длительного размышления математиков о натуральных числах. Вот, допустим, Вы видите только Ваше определение через вертикальные чёрточки. Как из этого определения Вы получили аксиомы Пеано? Или это, по-Вашему, не относится к математике?

Непосредственно следуют из базовых представлений о строках. Результатом длительного размышления математиков является то, что аксиоматики Пеано достаточно для построения всей арифметики. А то, что строки чёрточек удовлетворяют таким-то свойствам, как я полагаю, можно было спросить и у древнего предка Халдеев, и он бы дал такой же ответ, как любой современный человек.

маткиб писал(а):

Как, по-Вашему, из Вашего определения получить следующее:
1) Догадаться, что можно на строках вертикальных палочек ввести сложение, умножение и предикат равенства?

Сложение и умножение вводятся для операций со строками чёрточек, очевидно, в точности таким же образом, как и для "абстрактной арифметики", определяемой аксиомами Пеано.

Равенство для строк уже введено, здесь ничего добавлять не нужно.

маткиб писал(а):

2) Догадаться, что для сложения и умножения выполняются аксиомы Пеано (кроме индукции)?

Я не понял, что Вы имеете в виду. Аксиомы Пеано вроде бы не про сложение и умножение. Сложение и умножение определяются через операцию инкремента и, естественно, по этой причине никак нарушить аксиомы Пеано не могут.

маткиб писал(а):

3) Догадаться, что выполняется аксиома индукции $P(0)\&(\forall x)(P(x)\rightarrow P(x+1))\rightarrow P(x)$, где P - любая формула первого порядка с функциональными символами сложения, умножения, прибавления единицы и предикатом равенства?

То, что выполняется аксиома индукции, догадаться можно только с привлечением того, что у конструктивистов называется "абстракция потенциальной осуществимости" (или "реализуемости"). Это представление о том, что не смотря на технические ограничения "в принципе" можно составить любую строку. Оно тоже относится к базовым представлениям (как и всё, касающееся операций со строками).

маткиб писал(а):

Между прочим, расширив язык для P, мы можем сильно увеличить возможности аксиоматики по доказательству теорем (в том числе, записанных в старом языке). Кстати, из-за неочевидности (неконструктивности) этой схемы индукции, часто рассматривают её ограниченные варианты, например, такие, в которых P имеет вид $(\exists x_1)\ldots(\exists x_n)\Phi$, где $\Phi$ - бескванторная формула.

Если подумать, то можно аксиоматику сформулировать как теорию о натуральных числах и множествах натуральных чисел, тогда она будет значительно сильнее аксиоматики Пеано, в частности, позволять доказывать свойства натуральных чисел, которые можно сформулировать, но нельзя доказать в арифметике Пеано. Или же можно подумать и догадаться, что схема аксиом $\mathrm{Prf}_{\mathrm{ZFC}}(\Phi)\rightarrow\Phi$ тоже является свойством строк вертикальных палочек. Добавив её, мы получим возможность не расширяя языка доказывать всё то (из того, что можно в этом языке сформулировать), что доказуемо в ZFC, и даже чуть-чуть больше, а это значительно расширяет арифметику Пеано.

Я не вполне понял о чём Вы здесь.

маткиб писал(а):

Но как это следует из Вашего определения на основе палочек, ума не приложу.

Полагаю, что ровно таким же образом, как это должно (или не должно?) следовать из аксиоматики Пеано самой по себе.

маткиб писал(а):

Множество можно считать таким же базовым понятием, как Ваши строки вертикальных палочек (если особо не заморачиваться).

Что значит "не особо заморачиваться"? Т.е. не задавать вопросов типа: "Существует ли множество всех натуральных чисел?", "множество всех множеств натуральных чисел?", "множество вообще всех множеств?".

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

маткиб писал(а):

А никто и не просит это значение находить, достаточно только дать ему определение.

Правильно ли я понял, что это определение будет звучать примерно так:
"Истинность - это элемент множества из двух элементов"?

Не понимаю, какая от этого определения польза.

маткиб писал(а):

Если множество вообще - это сложное понятие (в принципе, я с этим согласен), то можно рассматривать множества натуральных чисел, которые настолько же очевидны, насколько сами числа (строки палочек). На основе множеств натуральных чисел без проблем можно строго определить понятие истинности в языке арифметики первого порядка.

Не согласен, что "множество натуральных чисел" столь же очевидно, как и само понятие натурального числа. Принципиальная возможность построить любую строку из чёрточек - очевидна. Но возможность построить совокупность всех строк из чёрточек - совсем не очевидна.

маткиб писал(а):

Аксиомы не берутся с потолка, они всегда являются следствием попытки описать некоторый вымышленный мир. Бывали, конечно, случаи, когда аксиомы придумывались без достаточно ясного представления об объекте, который нужно было описать, тогда и получались "парадоксы Рассела". Но это скорее указание на то, что не нужно пытаться описывать аксиомами "то, не знаю что".

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

маткиб писал(а):

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

Я не вполне понял о чём Вы здесь. Может быть о том, что можно мета-доказать некоторые утверждения, недоказуемые в арифметике, и далее - мета-мета-доказать некоторые утверждения, недоказуемые уже в мета-арифметике? Так это пожалуйста. Я даже не возражаю против того, чтобы доказанные таким образом утверждения включались в аксиомактику теории, т.е. расширяли аксиомы Пеано. Но что-то мне не верится, чтобы таким образом, т.е. не добавляя взятых с потолка аксиом, можно было получить ZFC.

[маткиб]

epros в сообщении #171143 писал(а):

Выше Вы говорили об отношении к "объективной реальности", а теперь - об отношении к "миру вымышленных сущностей", с чем я в ещё большей степени не согласен.

Человек, пытаясь узнать свойства объективной реальности, конструирует некоторый мир вымышленный сущностей, который, по его мнению, поможет описать некоторые свойства объективной реальности, а потом уже для этого вымышленного мира придумывает аксиомы и правила вывода.

epros в сообщении #171143 писал(а):

Я не уловил разницы между "сформулировать свойства в виде аксиом" и "выписать набор аксиом произвольно".

Однако, разница есть. И, вероятно, Вы это прекрасно понимаете.

epros в сообщении #171143 писал(а):

Насколько я понял, "мир вымышленных сущностей" неформализуем, а стало быть Ваше понятие об адекватности также неформализуемо. И это было бы ничего, если бы понятие "адекватности" было общеочевидным (подобно понятию о строке символов). Но так ведь нет же: я на 99% уверен, что практически у всех, включая математиков, специализирующихся в одной и той же области, представления об этом весьма различны.

Оно так же неформализуемо, как Ваши строки из вертикальных чёрточек. Есть конкретные вещи, для которых понятие адекватности одинаково у нормальных математиков (натуральные числа, например).

epros в сообщении #171143 писал(а):

Результатом длительного размышления математиков является то, что аксиоматики Пеано достаточно для построения всей арифметики.

Это с какого перепугу её достаточно для построения всей арифметики? Что Вы здесь вообще под арифметикой понимаете?

epros в сообщении #171143 писал(а):

Я не понял, что Вы имеете в виду. Аксиомы Пеано вроде бы не про сложение и умножение. Сложение и умножение определяются через операцию инкремента и, естественно, по этой причине никак нарушить аксиомы Пеано не могут.

Сформулируйте тогда Ваши аксиомы Пеано. Потому что мои аксиомы Пеано содержат умножение, и его оттуда не выбросить.

epros в сообщении #171143 писал(а):

Правильно ли я понял, что это определение будет звучать примерно так:

"Истинность - это элемент множества из двух элементов"?

Не понимаю, какая от этого определения польза.

Не обязательно, можно, например, так: истинность - это целое неотрицательное число, меньшее 2. Про пользу я уже писал, только Вы не осознали.

epros в сообщении #171143 писал(а):

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

Это всего лишь Ваше личное неверное мнение

epros в сообщении #171143 писал(а):

Я не вполне понял о чём Вы здесь. Может быть о том, что можно мета-доказать некоторые утверждения, недоказуемые в арифметике, и далее - мета-мета-доказать некоторые утверждения, недоказуемые уже в мета-арифметике? Так это пожалуйста. Я даже не возражаю против того, чтобы доказанные таким образом утверждения включались в аксиомактику теории, т.е. расширяли аксиомы Пеано. Но что-то мне не верится, чтобы таким образом, т.е. не добавляя взятых с потолка аксиом, можно было получить ZFC.

Ответьте на простой вопрос: как определить, какая строка символов (языка арифметики Пеано) является свойством натуральных чисел (строк вертикальных палочек), а какая нет?