Теорема Лёба

[Someone]

nikov в сообщении #175187 писал(а):

А что за аксиоматика такая?

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

Соответственно, в его аксиоматику входит интуиционистская логика, в которой закона исключённого третьего нет.

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

[nikov]

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

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

Как же это можно сделать?

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

epros писал(а):

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

То есть на вопрос: "существует ли простое число, больше чем $10^{10^{10}}?$" настоящий математик может лишь ответить "я знаю только, что из этих наборов значков с помощью таких правил можно получить вот такой набор значков", указав на формулировки аксиом Пеано и теоремы Евклида, "а что там на самом деле, меня не касается". Так?

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

epros писал(а):

Здесь существенна не схема аксиом, построенных с помощью Гёделевской нумерации внутри самой теории (что, конечно же, сложно), а простое утверждение внутри мета-теории (и на её языке, без всякой арифметизации):
$(\forall S \in T)((T \vdash S) \to S)$
Это утверждение читается как: "Теория $T$ доказывает только истинные утверждения" и означает состоятельность теории, что под силу понять и школьнику.

Так что, $\vdash$ - это самостоятельный символ метатеории? Как я понимаю, Гёдель доказывал свою теорему в теории, в которой нет такого символа, и его предикат доказуемости - это именно сложное утверждение о гёделевских номерах.

[маткиб]

epros писал(а):

М-мм, я не понял, что Вы имеете в виду под "приплетанием формальных выводов"?

Вот это

epros писал(а):

С логическими операциями всё не так просто. Например, чтобы доказать отрицание, необходимо доказать неразрешимость алгоритма, доказывающего $\Psi$. Обычно это выполняется путём сведения предположения $\Psi$ к противоречию. Что такое "противоречие" (или "абсурд") - это отдельная песня. Насколько я понимаю, большинство конструктивистов принимают его за базовое (неопределимое) понятие, т.е. полагают, что в любой формальной системе существует высказывание, которое считается очевидным образом неверным. Например, в арифметике таковым можно считать высказывание $1 = 2$. Вывод его из $\Psi$ означает доказательство $\neg \Psi$ (т.е. опровержение $\Psi$).

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

epros писал(а):

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

Замечание номер 1. Арифметизация вовсе не обязана строиться на разложении на простые множители (есть масса других способов).

Замечение номер 2. Если формула утверждает что-то о свойствах очень ресурсоёмкого алгоритма, то из этого вовсе не следует, что сама формула длинная.

Замечание номер 3. Длинные формулы будут получаться, если использовать аксиомы мета(n)-доказуемостей (чем больше n, тем длиннее формулы), а среди аксиом мета($\omega$)-доказуемости будут и достаточно короткие (меньше 1ГБ).

epros писал(а):

Может я туплю,

Очень может быть

epros писал(а):

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

И здесь Вы заблуждаетесь. Пример я уже приводил:
$(\exists n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$,
где $\mathrm{PA}_n$ - мета(n)-арифметика Пеано,
мета($\omega$)-доказуема, но не мета(n) доказуема ни для какого n (потому что Вторая Теорема Гёделя).

Может я туплю, но по-моему это n равно 1. Ведь $0=S(0)$ - это же высказывание в синтаксисе арифметики, правильно? А раз так, то для него должна быть аксиома уже в схеме мета-аксиом первого уровня:
$(\mathrm{PA}_1 \vdash \Phi) \to \Phi$

Из $(\mathrm{PA}_1 \vdash \Phi) \to \Phi$ не следует $(\exists n)(\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi$. Подсказка: первое - это $\neg\Phi\rightarrow(\mathrm{PA}_1\nvdash\Phi)$, а второе - $\neg\Phi\rightarrow(\forall n)(\mathrm{PA}_n\nvdash\Phi)$. Второе из первого не следует.

epros писал(а):

Кстати, доказуемость на мета($\omega$)-уровне только того, что доказуемо на каком-либо из мета(n)-уровней, по-моему следует из достаточно простых соображений:

Как Вы видите, не следует.

Добавлено спустя 13 минут 24 секунды:

nikov писал(а):

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

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

Как же это можно сделать?

Например, так, как это сделано в книге Верещагина и Шеня "Языки и исчисления" на страницах 93-100 (определение истинности - выразимость в арифметике).

[nikov]

epros писал(а):

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

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

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

Как раз-таки недостаточно. Есть примеры интуитивно истинных или доказуемых в ZFC утверждений о натуральных числах, которые не доказуемы, исходя из аксиом Пеано. Примеры я привел выше (http://www.ltn.lv/~podnieks/gt_rus/gram7.htm#pril2, http://www.ltn.lv/~podnieks/gt_rus/gram6.htm#glava65).

epros писал(а):

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

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

epros писал(а):

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

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

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

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

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

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

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

А можно примеры таких свойств?

[маткиб]

nikov в сообщении #175241 писал(а):

А можно примеры таких свойств?

Непротиворечивость арифметики Пеано.

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

Или непротиворечивость арифметики Пеано с непротиворечивостью арифметики Пеано.

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

Тот же самый вариант теоремы Рамсея.

Добавлено спустя 1 минуту 43 секунды:

Теорема Гудстейна
http://en.wikipedia.org/wiki/Goodstein's_theorem

[nikov]

epros писал(а):

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

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

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

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

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

epros писал(а):

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

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

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

Как долго пытаться?

Добавлено спустя 7 минут 27 секунд:

epros писал(а):

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

Более того, Вы даже не сможете определить умножение (т.е. записать формулу P(x,y,z), которая обладала бы свойствами x*y=z). Если это не так, опровергните.

Вы хотите от меня невозможно.

То есть, Вы согласны, что нельзя выписать формулу с тремя свободными переменными $P(x,y,z)$, используя только алфавит $S0=$ (как в формулировке аксиом Пеано из википедии), которая бы имела смысл $x*y=z?$

Добавлено спустя 5 минут 46 секунд:

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

nikov в сообщении #175241 писал(а):

А можно примеры таких свойств?

Непротиворечивость арифметики Пеано.
Или непротиворечивость арифметики Пеано с непротиворечивостью арифметики Пеано.
Тот же самый вариант теоремы Рамсея.

А разве для них достаточно арифметики с кванторами по множествам натуральных чисел?

[epros]

Someone писал(а):

Мы имеем дело с фанатиком конструктивного рекурсивного анализа (CRA),

У-уу, сейчас я Вас тоже как-нибудь обзову...

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

Someone писал(а):

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

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

[маткиб]

nikov в сообщении #175246 писал(а):

А разве для них достаточно арифметики с кванторами по множествам натуральных чисел?

Более, чем достаточно.

[nikov]

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

nikov в сообщении #175246 писал(а):

А разве для них достаточно арифметики с кванторами по множествам натуральных чисел?

Более, чем достаточно.

А где бы посмотреть доказательство?

[epros]

nikov писал(а):

То есть на вопрос: "существует ли простое число, больше чем $10^{10^{10}}?$" настоящий математик может лишь ответить "я знаю только, что из этих наборов значков с помощью таких правил можно получить вот такой набор значков", указав на формулировки аксиом Пеано и теоремы Евклида, "а что там на самом деле, меня не касается". Так?

Нет, на этот вопрос ответ: "Существует".
А что касается того, что "на самом деле", то давайте начнём говорить об этом после того, как чётко определим, что это такое.

nikov писал(а):

Так что, $\vdash$ - это самостоятельный символ метатеории? Как я понимаю, Гёдель доказывал свою теорему в теории, в которой нет такого символа, и его предикат доказуемости - это именно сложное утверждение о гёделевских номерах.

Ну, да, символ метатеории. Но при необходимости можно придумать и другой синтаксис. Что касается Гёделя, то, как я понимаю, своей системой нумерации оно обосновал равносильность утверждения метатеории о доказуемости ($T \vdash S$) и соответствующего высказывания арифметики ($Prf_T(k)$). Понятное дело, что все эти рассуждения можно проделать и на словах, но если уж поставить вопрос о том, чтобы записать это утверждение о равносильности на формальном языке, то как Вы это сделаете, располагая только одной половиной ($Prf_T(k)$) высказывания, и не располагая синтаксическими средствами для выражения того, чему это равносильно?

[маткиб]

nikov в сообщении #175266 писал(а):

А где бы посмотреть доказательство?

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

[epros]

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

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

Ну, дык. Формальный вывод согласно соответствующим правилам вывода. Добавляем к тому, что у нас есть, предположение $\Psi$ (как новую аксиому), и если выводится заведомо абсурдное утверждение, то значит доказано $\neg \Phi$.

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

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

Было бы интересно. Что-нибудь ещё мне нужно уточнить?

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

Замечание номер 1. Арифметизация вовсе не обязана строиться на разложении на простые множители (есть масса других способов).

Существенно менее ресурсоёмкие?

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

Замечание номер 3. Длинные формулы будут получаться, если использовать аксиомы мета(n)-доказуемостей (чем больше n, тем длиннее формулы), а среди аксиом мета($\omega$)-доказуемости будут и достаточно короткие (меньше 1ГБ).

Наверное те самые, которые являются аксиомами мета(n)-доказуемостей для небольших n? Остаётся надеятся, что нам будет достаточно только их.

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

Из $(\mathrm{PA}_1 \vdash \Phi) \to \Phi$ не следует $(\exists n)(\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi$. Подсказка: первое - это $\neg\Phi\rightarrow(\mathrm{PA}_1\nvdash\Phi)$, а второе - $\neg\Phi\rightarrow(\forall n)(\mathrm{PA}_n\nvdash\Phi)$. Второе из первого не следует.

Наверное я неправильно посчитал скобки.
Но всё же остаются два вопроса:
1. Правильно ли я понял, что это утверждение всего лишь означает, что если на каком-то из мета(n)-уровней доказано абсурдное утверждение, то мета($\omega$)-теория доказывает абсурдное утверждение (т.е. противоречива)? Почему тогда то же нельзя сказать о мета(n+1)-теории?
2. Моё рассуждение о конечности любого мета($\omega$)-доказательства ошибочно? В чём именно?

[маткиб]

epros писал(а):

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

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

Ну, дык. Формальный вывод согласно соответствующим правилам вывода. Добавляем к тому, что у нас есть, предположение $\Psi$ (как новую аксиому), и если выводится заведомо абсурдное утверждение, то значит доказано $\neg \Phi$.

А в выводе аксиомы Пеано можно использовать?
Кстати, а не будет ли Ваше определение эквивалентно следующему: формула $\Phi(x)$ называется представляющей частично определённый предикат $P(x)$, если для любого $x$:
1) если $P(x)$ истинно, то $\mathrm{PA}\vdash \Phi(x)$;
1) если $P(x)$ ложно, то $\mathrm{PA}\vdash\neg \Phi(x)$;
1) если $P(x)$ не определено, то $\mathrm{PA}\nvdash \Phi(x)$ и $\mathrm{PA}\nvdash\neg \Phi(x)$.
Если в выводе можно использовать аксиомы Пеано, то, вероятно, получится нечто похожее.

epros писал(а):

Было бы интересно. Что-нибудь ещё мне нужно уточнить?

Кроме того, что мы уточняем, надо бы уточнить формулировку утверждения. Потому что "алгоритм нельзя записать формулой" я не понимаю. Алгоритм - это машина Тьюринга, а формулам у нас (по определению) соответствует другая модель вычислений, т.е. говорить о точном совпадении машин Тьюринга и алгоритмов, соответствующих формулам, как минимум бессмысленно. Т.е. надо сформулировать утверждение с точки зрения вычисляемых функций, типа "для функции $F(x)$, нумерующей формулы теории, не существует формулы, представляющей предикат $y=F(x)$".

epros писал(а):

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

Замечание номер 1. Арифметизация вовсе не обязана строиться на разложении на простые множители (есть масса других способов).

Существенно менее ресурсоёмкие?

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

epros писал(а):

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

Замечание номер 3. Длинные формулы будут получаться, если использовать аксиомы мета(n)-доказуемостей (чем больше n, тем длиннее формулы), а среди аксиом мета($\omega$)-доказуемости будут и достаточно короткие (меньше 1ГБ).

Наверное те самые, которые являются аксиомами мета(n)-доказуемостей для
небольших n?

И те, которые не являются мета(n) доказуемыми ни при каких n.

epros писал(а):

Остаётся надеятся, что нам будет достаточно только их.

Но их недостаточно (хотя надежда и умирает последней ).

epros писал(а):

1. Правильно ли я понял, что это утверждение всего лишь означает, что если на каком-то из мета(n)-уровней доказано абсурдное утверждение, то мета($\omega$)-теория доказывает абсурдное утверждение (т.е. противоречива)?

Странная у Вас формулировка какая-то. А утверждение всего лишь означает, что ни на каком из мета(n)-уровней не может быть доказано абсурдное утверждение ($0=S(0)$).

epros писал(а):

Почему тогда то же нельзя сказать о мета(n+1)-теории?

Да можно наверно.

epros писал(а):

2. Моё рассуждение о конечности любого мета($\omega$)-доказательства ошибочно? В чём именно?

Естественно, оно ошибочно. Ошибка выделена красным.

epros писал(а):

Доказательство - это конечная последовательность формул теории (каждая из которых получена из нескольких предыдущих по правилу вывода или является аксиомой). Поэтому в доказательстве любой теоремы мета($\omega$)-теории используется конечное количество мета($\omega$)-аксиом. А поскольку каждая из мета($\omega$)-аксиом - это аксиома какого-либо из мета(n)-уровней, то среди них есть аксиома, мета(n)-уровень которой максимален. Вот на этом мета(n)-уровне и будет доказуема данная теорема.

[nikov]

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

Я даже аксиоматику такой арифметики с кванторами по множествам натуральных чисел нигде не видел (обычно домысливаю).

http://en.wikipedia.org/wiki/Second_order_arithmetic

[epros]

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

А в выводе аксиомы Пеано можно использовать?

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

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

Кстати, а не будет ли Ваше определение эквивалентно следующему: формула $\Phi(x)$ называется представляющей частично определённый предикат $P(x)$, если для любого $x$:
1) если $P(x)$ истинно, то $\mathrm{PA}\vdash \Phi(x)$;
1) если $P(x)$ ложно, то $\mathrm{PA}\vdash\neg \Phi(x)$;
1) если $P(x)$ не определено, то $\mathrm{PA}\nvdash \Phi(x)$ и $\mathrm{PA}\nvdash\neg \Phi(x)$.
Если в выводе можно использовать аксиомы Пеано, то, вероятно, получится нечто похожее.

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

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

Т.е. надо сформулировать утверждение с точки зрения вычисляемых функций, типа "для функции $F(x)$, нумерующей формулы теории, не существует формулы, представляющей предикат $y=F(x)$".

Ну, давайте так. Только в чём тут уточнение?

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

epros писал(а):

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

Замечание номер 3. Длинные формулы будут получаться, если использовать аксиомы мета(n)-доказуемостей (чем больше n, тем длиннее формулы), а среди аксиом мета($\omega$)-доказуемости будут и достаточно короткие (меньше 1ГБ).

Наверное те самые, которые являются аксиомами мета(n)-доказуемостей для
небольших n?

И те, которые не являются мета(n) доказуемыми ни при каких n.

Не могу понять, откуда возьмутся мета($\omega$)-аксиомы, не являющиеся мета(n)-аксиомами ни для какого n, если мы определяли в качестве мета($\omega$)-аксиом все мета(n)-аксиомы и только их.

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

epros писал(а):

1. Правильно ли я понял, что это утверждение всего лишь означает, что если на каком-то из мета(n)-уровней доказано абсурдное утверждение, то мета($\omega$)-теория доказывает абсурдное утверждение (т.е. противоречива)?

Странная у Вас формулировка какая-то. А утверждение всего лишь означает, что ни на каком из мета(n)-уровней не может быть доказано абсурдное утверждение ($0=S(0)$).

Моя формулировка лишь добавляет к этому: "... если мета($\omega$)-теория непротиворечива". Но, конечно, это подразумевается.

Кстати, значит ли это, что Вашу формулировку можно записать так:
$(\forall n)(\mathrm{PA}_n \nvdash (0=S(0)))$?
Т.е. без всяких импликаций?

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

Естественно, оно ошибочно. Ошибка выделена красным.

Т.е. Вы утверждаете, что в мета($\omega$)-теории появились некоторые новые аксиомы (которых не было ни на одном из мета(n)-уровней)? И пример такой аксиомы - это Ваше утверждение, приведённое выше?

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