Возможности математики без математической индукции

[Lukin]

Lukin в сообщении #560670 писал(а):

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

Обратите внимание на выделенный фрагмент, конечно нужно выбрать что-то одно, добавить аксиому индукции или "анти-индукции".

[LaTeXScience]

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

Конечно же нет! Есть куча утверждений с квантором всеобщности, которые не только не аксиомы, но и вообще неверны.

Вы меня неправильно поняли. Мы не будем ему такие утверждения говорить, которые неверны.

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

Разумеется нет! В непротиворечивость аксиоматики остаётся только верить.

И тут мы опять возвращаемся к теме веры (которая не совместима с наукой).

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

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

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

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

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

Хорошо, почему теорема дедукции верна по-вашему? Чем она лучше своего отрицания? Что, будете сейчас утверждать, что до нее можно додуматься не пользуясь мат. индукцией?

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

Почему бы мне такого не говорить?

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

-- 16.04.2012, 17:29 --

Lukin
Мне кажется, что Вы не понимаете разницу между тем, чтобы выкинуть какую-то аксиому из теории, и тем, чтобы поменять ее на ее же отрицание.

[Lukin]

LaTeXScience в сообщении #560715 писал(а):

LukinМне кажется, что Вы не понимаете разницу между тем, чтобы выкинуть какую-то аксиому из теории, и тем, чтобы поменять ее на ее же отрицание.

Разница в том, что в первом случае формула индукции будет недоказуемым утверждением, как и ее отрицание, а во втором - ложным, а ее отрицание истинным.
А Вы понимаете эту разницу ?

[epros]

LaTeXScience в сообщении #560715 писал(а):

Вы меня неправильно поняли. Мы не будем ему такие утверждения говорить, которые неверны.

Что значит «неверны»? Вы что же, претендуете на знание какой-то абсолютной истины? Речь была об аксиомах с квантором всеобщности. В каком смысле могут быть «неверны» аксиомы? Например, верна или нет аксиома $\forall n \exists m ~ m = n + 1$? Никакой индукции для её доказательства никто не использовал, её просто приняли за аксиому.

LaTeXScience в сообщении #560715 писал(а):

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

Разумеется нет! В непротиворечивость аксиоматики остаётся только верить.

И тут мы опять возвращаемся к теме веры (которая не совместима с наукой).

Непротиворечивость арифметики не доказана. Арифметика не имеет отношения к науке?

LaTeXScience в сообщении #560715 писал(а):

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

Да причём тут мета-аксиомы? Мета-теоретически мы можем думать о теории что угодно: Что она выражает абсолютную истину или, наоборот, что теория ничего осмысленного не описывает, а была разработана только для развлечения. Это никак не отразится на выводах в рамках самой теории.

LaTeXScience в сообщении #560715 писал(а):

Хорошо, почему теорема дедукции верна по-вашему? Чем она лучше своего отрицания? Что, будете сейчас утверждать, что до нее можно додуматься не пользуясь мат. индукцией?

Далась Вам эта теорема дедукции... Представьте себе, сейчас я буду утверждать, что для любой конечно аксиоматизируемой теории мета-теорему дедукции можно доказать без мат. индукции. Индукция нужна только для доказательства обобщающего утверждения: «Для любой теории первого порядка ...»

LaTeXScience в сообщении #560715 писал(а):

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

Почему бы мне такого не говорить?

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

Я же сказал, что никакой такой уверенности у меня нет. Наоборот, я уверен, что и компьютер с распознаванием достаточно длинных формул не справится (вычислительных мощностей не хватит), и «дикарь» с некоторыми формулами не справится, не смотря на исчерпывающее знание синтаксиса (интеллектуальных возможностей не хватит). Тем не менее, я предпочитаю рассматривать такие ситуации как выходящие за рамки наших интересов: Ну, не понадобится нам никогда распознавать НАСТОЛЬКО сложные формулы.

[LaTeXScience]

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

Что значит «неверны»?

Вы первый произнесли это слово, Вы и объясняйте.

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

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

Доказана товарищем Генценом.

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

Арифметика не имеет отношения к науке?

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

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

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

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

[epros]

LaTeXScience в сообщении #560802 писал(а):

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

Что значит «неверны»?

Вы первый произнесли это слово, Вы и объясняйте.

Что объяснять? Вы намекнули, что какие-то аксиомы, которые мы должны сообщить «дикарю», неверны. Вы о чём?

LaTeXScience в сообщении #560802 писал(а):

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

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

Доказана товарищем Генценом.

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

LaTeXScience в сообщении #560802 писал(а):

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

Арифметика не имеет отношения к науке?

А мы в нее не верим.

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

Арифметика МОЖЕТ оказаться противоречивой, но это не мешает нам ей пользоваться. С какой стати я должен доказывать непротиворечивость упрощенного варианта арифметики - арифметики Робинсона, прежде, чем начать ей пользоваться?

LaTeXScience в сообщении #560802 писал(а):

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

Конечное количество аксиом всё меняет. Оно позволяет записать теорему дедукции одной формулой, в которую войдут все аксиомы.

[LaTeXScience]

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

Вы намекнули, что какие-то аксиомы, которые мы должны сообщить «дикарю», неверны.

Ничего я не намекал.

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

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

Я не понимаю, почему Вы вообще связываете понятие непротиворечивости теории с понятием веры в нее?

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

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

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

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

Оно позволяет записать теорему дедукции одной формулой, в которую войдут все аксиомы.

А теоремы?

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

(Оффтоп)

Имхо, ультрафинитизм интереснее, чем ваш обычный финитизм/конструктивизм.

[epros]

LaTeXScience в сообщении #560854 писал(а):

Я не понимаю, почему Вы вообще связываете понятие непротиворечивости теории с понятием веры в нее?

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

LaTeXScience в сообщении #560854 писал(а):

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

Если арифметика противоречива, то в ней можно вывести вообще всё, включая $0 = 1$. Но пока ничего такого не выведено, так что выводится отнюдь не всё, а только кое-что. Так что можно спокойно пользоваться.

LaTeXScience в сообщении #560854 писал(а):

А теоремы?

Что теоремы? В формуле, которой записывается мета-теорема дедукции, перечисляются только аксиомы:

$\forall \varphi, \psi ~ (a_1 \wedge a_2 \wedge \dots \wedge a_n \wedge \varphi \vdash \psi) \to (a_1 \wedge a_2 \wedge \dots \wedge a_n \vdash \varphi \to \psi)$

Здесь $\varphi$ и $\psi$ - переменные мета-теории, принимающие в качестве значений высказывания языка теории.

[Lukin]

LaTeXScience в сообщении #560854 писал(а):

Имхо, ультрафинитизм интереснее, чем ваш обычный финитизм/конструктивизм.

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

(Оффтоп)

Погуглите, "Альтернативная теория множеств: Новый взгляд на бесконечность"
Автор: Вопенка П. Издательство: Новосибирск: Институт математики Год: 2004
или "Математика в альтернативной теории множеств" Вопенка П.

[epros]

Кстати, мне сейчас в голову пришёл замечательный пример случая, когда теорема дедукции не работает. Есть ещё вот такой вариант арифметики: Примитивно-рекурсивная арифметика Сколема (PRA). Это - теория без кванторов, но при этом - не являющаяся конечно-аксиоматизируемой. В ней есть мат. индукция, реализуемая отдельным правилом вывода: $(PRA \vdash \varphi(0) \wedge [\varphi(n) \to \varphi(n+1)]) \to (PRA \vdash \varphi(n))$. С использованием мат. индукции можно доказать всюду определённость любой примитивно-рекурсивной функции. Правда отсутствие кванторов в языке создаёт трудности для записи утверждения о всюду определённости функции $f$: $\forall n \exists m ~ m = f(n)$, однако эту проблему решил Клини, введя свой T-предикат, с помощью которого такие формулы можно записывать без кванторов. Однако есть такие обще-рекурсивные функции, всюду определённость которых в PRA недоказуема (при том, что определение самих этих функций можно записать в языке PRA). Простейшим примером такой функции является функция Аккермана. Посмотрев на определение функции Аккермана в статье википедии, можно убедиться, что она определяется тремя дополнительными аксиомами:

$A(0,n) = n+1$
$A(m+1,0) = A(m,1)$
$A(m+1,n+1) = A(m, A(m+1,n))$

где $A$ - функциональный символ, а $m$ и $n$ - символы переменных. Как видите, всё в пределах синтаксиса языка PRA. Допустим, что с помощью T-предиката Клини мы записали в бескванторной форме утверждение о всюду определённости функции Аккермана: $\varphi_A(m,n) \equiv \exists k ~ k = A(m,n)$. Что мешает нам в рамках PRA, использовав мат. индукцию, доказать его?

Из определения функции Аккермана прямо следует следующее:

1) $\varphi_A(0,n)$
2) $\varphi_A(m,1) \to \varphi_A(m+1,0)$
3) $[\forall k ~ \varphi_A(m,k)] \to [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$

Последнее утверждение не обошлось без квантора, от которого можно избавиться, если подставить вместо символа переменной $k$ символ произвольной функции $K(m)$ - эта операция называется "скулемизация". Тогда оно запишется так:

3') $\neg \varphi_A(m,K(m)) \vee [\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)]$

(это читается как: "Для любого $m$ или существует такое $K$, что $\varphi_A(m,K)$ ложно, или для любого $n$ из $\varphi_A(m+1,n)$ следует $\varphi_A(m+1,n+1)$").

Обращаем внимание, что (2) совместно с (3') приводят к:

4') $\neg \varphi_A(m,K(m)) \vee [\varphi_A(m+1,0) \wedge \{\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)\}]$

или с квантором это бы записалось так:

4) $[\forall k ~ \varphi_A(m,k)] \to [\varphi_A(m+1,0) \wedge \{\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)\}]$

Здесь в правой части импликации стоит условие мат. индукции по $n$. Казалось бы, что ещё нужно? Вроде бы, осталось подставить вместо выражения в правой части импликации $\varphi_A(m+1,n)$, а потом, использовав (1) и применив индукцию по $m$, получить общее утверждение: $\varphi_A(m,n)$? Ан нет. Доказанного утверждения $\varphi_A(m+1,0) \wedge \{\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)\}$ у нас нет, оно стоИт внутри дизъюнкции, поэтому непосредственно применить соответствующее правило вывода мы не можем.

Вот тут и выходит на сцену теорема дедукции: Предположив $\varphi_A(m,K(m))$, мы можем из (4') вывести $\varphi_A(m+1,0) \wedge \{\varphi_A(m+1,n) \to \varphi_A(m+1,n+1)\}$, а отсюда, использовав мат. индукцию, вывести $\varphi_A(m+1,n)$. Далее, применив теорему дедукции, мы можем считать доказанным $\neg \varphi_A(m,K(m)) \vee \varphi_A(m+1,n)$ - эквивалент импликации, записанный в бескванторной форме. Далее для доказательства общего утверждения остаётся только применить индукцию по $m$.

Как я понимаю, проблема заключается именно в том, что мета-теорема дедукции к PRA неприменима: Ниоткуда не следует, что из $PRA \wedge \varphi \vdash \psi$ мы имеем право вывести $PRA \vdash \neg \varphi \vee \psi$ - при определении PRA никаких подобных правил Сколем не оговорил. Опять же, доказать это без мат. индукции невозможно, ибо PRA - бесконечно аксиоматизируемая теория, так что просто перечислить все аксиомы, которые нужно подставить вместо "PRA" в формулировку мета-теоремы дедукции, мы не можем.

Но может быть, конечно, я чего-то просто не допонял ...

[докер]

(Оффтоп)

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

LaTeXScience в сообщении #560802 писал(а):

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

Я поняла, что арифметика предоставляет возможность подсчитать бесконечное количество яблок, и если бесконечного количества яблок нет, то это проблема не математики, а садоводов. Сколько яблок предоставите, столько и сосчитаем. Почему опять яблоки интерпретируем как числа?