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

[Lukin]

Предлагаю усилить предложение epros "обходится в теории без аксиомы индукции", шагнув чуть дальше, "примем в теории обратное утверждение": если из $P(n)$ следует $P(n+1)$, то существует такое $n$, для которого $\neg P(n)$.
Вот и теория без математической индукции, которую можно создать в метатеории с аналогичной аксиомой.
А то создается впечатление, что все спорят, потому что под математической индукцией "понимают одно и тоже".

Относительно распознавания корректности формул. Возможна ведь самоприменимая теория. Будем считать, что моделью теории является язык, на котором она сформулирована, а синтаксически корректными лишь те формулы, которые являются объектами ее модели. Такая теория эффективно справится с распознаванием синтаксической корректности собственных формул, но, конечно, не с распознаванием их истинности.

[epros]

Someone в сообщении #560234 писал(а):

Причём тут множества?

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

Someone в сообщении #560234 писал(а):

Что такое "первое"? И как его "стереть"?

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

[LaTeXScience]

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

Нет, непонятно.

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

Ещё раз повторю: Индукция нужна для ОБОБЩАЮЩИХ выводов типа: «Любая формула является словом». Зачем при распознавании слова (или формулы) $0 = 1$ нам нужны обобщающие выводы?

Хорошо, т.е. Вы исходите из того, что мы дикарю не произнесем ни одного высказывания вида $\forall x \in N :\,P(x)$, где $N$ -- cчетное множество, $P$ -- предикат. Но, к сожалению, Вы уже произнесли ему такое высказывание:

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

Слово состоит из букв.

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

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

А с чего Вы взяли, что результатом работы данного НАМ всегда будет либо ``да'', либо ``нет'' для каждого переданного ему слова, а может он для какого-то слова ответит что-то третье? Уж не посмели ли Вы неосознанно использовать математическую индукцию (ай-я-яй)?

[Someone]

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

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

Строка - это не множество символов. А "состоит из" - слишком неопределённо, чтобы понять, что такое строка символов. Даже если все символы вполне точно определены.

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

Ну, должны же быть какие-то базовые понятия. Если «дикарь» не понимает «состоит из», то может быть «первое» (или «крайнее») и «стереть» (или «закрыть») поймёт.

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

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

[LaTeXScience]

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

Я утверждаю, что без мат. индукции можно обойтись. Она нужна только для обобщающих выводов типа: «Любая формула может быть распознана». А вот этого как раз нам и не нужно: Мы можем для любой конкретной формулы доказать, что она может быть распознана, применив N раз правило modus ponens.

Вы здесь произнесли утверждение вида $\forall x \in N : P(x)$. Ай-я-ай.

[Lukin]

Предвижу, что скоро понятие математической индукции размоется так, что ею станет любая индукция, обычная транзитивность, объединение или modus ponens.
Нужно все-таки различать, какое из понятий уже, и конкретней.
$\forall x \in \matthbb{N} : (P(x))$. Кто сказал, что $x \in \mathbb {N}$ ?
$x$ - это обозначение элемента, совокупность которых, даже не множество, и, вообще, без какого-либо порядка. $x$ - это элемент неперечислимой беспорядочной кучи, для которой аксиома нуля, следования или минимального элемента и некоторые из ZF не имеют места быть. Индукция, как правило логического вывода остается, а математической индукции нет.
Начиналась тема с вопроса о древних, как они обходились без математической индукции ? А так и обходились - была куча разовых правил и все. Обобщить и упорядочить они их не могли, т.к. математической индукции не было, да и числа были другими с плохими свойствами (как Римские, например), но это не мешало им жить, строить пирамиды и т.д.

[epros]

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

Хорошо, т.е. Вы исходите из того, что мы дикарю не произнесем ни одного высказывания вида $\forall x \in N :\,P(x)$, где $N$ -- cчетное множество, $P$ -- предикат.

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

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

Но, к сожалению, Вы уже произнесли ему такое высказывание:

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

Слово состоит из букв.

А обобщённые утверждения (типа этого), которые закладываются в качестве аксиомы, допустимы. Мы ведь не требуем от «дикаря», чтобы он их доказывал по индукции.

Кстати, в арифметике Робинсона есть такая аксиома:
$\forall n \exists m ~ m = n + 1$,
которая является утверждением с квантором всеобщности. Однако почему-то никто не считает, что эта аксиома имеет отношение к индукции.

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

А с чего Вы взяли, что результатом работы данного НАМ всегда будет либо ``да'', либо ``нет'' для каждого переданного ему слова, а может он для какого-то слова ответит что-то третье? Уж не посмели ли Вы неосознанно использовать математическую индукцию (ай-я-яй)?

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

-- Вс апр 15, 2012 22:56:16 --

Someone в сообщении #560356 писал(а):

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

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

[Someone]

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

А эта железяка - и есть «формализация», которая на не слишком длинных строках будет нормально работать.

Фи!

[LaTeXScience]

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

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

Точнее, Вы исходите из того, что мы заставляем его каждое наше утверждение вида $\forall x \in N : P(x)$ принять за аксиому.

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

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

И то утверждение, что Ваша аксиоматика непротиворечива, Вы тоже добавляете в качестве аксиомы?

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

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

Ни с чего я это не взял.

Тогда не говорите: ``распознающего слово в заданном алфавите''.

[epros]

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

Точнее, Вы исходите из того, что мы заставляем его каждое наше утверждение вида $\forall x \in N : P(x)$ принять за аксиому.

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

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

И то утверждение, что Ваша аксиоматика непротиворечива, Вы тоже добавляете в качестве аксиомы?

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

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

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

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

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

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

Ни с чего я это не взял.

Тогда не говорите: ``распознающего слово в заданном алфавите''.

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

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

[epros]

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

Предлагаю усилить предложение epros "обходится в теории без аксиомы индукции", шагнув чуть дальше, "примем в теории обратное утверждение": если из $P(n)$ следует $P(n+1)$, то существует такое $n$, для которого $\neg P(n)$.

Не пойдёть. Если в качестве $P(n)$ взять $\exists m ~ m = n + 1$, то получим противоречие между одной из аксиом арифметики и этой Вашей аксиомой "анти-индукции".

[Lukin]

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

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

Предлагаю усилить предложение epros "обходится в теории без аксиомы индукции", шагнув чуть дальше, "примем в теории обратное утверждение": если из $P(n)$ следует $P(n+1)$, то существует такое $n$, для которого $\neg P(n)$.

Не пойдёть. Если в качестве $P(n)$ взять $\exists m ~ m = n + 1$, то получим противоречие между одной из аксиом арифметики и этой Вашей аксиомой "анти-индукции".

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

Ales в сообщении #529801 писал(а):

Аксиома Архимеда не предусматривает вывод по индукции: для любых двух отрезков существует число такое, что первый отрезок увеличенный именно во столько раз превзойдет по длине второй. Это просто универсальное правило, вывод по индукции не применяется.

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

-- 16.04.2012, 10:47 --

А вообще -то, и в арифметике Робинсона пройдет, существование такого элемента не означает, что он непосредственно "следует за...".

[epros]

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

В арифметике Робинсона не пройдёть, я имел в виду аксиоматику Пеано.

Это псевдо-осмысленный текст?

[Lukin]

(Оффтоп)

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

Это псевдо-осмысленный текст?

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

[epros]

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

Просто не ознакомился до предыдущего ответа с арифметикой Робинсона, вот и подумал, что они эквивалентны.

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