Основания математики - элементарное рассмотрение

[vek88]

Итак, попытаемся доказать,

vek88 в сообщении #431911 писал(а):

что принцип математической индукции является метатеоремой над классом таких К-систем (программа минимум).

Предположим, что в некоторой К-системе рассматриваемого класса представлено определение некоторого предиката $P(m)$ на множестве натуральных чисел. Предположим, что нам удалось доказать две метатеоремы над этой К-системой.

$$P(0), \forall m (P(m) \rightarrow P(m|)).$$

Примечание. Я как всегда несколько вольно обращаюсь с синтаксисом. Отчасти делаю это умышленно, чтобы за синтаксисом мы не потеряли семантику.

А теперь, внимание, главный трюк нашего доказательства. Пополним нашу теорию этими двумя метатеоремами. Это значит, что мы добавим в К-систему два правила.

$$P(N), \frac{P(Nx)}{P(Nx|)}.$$

ИМХО имеем право пополнять теорию построенными фрагментами метатеории. При условии, что мы не изменяем истинность/ложность утверждений теории/метатеории (ИМХО в данном случае это так).

Сравним эти правила с определением натуральных чисел

$$N, \frac{Nx}{Nx|}.$$

Сразу бросается в глаза некое "подобие" правил для предиката $P$ и правил, определяющих натуральные числа.

Вопрос к общественности - и что же отсюда следует?

[Someone]

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

[robez]

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

[vek88]

robez в сообщении #432209 писал(а):

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

robez

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

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

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

Someone

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

С уважением,
vek88

[Someone]

vek88 в сообщении #432042 писал(а):

Сравним эти правила с определением натуральных чисел

$$N, \frac{Nx}{Nx|}.$$

Я не склонен рассматривать это как определение натуральных чисел, потому что упорядоченное множество $\mathbb N+\mathbb Z$ (сумма порядковых типов: каждый элемент $\mathbb N$ предшествует каждому элементу $\mathbb Z$) является очевидной моделью.

[vek88]

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

vek88 в сообщении #432042 писал(а):

Сравним эти правила с определением натуральных чисел

$$N, \frac{Nx}{Nx|}.$$

Я не склонен рассматривать это как определение натуральных чисел, потому что упорядоченное множество $\mathbb N+\mathbb Z$ (сумма порядковых типов: каждый элемент $\mathbb N$ предшествует каждому элементу $\mathbb Z$) является очевидной моделью.

В каноническом исчислении, содержащем эти два правила, выводимы в точности слова (нулем обозначил пустое слово) $0, |, ||, ..., |||||, ...$ (помеченные меткой $N$). Ничто другое здесь не выводимо! Следовательно, имею право называть эти слова натуральными числами. Во всяком случае Мартин-Леф в Очерках по конструктивыной математике начинает Главу 1 с этого примера натуральных чисел.

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

А то, что при иной интерпретации правил, отличной от канонических исчислений или К-систем, можно рассматривать Вашу модель - я не спорю. Но это уже другая тема, тоже интересная, но вне рамок К-систем.

[Someone]

vek88 в сообщении #432286 писал(а):

В каноническом исчислении, содержащем эти два правила, выводимы в точности слова (нулем обозначил пустое слово) $0, |, ||, ..., |||||, ...$ (помеченные меткой $N$). Ничто другое здесь не выводимо! Следовательно, имею право называть эти слова натуральными числами. Во всяком случае Мартин-Леф в Очерках по конструктивыной математике начинает Главу 1 с этого примера натуральных чисел.

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

С точки зрения теории множеств, в счётной нестандартной модели арифметики натуральный ряд имеет порядковый тип $\mathbb N+\mathbb Q\cdot\mathbb Z$ (имеются в виду операции над порядковыми типами). В любой модели арифметики индуктивное определение $P(0)=|$ и $P(n|)=P(n)|$ определяет функцию $P(n)$ для всех натуральных чисел, а не только для "конечных" (кстати, отличить средствами самой арифметики "конечные" натуральные числа от "бесконечных" невозможно). А ведь есть ещё и несчётные модели. Поэтому какие у Вас основания считать, что в моей модели что-то не выводимо? А если что, возьмите вместо моей модели нестандартный натуральный ряд.

vek88 в сообщении #432286 писал(а):

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

Никакого трансфинитного вывода.

vek88 в сообщении #432286 писал(а):

А то, что при иной интерпретации правил, отличной от канонических исчислений или К-систем, можно рассматривать Вашу модель - я не спорю. Но это уже другая тема, тоже интересная, но вне рамок К-систем.

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

[vek88]

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

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

Так ведь я согласен с Вами в части Вашей модели.

vek88 в сообщении #432286 писал(а):

А то, что при иной интерпретации правил, отличной от канонических исчислений или К-систем, можно рассматривать Вашу модель - я не спорю. Но это уже другая тема, тоже интересная, но вне рамок К-систем.

Разногласия у нас Вами по поводу того, что выводимо/не выводимо в каноническом исчислении или в К-системе.

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

Никакого трансфинитного вывода.

Я не достаточно точно выразился. Да, выводы и в каноническом исчислении и в К-системе - это конечные объекты.

А вот что я имел в виду. В К-системе для установления истинности/ложности утверждений в общем случае необходимо рассмотреть бесконечную совокупность выводов, поскольку необходимо учесть отношение исключения на множестве выводов.

Простейший пример - по определению слово ложно в К-системе iff все его выводы являются Л-выводами. В общем случае это может потребовать рассмотрения бесконечного количества выводов.

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

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

[vek88]

(Оффтоп)

vek88 в сообщении #432359 писал(а):

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

Мдя ... возможность посидеть за компьютером есть, но сил нет. Казалось, что вот сгоняю на машине в Ростов Великий туда и обратно - для бешеной собаки 400 км не крюк - а потом посижу и напишу свои клевые посты. Ан нет - не так все просто. Оказалось, что быть срулем 5 часов в такую погоду очень утомительно - дождь, от грузовиков и фур летит в стекло всякая грязь, темно, ни хрена не видно. Да еще, блин, в Ростове не заметил запрет и заехал на территорию вокзала - что-то, думаю, как-то просторно - только хотел слинять, ментовка полицовка уже тут как тут.

Короче, испортить тему плохими ответами не хочу. Так что свое выступление переношу на утро завтрашего дня поскольку, надеюсь, завтра будет лучше, чем вчера, т.е. сегодня.

Еще короче - пойду тяпну кагорчику.

[vek88]

vek88 в сообщении #432042 писал(а):

А теперь, внимание, главный трюк нашего доказательства. Пополним нашу теорию этими двумя метатеоремами. Это значит, что мы добавим в К-систему два правила.

$$P(N), \frac{P(Nx)}{P(Nx|)}.$$

ИМХО имеем право пополнять теорию построенными фрагментами метатеории. При условии, что мы не изменяем истинность/ложность утверждений теории/метатеории (ИМХО в данном случае это так).

Сравним эти правила с определением натуральных чисел

$$N, \frac{Nx}{Nx|}.$$

Сразу бросается в глаза некое "подобие" правил для предиката $P$ и правил, определяющих натуральные числа.

Вопрос к общественности - и что же отсюда следует?

А отсюда следует простая вещь - утверждение $P(Nx)$ истинно для любого натурального числа.

Доказательство. Пусть $Nx$ натуральное число. Это значит, что существует его И-вывод. Возьмем в этом И-выводе вхождение каждого натурального числа "в скобки" $P()$. Получим И-вывод утверждения $P(Nx)$. Следовательно, $P(Nx)$ истинно. А значит истинно утверждение

$$Nx \rightarrow P(Nx).$$

Что и требовалось доказать.

Примечание. Здесь пока имели обычное каноническое исчисление. Поэтому И-вывод - это просто вывод.

Осталось доказать истинность утверждения

$$\forall x (Nx \rightarrow P(Nx)).$$

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

(Оффтоп)

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

[vek88]

Определение квантора $\forall$ списываю со стр. 123 "Представление в ЭВМ ..." http://narod.ru/disk/2413304001/%D0%9A% ... .djvu.html, упрощая применительно к нашему случаю.

$$\frac{\ominus (Nx \rightarrow P(Nx))}{H},$$

$$\frac{\ominus H}{\forall x (Nx \rightarrow P(Nx))}.$$

Поясним почему выражение

$$\forall x (Nx \rightarrow P(Nx))$$

истинно.

Заметим, что это выражение имеет единственный вывод - применение второго из вышеприведенных правил. Этот вывод имеет в качестве исключений (по определению исключения в К-системе на стр. 122) все выводы константы $H$. Докажем, что все эти исключения являются Л-выводами. А значит сам вывод - И-вывод (и поэтому выражение с квантором истинно).

Все выводы константы $H$ являются применениями первого правила для различных значений $x$. И каждый такой вывод является Л-выводом, поскольку имеет в качестве исключения И-вывод (для натуральных чисел) или вообще не имеет выводов (для "прочих" значений $x$).

Мы доказали истинность принципа математической индукции.

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

[robez]

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

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

Цитата:

В частности, любой алгоритм является К-функцией,
но обратное неверно — К-функция в общем случае непредставима в ви-
де алгоритма.

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

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

[vek88]

robez в сообщении #432209 писал(а):

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

robez

Принято разбираться с вопросами в порядке их поступления. ИМХО мы еще не разобрались с Вашим вопросом о шарлатанстве. А Вы уже задали много-много новых вопросов.

Давайте все-таки будем волноваться поэтапно. Просьба ответить на мой вопрос

vek88 в сообщении #432220 писал(а):

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

-- Вс апр 10, 2011 12:25:59 --

Просмотрел последние сообщения на предмет "хвостов". Нашел высказывания Someone, не относящиеся непосредственно к индукции, но относящиеся к теме. Поэтому обязан их прокомментировать.

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

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

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

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

[vek88]

Другой вопрос - ординалы, следующие за конечными натуральными числами. Здесь даже конструктивисты вводят понятие ординальных чисел (см. того же Мартин-Лефа). Хотя у них это ИМХО не может быть сделано средствами финитной формальной системы, а возможно лишь на метауровне, что лично мне не очень нравится.

А вот в К-системах само определение истинности/ложности слов неявно содержит в себе трансфинитную индукцию. Если это кому-нибудь интресно, готов привести эквивалентное определение И-/Л-выводов в К-системе, хорошо иллюстрирующее "работу трансфинитной индукции".

С учетом сказанного, на уровне семантики я солидарен с Вами в Вашем высказывании

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

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

А расхождения у нас с Вами ИМХО лежат в области синтаксиса, на котором, как все уже заметили, я не склонен зацикливаться.

[vek88]

vek88 в сообщении #433106 писал(а):

Все выводы константы $H$ являются применениями первого правила для различных значений $x$. И каждый такой вывод является Л-выводом, поскольку имеет в качестве исключения И-вывод (для натуральных чисел) или вообще не имеет выводов (для "прочих" значений $x$).

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

Исправление. Необходимо использовать усиленный вариант "нанесения метки", т.е. ограничить область переменной $x$ натуральными числами (см. стр. 122). Или просто скажем, что в первом правиле свободная переменная $x$ имеет тип "натуральное число", т.е. в качестве значений принимает только (конечные) натуральные числа. Тогда вместо неправильного абзаца имеем:

Цитата:

Все выводы константы $H$ являются применениями первого правила для различных значений $x$ (натуральных чисел). И каждый такой вывод является Л-выводом, поскольку имеет в качестве исключения И-вывод (для каждого натурального числа).