Теорема Лёба

[Мат]

Это все лажа для тех, кто ленится и не может доказывать - тот выдумывает такие теоремы! А кто-то их воспевает . Леб был лодырем и бездельником, вот и выдумал, как ничего не делать

[маткиб]

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

Давайте уж остановимся на чем-то одном:

1. Либо Вы признаёте неконструктивные доказательства, и тогда, неконструктивно доказав, что "доказательство существует", Вы можете быть уверены, что доказательство "реально имеется".

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

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

Мне этот пример пока непонятен. Я понимаю, что высказывание "ZFC противоречива" можно арифметизировать по Гёделю, а потом получившееся арифметическое выражение добавить к ZFC в качестве новой аксиомы. Но мне не очевидно, что в итоге мы получим противоречивую теорию (в смысле ..., откуда следует доказуемость 2+2=5).

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

P.S. В качестве упражнения рекомендую любыми средствами (кроме слепой веры) обосновать, что любое утверждение, для которого $\mathrm{ZFC}\vdash\mathrm{Prf}_{\mathrm{ZFC}}(\Phi)$, доказуемо в ZFC. Очень вытрезвляет.

[epros]

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

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

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

Вы ведь выше описали ситуацию, когда в метатеории доказано, что в теории есть доказательство некоего утверждения. Почему Вы вдруг усомнились в доказательстве своей метатеории и предполагаете, что "формальное доказательство в теории T (строка символов, допускающая машинную проверку)" может "на самом деле" и не существовать?

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

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

По-моему, это замечание не в тему. Я не предлагал Вам запихивать в теорию утверждение о её собственной состоятельности. Речь была о том, что Вы в рамках метатеории сформулировали два противоположных утверждения: $(T \vdash A)$ и $\neg (T \vdash A)$.

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

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

Это весьма упрощённая формулировка. Теория не может даже сформулировать высказывание о собственной противоречивости или непротиворечивости, у неё для этого не хватит выразительных средств. Очевидно, речь идёт о том, что теория может доказать некое утверждение (обозначим его $S$), которое с точки зрения метатеории эквивалентно утверждению о противоречивости теории, что в свою очередь с точки зрения метатеории эквивалентно утверждению о доказуемости в теории того, что 2+2=5.

Фактически $S$ просто утверждает, что существует некое число (а уж метатеория знает, что это число - Гёделевский номер доказательства того, что 2+2=5). Естественно, неконструктивное утверждение о существовании некоторого числа и предъявление этого числа в виде строки в десятичной записи - это существенно разные вещи, второго у нас может и не быть.

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

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

P.S. В качестве упражнения рекомендую любыми средствами (кроме слепой веры) обосновать, что любое утверждение, для которого $\mathrm{ZFC}\vdash\mathrm{Prf}_{\mathrm{ZFC}}(\Phi)$, доказуемо в ZFC. Очень вытрезвляет.

Честно говоря, я не понял, чего Вы здесь от меня ждёте. Доказательства того, что:
$(ZFC \vdash (ZFC \vdash \Phi)) \to (ZFC \vdash \Phi)$


По-моему, это непосильная задача, если это вообще доказуемо.

[маткиб]

epros писал(а):

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

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

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

К сожалению, всё не так просто. И это наглядно показывает теорема Гёделя (вторая), или всё та же теорема Лёба.

epros писал(а):

Вы ведь выше описали ситуацию, когда в метатеории доказано, что в теории есть доказательство некоего утверждения. Почему Вы вдруг усомнились в доказательстве своей метатеории и предполагаете, что "формальное доказательство в теории T (строка символов, допускающая машинную проверку)" может "на самом деле" и не существовать?

По поводу метатеории я нигде никаких сомнений не высказывал (читайте внимательно). Все сомнения относятся к теории T: средставми теории T нельзя такую (нехорошую) ситуацию исключить.

epros писал(а):

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

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

По-моему, это замечание не в тему. Я не предлагал Вам запихивать в теорию утверждение о её собственной состоятельности. Речь была о том, что Вы в рамках метатеории сформулировали два противоположных утверждения: $(T \vdash A)$ и $\neg (T \vdash A)$.

Я этого не делал. У меня в метатеории были утверждения $T\vdash(T\vdash A)$ и $\neg(T\vdash A)$.

epros писал(а):

Очевидно, речь идёт о том, что теория может доказать некое утверждение (обозначим его $S$), которое с точки зрения метатеории эквивалентно утверждению о противоречивости теории, что в свою очередь с точки зрения метатеории эквивалентно утверждению о доказуемости в теории того, что 2+2=5.

Фактически $S$ просто утверждает, что существует некое число (а уж метатеория знает, что это число - Гёделевский номер доказательства того, что 2+2=5). Естественно, неконструктивное утверждение о существовании некоторого числа и предъявление этого числа в виде строки в десятичной записи - это существенно разные вещи, второго у нас может и не быть.

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

Для того конкретного примера моя метатеория отвергает существование такого числа.

epros писал(а):

Честно говоря, я не понял, чего Вы здесь от меня ждёте. Доказательства того, что:
$(ZFC \vdash (ZFC \vdash \Phi)) \to (ZFC \vdash \Phi)$

Именно этого.

epros писал(а):

По-моему, это непосильная задача, если это вообще доказуемо.

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

[epros]

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

epros писал(а):

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

К сожалению, всё не так просто. И это наглядно показывает теорема Гёделя (вторая), или всё та же теорема Лёба.

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

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

Все сомнения относятся к теории T: средставми теории T нельзя такую (нехорошую) ситуацию исключить.

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

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

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

У меня в метатеории были утверждения $T\vdash(T\vdash A)$ и $\neg(T\vdash A)$.

Понятно. Только для полноты въедливости одно маленькое уточнение:
На самом деле $T \vdash B$, $B \leftrightarrow (T \vdash A)$ и $\neg (T \vdash A)$ - вот три утверждения метатеории, о которых, очевидно, идёт речь? (Ибо $T \vdash A$ непосредственно невыразимо средствами теории $T$).

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

Для того конкретного примера моя метатеория отвергает существование такого числа.

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

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

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

epros писал(а):

Честно говоря, я не понял, чего Вы здесь от меня ждёте. Доказательства того, что:
$(ZFC \vdash (ZFC \vdash \Phi)) \to (ZFC \vdash \Phi)$

Именно этого.

epros писал(а):

По-моему, это непосильная задача, если это вообще доказуемо.

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

С моей точки зрения это не особо легче, чем "выяснить" насколько истинно $(ZFC \vdash \Phi) \to \Phi$. А это, как Вы понимаете, есть утверждение о состоятельности ZFC, кое в настоящее время является для математиков не более чем предметом веры (и похоже, что таковым и останется навсегда). Поэтому я и говорю: "непосильная задача".

epros писал(а):

ZFC-доказательство - оно либо существует (можно его выписать на бумажке), либо не существует

Как Вы просто рассудили: либо есть, либо нет. А вот я знаю ещё один вариант: "доселе никому не ведомо". Возьмите в качестве $\Phi$ то же самое утверждение о существовании нечётного совершенного числа.

[маткиб]

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

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

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

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

Как Вы просто рассудили: либо есть, либо нет. А вот я знаю ещё один вариант: "доселе никому не ведомо".

Я бы не стал это называть ещё одним вариантом.

[epros]

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

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

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

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

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

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

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

Как Вы просто рассудили: либо есть, либо нет. А вот я знаю ещё один вариант: "доселе никому не ведомо".

Я бы не стал это называть ещё одним вариантом.

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

[маткиб]

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

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

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

В. И. Арнольд писал(а):

Хорошо известно, что получается, если из учения, веры или науки ​уходит дух, а остаётся один формальный ритуал: получается маразм.

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

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

ZFC - это не предел возможностей мышления (и даже не почти предел).

[epros]

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

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

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

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

В. И. Арнольд писал(а):

Хорошо известно, что получается, если из учения, веры или науки ​уходит дух, а остаётся один формальный ритуал: получается маразм.

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

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

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

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

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

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

ZFC - это не предел возможностей мышления (и даже не почти предел).

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

[маткиб]

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

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

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

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

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

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

Говорить можно, но арифметика (Пеано) может и не ответить на вопрос о доказуемости. А ZFC, например, может. И какой вывод из этого делать? Или ZFC не может, а какая-нибудь более сильная теория может. Что делать в таких случаях?

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

Поэтому Ваше высказывание о том, что "доказательство либо существует, либо нет" представляется мне некорректным.

Совершенно не понимаю, почему оно Вам представляется некорректным.

[epros]

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

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

А вот и нет Не согласен.

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

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

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

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

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

Но вопрос о придумывании таких теорий тоже относится к математике (а к чему же ещё?).

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

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

Если, например, ZFC не позволяет ответить на вопрос, который эквивалентен существованию нужной ракеты, то нужно придумать что-то такое, что позволит ответить на этот вопрос. И заявления о неразрешимости тут недопустимы.

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

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

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

Я не знаю, что Вы называете "принципиальной" неразрешимостью. С моей точки зрения неразрешимость $S$ в $T$ это:
$\neg (T \vdash S) \wedge \neg (T \vdash \neg S)$

Разумеется, это утверждение тоже сформулировано в рамках некой теории (каковая по отношению к $T$ является мета-теорией, ибо может формулировать утверждения касательно того, являются ли те или иные высказывания в синтаксисе $T$ её теоремами). И разумеется, что можно придумать расширение $T$, в котором $S$ будет так или иначе разрешимо.

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

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

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

Говорить можно, но арифметика (Пеано) может и не ответить на вопрос о доказуемости. А ZFC, например, может. И какой вывод из этого делать? Или ZFC не может, а какая-нибудь более сильная теория может. Что делать в таких случаях?

ZFC тут не причём, в ней куча совершенно лишнего и бесполезного с точки зрения решения вопроса разрешимости тех или иных арифметических выражений. Я ведь выше говорил о чём? Допустим, есть некое арифметическое выражение $S$ и мы исследуем вопрос его доказуемости в арифметике Пеано $A$, т.е мы хотим знать: верно ли $A \vdash S$. Обозначим ту теорию, в которой мы пытаемся доказать это высказывание, как $MA$ (мета-арифметика). Бьёмся, бьёмся - ни доказать, ни опровергнуть не можем. Тогда мы "поднимаемся на ступеньку выше" и пытаемся рассмотреть вопрос доказуемости уже в $MA$, т.е. начинаем рассуждать в рамках "мета-мета-арифметики" $MMA$. И вот, "успех" - в рамках $MMA$ нам удаётся совершенно строго доказать, что:
$\neg (MA \vdash (A \vdash S)) \wedge \neg (MA \vdash \neg (A \vdash S))$

Т.е. то, о чём я говорил выше: вопрос о доказуемости в арифметике $S$ неразрешим (в мета-арифметике), и это доказано (в мета-мета-арифметике). Воможна такая ситуация? Я полагаю что да, причём $MA$ и $MMA$ могут не использовать ни одной дополнительной аксиомы по отношению к $A$.

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

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

Поэтому Ваше высказывание о том, что "доказательство либо существует, либо нет" представляется мне некорректным.

Совершенно не понимаю, почему оно Вам представляется некорректным.

Вот это высказывание :
$MA \vdash ((A \vdash S) \vee \neg (A \vdash S))$
Я понимаю, что это не то же самое, что:
$(MA \vdash (A \vdash S)) \vee (MA \vdash \neg (A \vdash S))$
Но одно весьма близко к другому

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

[маткиб]

epros писал(а):

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

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

А вот и нет Не согласен.

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

Дело тут вот в чём. Вообще говоря, нельзя абсолютно строго определить, что такое истинность, например, для формул формальной арифметики (не используя какие-либо другие представления об истинности). Однако, любой нормальный человек способен понять, что это такое, используя свою интуицию натурального ряда и логических операций. Это то, что совершенно разные люди способны понимать одинаково, но не способны это своё понимание формализовать. И из-за этой "неформализуемости" всегда появляются люди, которые намеренно заявляют "я не понимаю, что такое истинность" и на любые попытки им объяснить говорят, что вы не определили то-то и то-то, поэтому разговор беспредметен. К таким людям относятся, например, конструктивисты. Но я не считаю такой подход правильным. Это просто самоограничение. И из-за этого самоограничения теряется смысл математики как инструмента для решения прикладных вопросов. По моему мнению, человек способен иметь некоторое представление о том, что такое арифметическая истинность (если он сам не будет себе мешать), и вполне можно добиться, чтобы разные люди понимали это одинаково, не определениями, но объяснениями (возможно, рукомахательными), поясняющими примерами, которые позволят человеку самому дойти до этого. А когда человек понимает, что такое истинность, он может пытаться формализовать некоторые свойства этой истинности, так появляются корректные формальные теории. Например, любому здравомыслящему математику понятно, что понимается под истинностью, например, теоремы Ферма: уравнение $x^n+y^n=z^n$ не имеет решений в натуральных числах при $n\geq 3$ (несмотря на то, что мало людей могут убедиться, истинно оно или ложно). И человеческий опыт подтверждает, что подобные представления об истинности вполне себе осмысленны (ракеты ведь летают).

epros писал(а):

Допустим, есть некое арифметическое выражение $S$ и мы исследуем вопрос его доказуемости в арифметике Пеано $A$, т.е мы хотим знать: верно ли $A \vdash S$. Обозначим ту теорию, в которой мы пытаемся доказать это высказывание, как $MA$ (мета-арифметика). Бьёмся, бьёмся - ни доказать, ни опровергнуть не можем. Тогда мы "поднимаемся на ступеньку выше" и пытаемся рассмотреть вопрос доказуемости уже в $MA$, т.е. начинаем рассуждать в рамках "мета-мета-арифметики" $MMA$. И вот, "успех" - в рамках $MMA$ нам удаётся совершенно строго доказать, что:
$\neg (MA \vdash (A \vdash S)) \wedge \neg (MA \vdash \neg (A \vdash S))$

Т.е. то, о чём я говорил выше: вопрос о доказуемости в арифметике $S$ неразрешим (в мета-арифметике), и это доказано (в мета-мета-арифметике). Воможна такая ситуация? Я полагаю что да, причём $MA$ и $MMA$ могут не использовать ни одной дополнительной аксиомы по отношению к $A$.

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

[epros]

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

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

"Интуиция - это не то, на чём я стоЮ" (c)

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

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

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

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

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

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

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

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

Скажите теперь, кто ближе к "прикладным вопросам"? И обратите внимание: это при том, что конструктивное определение натурального числа является изначально формализованным (в том смысле, что определены алфавит и грамматика языка формальной теории).

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

Например, любому здравомыслящему математику понятно, что понимается под истинностью, например, теоремы Ферма: уравнение $x^n+y^n=z^n$ не имеет решений в натуральных числах при $n\geq 3$ (несмотря на то, что мало людей могут убедиться, истинно оно или ложно).

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

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

epros писал(а):

Допустим, есть некое арифметическое выражение $S$ и мы исследуем вопрос его доказуемости в арифметике Пеано $A$, т.е мы хотим знать: верно ли $A \vdash S$. Обозначим ту теорию, в которой мы пытаемся доказать это высказывание, как $MA$ (мета-арифметика). Бьёмся, бьёмся - ни доказать, ни опровергнуть не можем. Тогда мы "поднимаемся на ступеньку выше" и пытаемся рассмотреть вопрос доказуемости уже в $MA$, т.е. начинаем рассуждать в рамках "мета-мета-арифметики" $MMA$. И вот, "успех" - в рамках $MMA$ нам удаётся совершенно строго доказать, что:
$\neg (MA \vdash (A \vdash S)) \wedge \neg (MA \vdash \neg (A \vdash S))$

Т.е. то, о чём я говорил выше: вопрос о доказуемости в арифметике $S$ неразрешим (в мета-арифметике), и это доказано (в мета-мета-арифметике). Воможна такая ситуация? Я полагаю что да, причём $MA$ и $MMA$ могут не использовать ни одной дополнительной аксиомы по отношению к $A$.

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

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

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

[nikov]

epros писал(а):

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

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

[маткиб]

epros писал(а):

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

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

"Интуиция - это не то, на чём я стоЮ" (c)

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

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

epros писал(а):

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

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

epros писал(а):

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

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

epros писал(а):

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

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

epros писал(а):

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

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

epros писал(а):

Скажите теперь, кто ближе к "прикладным вопросам"? И обратите внимание: это при том, что конструктивное определение натурального числа является изначально формализованным (в том смысле, что определены алфавит и грамматика языка формальной теории).

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

epros писал(а):

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

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

epros писал(а):

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

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

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