2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3, 4, 5, 6, 7, 8  След.
 
 
Сообщение26.12.2008, 13:02 
Заслуженный участник
Аватара пользователя


28/09/06
10413
маткиб писал(а):
Человек, пытаясь узнать свойства объективной реальности, конструирует некоторый мир вымышленный сущностей, который, по его мнению, поможет описать некоторые свойства объективной реальности, а потом уже для этого вымышленного мира придумывает аксиомы и правила вывода.

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

маткиб писал(а):
epros в сообщении #171143 писал(а):
Я не уловил разницы между "сформулировать свойства в виде аксиом" и "выписать набор аксиом произвольно".

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

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

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

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

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

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

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

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

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

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

маткиб писал(а):
epros в сообщении #171143 писал(а):
Правильно ли я понял, что это определение будет звучать примерно так:

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

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

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

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

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

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

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

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

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

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

 Профиль  
                  
 
 
Сообщение26.12.2008, 14:37 


04/10/05
272
ВМиК МГУ
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 писал(а):
Попытаться выполнить формальный вывод этой строки (символов языка теории) из свойств, сформулированых исходя из наших базовых представлений о строках чёрточек.


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

 Профиль  
                  
 
 
Сообщение26.12.2008, 17:39 
Заслуженный участник
Аватара пользователя


28/09/06
10413
маткиб писал(а):
Вот Ваши аксиомы Пеано:
$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$, то получим сроку чёрточек, а значит мы можем записать это в качестве свойства операции умножения натуральных чисел: "Произведение натуральных чисел - натуральное число".

 Профиль  
                  
 
 
Сообщение26.12.2008, 18:27 


04/10/05
272
ВМиК МГУ
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$, предикатным символом $=$ (т.е. в том языке, в котором записаны мои аксиомы Пеано)? С какими заведомо все согласятся?

 Профиль  
                  
 
 
Сообщение27.12.2008, 11:20 
Заслуженный участник
Аватара пользователя


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

Ну да ладно, это вопрос терминологический. Хотите называть $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$, предикатным символом $=$ (т.е. в том языке, в котором записаны мои аксиомы Пеано)? С какими заведомо все согласятся?

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

 Профиль  
                  
 
 
Сообщение27.12.2008, 19:41 


04/10/05
272
ВМиК МГУ
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$, предикатным символом $=$ (т.е. в том языке, в котором записаны мои аксиомы Пеано)? С какими заведомо все согласятся?

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


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

 Профиль  
                  
 
 
Сообщение28.12.2008, 00:00 
Заслуженный участник
Аватара пользователя


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

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

 Профиль  
                  
 
 
Сообщение28.12.2008, 01:19 


04/10/05
272
ВМиК МГУ
epros в сообщении #172158 писал(а):
Не понял Вашей претензии. Я про "принципиальную" неразрешимость высказываний, неразрешимых в этом языке, ничего не говорил. Помнится, я наоборот говорил о том, что можно мета-доказать кое-что, недоказуемое в формальной арифметике, и включение этого в аксиоматику - легальный способ расширения арифметики.


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

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

 Профиль  
                  
 
 
Сообщение29.12.2008, 10:15 
Заслуженный участник
Аватара пользователя


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

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

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

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

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

 Профиль  
                  
 
 
Сообщение29.12.2008, 22:44 


04/10/05
272
ВМиК МГУ
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 писал(а):
Доказательства (включая мета-), с моей точки зрения относятся к математике. А в каком смысле в математике можно как-то по-другому "искать способы" (не внося новых определений) мне не вполне понятно.


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

 Профиль  
                  
 
 
Сообщение30.12.2008, 10:50 
Заслуженный участник
Аватара пользователя


28/09/06
10413
маткиб писал(а):
А вот я признаю ещё один способ: мета($\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$)-уровне мы тоже вынуждены будем принять её без доказательств? Я так подозреваю, что первое мы никогда не докажем и не опровергнем.

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

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

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

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

 Профиль  
                  
 
 
Сообщение30.12.2008, 17:04 


04/10/05
272
ВМиК МГУ
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$)-доказуемостью.

 Профиль  
                  
 
 
Сообщение31.12.2008, 11:03 
Заслуженный участник
Аватара пользователя


28/09/06
10413
маткиб писал(а):
Тогда я опять перестаю понимать, что Вы подразумеваете под мета-доказуемостью. А то Вы как-то уклончиво в прошлый раз ответили, и я понял неправильно. Я понял так: для теории $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$ алгоритма, перечисляющего все аксиомы теории".

 Профиль  
                  
 
 
Сообщение31.12.2008, 13:19 


04/10/05
272
ВМиК МГУ
epros писал(а):
Дело в том, что формула, нумерующая аксиомы, вообще говоря не является формулой теории.


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

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


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

 Профиль  
                  
 
 
Сообщение31.12.2008, 14:01 
Заслуженный участник
Аватара пользователя


28/09/06
10413
маткиб писал(а):
epros писал(а):
Дело в том, что формула, нумерующая аксиомы, вообще говоря не является формулой теории.

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

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 119 ]  На страницу Пред.  1, 2, 3, 4, 5, 6, 7, 8  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group