Теорема Лёба

[epros]

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

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

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

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

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

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

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

Если бы понимал, то не сказал бы этого.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Продемонстрируйте разницу. Раз уж Ваше мнение "верное".

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

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

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

[маткиб]

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

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

Вот Ваши аксиомы Пеано:
$1\in\mathbb{N}$.
$x\in\mathbb{N}\rightarrow S(x)\in\mathbb{N}$.
$\nexists x\in\mathbb{N}(S(x)=1)$.
$S(b)=a\rightarrow(S(c)=a\rightarrow b=c)$.
$P(1)\rightarrow(\forall n(P(n)\rightarrow P(S(n))\rightarrow\forall n\in\mathbb{N}(P(n)))$.

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

А мои аксиомы Пеано вот здесь (если там не ошиблись):
$a+0=a$.
$a+S(b)=S(a+b)$.
$a\cdot 0=0$.
$a\cdot S(b)=(a\cdot b)+a$.
$\neg(S(a)=0)$.
$S(a)=S(b)\rightarrow a=b$.
$a=b\ \&\ a=c\rightarrow b=c$.
$a=b\rightarrow S(a)=S(b)$.
$A(0)\ \&\ \forall x(A(x)\rightarrow A(S(x)))\rightarrow\forall x A(x)$,
где $A(x)$ - произвольная формула первого порядка с функциональными символами $S$, $\cdot$, $+$, предикатом $=$, константным символом $0$. Язык, используемый в моих аксиомах, позволяет хотя бы сформулировать все разумные первопорядковые утверждения о конечных объектах, и многие из них доказать или опровергнуть (хотя и не все), а вот Ваша - нет. Но и свою аксиоматику Пеано я бы не стал называть формализацией всех свойств строк из вертикальных палочек, записываемых в виде формул этого языка.

epros писал(а):

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

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

По остальным вопросам спорить не буду (устал).

Добавлено спустя 55 секунд:

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

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

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

[epros]

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

Вот Ваши аксиомы Пеано:
$1\in\mathbb{N}$.
$x\in\mathbb{N}\rightarrow S(x)\in\mathbb{N}$.
$\nexists x\in\mathbb{N}(S(x)=1)$.
$S(b)=a\rightarrow(S(c)=a\rightarrow b=c)$.
$P(1)\rightarrow(\forall n(P(n)\rightarrow P(S(n))\rightarrow\forall n\in\mathbb{N}(P(n)))$.

Только они не мои, а Пеано, обо, как я понимаю, именно он сформулировал их в таком составе.

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

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

Вы хотите от меня невозможно. Определения, в том числе определения операций, в теории не "выводятся", они в неё "вводятся". Например, посредством указания свойств операции. В частности, определение операции инкремента вводится в теорию 2-ой, 3-ей и 4-ой из 5-ти приведённых выше формул.

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

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

А мои аксиомы Пеано вот здесь (если там не ошиблись):
$a+0=a$.
$a+S(b)=S(a+b)$.
$a\cdot 0=0$.
$a\cdot S(b)=(a\cdot b)+a$.
$\neg(S(a)=0)$.
$S(a)=S(b)\rightarrow a=b$.
$a=b\ \&\ a=c\rightarrow b=c$.
$a=b\rightarrow S(a)=S(b)$.
$A(0)\ \&\ \forall x(A(x)\rightarrow A(S(x)))\rightarrow\forall x A(x)$,
где $A(x)$ - произвольная формула первого порядка с функциональными символами $S$, $\cdot$, $+$, предикатом $=$, константным символом $0$.

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

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

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

Может быть Вы тогда продемонстрируете, как Вы в Вашей теории определите возведение в степень: $a^b$, не указав никаких свойств этой операции (а пользуясь только возможностями расширенного синтаксиса, т.е. возможностью ставить переменную в позицию верхнего индекса)?

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

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

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

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

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

По-моему, этому ничто не мешает.

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

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

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

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

Если это вопрос "вообще", то базовые представления - это то, с чем заведомо все согласятся, не потребовав обоснования.

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

[маткиб]

epros писал(а):

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

Вот Ваши аксиомы Пеано:
$1\in\mathbb{N}$.
$x\in\mathbb{N}\rightarrow S(x)\in\mathbb{N}$.
$\nexists x\in\mathbb{N}(S(x)=1)$.
$S(b)=a\rightarrow(S(c)=a\rightarrow b=c)$.
$P(1)\rightarrow(\forall n(P(n)\rightarrow P(S(n))\rightarrow\forall n\in\mathbb{N}(P(n)))$.

Только они не мои, а Пеано, обо, как я понимаю, именно он сформулировал их в таком составе.

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

epros писал(а):

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

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

Вы хотите от меня невозможно. Определения, в том числе определения операций, в теории не "выводятся", они в неё "вводятся". Например, посредством указания свойств операции. В частности, определение операции инкремента вводится в теорию 2-ой, 3-ей и 4-ой из 5-ти приведённых выше формул.

Такой подход возможен, но имеет очень важный недостаток: при желании ввести новую операцию приходится расширять синтаксис и добавлять новые аксиомы, при этом нет никакой гарантии, что не появятся противоречия. Например, захочу я ввести новую операцию $P$, введу для неё аксиому $\forall x(S(P(x))=x)$, и выведу в новой теории $S(1)=1$ (бредовое утверждение в старом языке). А вот моя аксоматика Пеано позволяет вводить новые операции, не расширяя синтаксис и не добавляя новых аксиом.

epros писал(а):

Может быть Вы тогда продемонстрируете, как Вы в Вашей теории определите возведение в степень: $a^b$, не указав никаких свойств этой операции (а пользуясь только возможностями расширенного синтаксиса, т.е. возможностью ставить переменную в позицию верхнего индекса)?

Никакого расширенного синтаксиса не нужно, достаточно только того, на основе которого описаны мои аксиомы Пеано. Делается это очень просто: строится формула $P(a,b,c)$, которая, по моему личному мнению, будет выражать свойство $c=a^b$ (как строить такие формулы, описано, например, в книге Верещагина и Шеня "Языки и исчисления" в главе Языки первого порядка/Выразимость в арифметике), потом для $P$ формально доказываются некоторые свойства (например, $P(a,b,c)\rightarrow P(a,b+1,c\cdot a)$). Если пользователю удобно, он может эти доказанные свойства использовать как аксиомы для новой операции, при этом эти "аксиомы" гарантированно не будут давать противоречий. Так я могу ввести и нечисловые операции, например, со строками, графами, программами и т.п. (подразумевая, что они у меня закодированы числами). При этом процесс перевода интересующих пользователя утверждений о различных объектах в этот язык для пользователя значительно проще, чем выяснение истинности утверждений (т.е. это имеет практический смысл). А вот на основе Ваших аксиом Пеано ничего подобного сделать не получится.

epros писал(а):

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

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

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

А я и не говорю про все операции, которые могут прийти в голову. У нас конкретные операции: $+$, $\cdot$, $S$, $0$, $=$. И по отношению к этим операциям аксиомы Пеано (мои) не являются формализацией всех свойств натуральных чисел.

epros писал(а):

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

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

Если это вопрос "вообще", то базовые представления - это то, с чем заведомо все согласятся, не потребовав обоснования.

Конкретный вопрос: какие базовые свойства у натуральных чисел (строк вертикальных палочек), представимые в виде формул первого порядка с константным символом $0$, функциональными символами $+$, $\cdot$, $S$, предикатным символом $=$ (т.е. в том языке, в котором записаны мои аксиомы Пеано)? С какими заведомо все согласятся?

[epros]

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

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

Ну да ладно, это вопрос терминологический. Хотите называть $a \cdot S(b)=(a \cdot b) + a$ "аксиомой Пеано" - на здоровье.

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

Такой подход возможен, но имеет очень важный недостаток: при желании ввести новую операцию приходится расширять синтаксис и добавлять новые аксиомы, при этом нет никакой гарантии, что не появятся противоречия. Например, захочу я ввести новую операцию $P$, введу для неё аксиому $\forall x(S(P(x))=x)$, и выведу в новой теории $S(1)=1$ (бредовое утверждение в старом языке).

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

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

А вот моя аксоматика Пеано позволяет вводить новые операции, не расширяя синтаксис и не добавляя новых аксиом.

Сейчас посмотрим.

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

Никакого расширенного синтаксиса не нужно, достаточно только того, на основе которого описаны мои аксиомы Пеано. Делается это очень просто: строится формула $P(a,b,c)$, которая, по моему личному мнению, будет выражать свойство $c=a^b$ (как строить такие формулы, описано, например, в книге Верещагина и Шеня "Языки и исчисления" в главе Языки первого порядка/Выразимость в арифметике),

А как Вы думаете, эта формула сама по себе разве не является определением операции? И разве нельзя её записать в форме нового утверждения теории (аксиомы)? Например, вот это:
$P(a,b,c) \leftrightarrow a + (S(1) \cdot b) = c$
разве не определяет новую бинарную операцию через операции $+$ и $\cdot$? Вопрос введения для неё нового обозначения (т.е. расширение синтаксиса), по-моему, является чисто формальным.

И, кстати, мне всё-таки любопытно, как именно можно записать формулу $a^b = c$ исключительно через операции сложения, умножения и инкремента?

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

потом для $P$ формально доказываются некоторые свойства (например, $P(a,b,c)\rightarrow P(a,b+1,c\cdot a)$). Если пользователю удобно, он может эти доказанные свойства использовать как аксиомы для новой операции, при этом эти "аксиомы" гарантированно не будут давать противоречий.

Ну разумеется. Добавление аксиомы $a + S(b)=S(a + b)$ тоже не приведёт к противоречиям уже потому, что это есть свойство строк чёрточек по отношению к операции их конкатенации (соединения).

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

А вот на основе Ваших аксиом Пеано ничего подобного сделать не получится.

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

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

А я и не говорю про все операции, которые могут прийти в голову. У нас конкретные операции: $+$, $\cdot$, $S$, $0$, $=$.

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

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

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

Не спорю.

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

Конкретный вопрос: какие базовые свойства у натуральных чисел (строк вертикальных палочек), представимые в виде формул первого порядка с константным символом $0$, функциональными символами $+$, $\cdot$, $S$, предикатным символом $=$ (т.е. в том языке, в котором записаны мои аксиомы Пеано)? С какими заведомо все согласятся?

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

[маткиб]

epros писал(а):

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

Никакого расширенного синтаксиса не нужно, достаточно только того, на основе которого описаны мои аксиомы Пеано. Делается это очень просто: строится формула $P(a,b,c)$, которая, по моему личному мнению, будет выражать свойство $c=a^b$ (как строить такие формулы, описано, например, в книге Верещагина и Шеня "Языки и исчисления" в главе Языки первого порядка/Выразимость в арифметике),

А как Вы думаете, эта формула сама по себе разве не является определением операции? И разве нельзя её записать в форме нового утверждения теории (аксиомы)? Например, вот это:
$P(a,b,c) \leftrightarrow a + (S(1) \cdot b) = c$
разве не определяет новую бинарную операцию через операции $+$ и $\cdot$? Вопрос введения для неё нового обозначения (т.е. расширение синтаксиса), по-моему, является чисто формальным.

В данном случае это не чисто формальный вопрос. Если уж мы занимаемся формализацией, то можно поступить двумя способами:
1) создать некоторую фиксированную формальную теорию, и в ней работать;
2) создать формальную теорию, которую при желании мы можем расширять, добавляя новые аксиомы и расширяя синтаксис.

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

epros писал(а):

И, кстати, мне всё-таки любопытно, как именно можно записать формулу $a^b = c$ исключительно через операции сложения, умножения и инкремента?

Это делается громоздко, но делается. В книге Верещагина и Шеня "Языки и исчисления" на страницах 100-104 доказано, как выразить предикат $x=4^y$. В их же книге "Вычислимые функции" доказан более общий результат: предикат $P(x_1,\ldots,x_n)$ арифметичен (выразим первопорядковой формулой в языке с +,*,S,0,=) тогда и только тогда, когда он представим в виде
$(\exists y_1)(\forall y_2)\ldots(\exists y_{2m-1})(\forall y_{2m})Q(x_1,\ldots,x_n,y_1,\ldots,y_{2m})$, где $Q$ - алгоритмически разрешимый предикат (поэтому все алгоритмически разрешимые, в том числе $c=a^b$, сразу сюда попадают). Скачать верещагина и Шеня здесь. Вообще, подобная техника должна быть изложена в любом доказательстве теоремы Гёделя о неполноте (т.е. выходит, что Вы его не читали?).

epros писал(а):

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

Конкретный вопрос: какие базовые свойства у натуральных чисел (строк вертикальных палочек), представимые в виде формул первого порядка с константным символом $0$, функциональными символами $+$, $\cdot$, $S$, предикатным символом $=$ (т.е. в том языке, в котором записаны мои аксиомы Пеано)? С какими заведомо все согласятся?

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

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

[epros]

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

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

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

[маткиб]

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

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

Вопрос номер один. Какие ещё есть легальные способы расширения арифметики (без расширения синтаксиса), кроме добавления мета(n)-доказуемых формул?

Вопрос номер два. Относится ли поиск таких способов, по-Вашему, к математике?

[epros]

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

Вопрос номер один. Какие ещё есть легальные способы расширения арифметики (без расширения синтаксиса), кроме добавления мета(n)-доказуемых формул?

Среди способов расширения арифметики (как и любых других теорий) я вижу:
1. Связанные с расширением синтаксиса, например, определение новых типов объектов или операций. Но Вы это исключили из рассмотрения.
2. Формализация новых недоказуемых, но общеочевидных свойств объектов теории (как я понимаю, с момента первой же более или менее внятной формализации теории этот способ становится неактуальным, поскольку все вполне очевидные свойства очень быстро исчерпываются теоремами и аксиомами теории).
3. Мета(n)-доказательства новых формул. Доказательство в рамках теории, как я понимаю, с Вашей точки зрения не является "расширением" теории, т.е. не вносит в неё ничего нового. Но с моей точки зрения оно, тем не менее, тоже является нетривиальным математическим результатом.

Больше я, вроде бы, ничего не нахожу.

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

Вопрос номер два. Относится ли поиск таких способов, по-Вашему, к математике?

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

[маткиб]

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

Среди способов расширения арифметики (как и любых других теорий) я вижу:

1. Связанные с расширением синтаксиса, например, определение новых типов объектов или операций. Но Вы это исключили из рассмотрения.

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

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

Больше я, вроде бы, ничего не нахожу.

Понятно, т.е. по отношению к арифметике (в синтаксисе 0,+,*,S,=) Вы не признаёте ничего, кроме аксиом Пеано и мета(n)-доказуемых утверждений (потому что "общеочевидных", но не доказуемых в арифметике Пеано Вы не найдёте). А вот я признаю ещё один способ: мета($\omega$)-доказуемость. Он получается, если к аксиомам Пеано с использованием Гёделевской нумерации добавить схему аксиом
$(\forall n)((\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi)$,
где $\mathrm{PA}_n$ - это арифметика Пеано + все мета(n)-доказуемые в ней утверждения. Этот способ не сводится к мета(n)-доказуемости (хотя бы потому, что, например, при $\Phi\equiv(S(0)=0)$ эта аксиома не является мета(n) доказуемой ни при каком n). По-моему, вполне легальный способ. И к получившейся теории можно применить трюк мета(n)-доказуемости, получится мета($\omega+n$) - доказуемость, и т.д. И тут возникает вопрос о формализации легальных способов такого типа.

epros писал(а):

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

Вот я показал вполне легальный способ, о котором Вы сразу не догадались. Говорить, что нет других способов, было бы очень смело (а вдруг Дядя Вася ещё что-нибудь придумает?). Тем более, что такие способы на самом деле есть.

[epros]

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

А вот я признаю ещё один способ: мета($\omega$)-доказуемость. Он получается, если к аксиомам Пеано с использованием Гёделевской нумерации добавить схему аксиом
$(\forall n)((\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi)$,
где $\mathrm{PA}_n$ - это арифметика Пеано + все мета(n)-доказуемые в ней утверждения.

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

Возьмём в качестве примера схему индукции, которая на мета(1)-уровне записывается одной аксиомой:
$(\forall P \in A)(A \vdash P(1) \to ((\forall n \in \mathbb{N})(P(n) \to P(n+1)) \to (\forall n \in \mathbb{N})(P(n))))$

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

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

Говорить, что нет других способов, было бы очень смело (а вдруг Дядя Вася ещё что-нибудь придумает?).

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

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

Тем более, что такие способы на самом деле есть.

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

[маткиб]

epros писал(а):

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

А вот я признаю ещё один способ: мета($\omega$)-доказуемость. Он получается, если к аксиомам Пеано с использованием Гёделевской нумерации добавить схему аксиом
$(\forall n)((\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi)$,
где $\mathrm{PA}_n$ - это арифметика Пеано + все мета(n)-доказуемые в ней утверждения.

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

Возьмём в качестве примера схему индукции, которая на мета(1)-уровне записывается одной аксиомой:
$(\forall P \in A)(A \vdash P(1) \to ((\forall n \in \mathbb{N})(P(n) \to P(n+1)) \to (\forall n \in \mathbb{N})(P(n))))$

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

Тогда я опять перестаю понимать, что Вы подразумеваете под мета-доказуемостью. А то Вы как-то уклончиво в прошлый раз ответили, и я понял неправильно. Я понял так: для теории $T$ мета-доказуемыми называются те и только те предложения, которые доказуемы в теории $T+R_T$, где $R_T$ есть построенная с помощью Гёделевской нумерации (т.е. без расширения синтаксиса) схема аксиом $(T\vdash\Phi)\rightarrow\Phi$.

Если понимать так, то никакой проблемы с формализацией мета($\omega$)-доказуемости нет. Пусть $F(n)$ - вычислимая функция, которая по номеру $n$ алгоритма, перечисляющего все аксиомы теории, вычисляет номер алгоритма, перечисляющего все аксиомы "мета-доказуемости" в этой теории (очевидно, что здесь всё алгоритмично). Тогда для перечисления всех аксиом мета(m)-доказуемостей (для всех m сразу) нужно на первом шаге запустить алгоритм $n$ (перечисляющий аксиомы исходной теории) один такт, потом алгоритмы $n$ и $F(n)$ 2 такта, потом $n$, $F(n)$, $F(F(n))$ 3 такта и т.д., на каждом шаге регистрировать и выдавать строки, которые выдадут соответствующие алгоритмы. А если есть алгоритм, перечисляющий сразу все аксиомы мета(m)-доказуемостей, то с помощью Гёделевской нумерации можно сформулировать аксиому мета($\omega$)-доказуемости.

epros писал(а):

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

Говорить, что нет других способов, было бы очень смело (а вдруг Дядя Вася ещё что-нибудь придумает?).

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

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

Тем более, что такие способы на самом деле есть.

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

Продемонстрирую после того, как разберёмся с мета($\omega$)-доказуемостью.

[epros]

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

Тогда я опять перестаю понимать, что Вы подразумеваете под мета-доказуемостью. А то Вы как-то уклончиво в прошлый раз ответили, и я понял неправильно. Я понял так: для теории $T$ мета-доказуемыми называются те и только те предложения, которые доказуемы в теории $T+R_T$, где $R_T$ есть построенная с помощью Гёделевской нумерации (т.е. без расширения синтаксиса) схема аксиом $(T\vdash\Phi)\rightarrow\Phi$.

Да нет, вроде бы всё правильно.

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

Если понимать так, то никакой проблемы с формализацией мета($\omega$)-доказуемости нет. Пусть $F(n)$ - вычислимая функция, которая по номеру $n$ алгоритма, перечисляющего все аксиомы теории, вычисляет номер алгоритма, перечисляющего все аксиомы "мета-доказуемости" в этой теории (очевидно, что здесь всё алгоритмично). Тогда для перечисления всех аксиом мета(m)-доказуемостей (для всех m сразу) нужно на первом шаге запустить алгоритм $n$ (перечисляющий аксиомы исходной теории) один такт, потом алгоритмы $n$ и $F(n)$ 2 такта, потом $n$, $F(n)$, $F(F(n))$ 3 такта и т.д., на каждом шаге регистрировать и выдавать строки, которые выдадут соответствующие алгоритмы. А если есть алгоритм, перечисляющий сразу все аксиомы мета(m)-доказуемостей, то с помощью Гёделевской нумерации можно сформулировать аксиому мета($\omega$)-доказуемости.

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

[маткиб]

epros писал(а):

Дело в том, что формула, нумерующая аксиомы, вообще говоря не является формулой теории.

Я не понял, что это значит. Мы можем работать с номерами аксиом, а самих аксиом вообще не касаться.

epros писал(а):

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

Есть алгоритм - есть и номер

[epros]

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

epros писал(а):

Дело в том, что формула, нумерующая аксиомы, вообще говоря не является формулой теории.

Я не понял, что это значит. Мы можем работать с номерами аксиом, а самих аксиом вообще не касаться.

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