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

[vek88]

Итак, дана произвольная (финитная) формальная система $E$, например, каноническое исчисление Поста, см. post283784.html#p283784. Рассмотрим множество выводов этой формальной системы.

Предположим на этом множестве выводов задано некоторое бинарное отношение - назовем его отношение исключения и обозначим $<$. Пусть $P, Q$ - выводы. Если $P<Q$, будем говорить, что вывод $P$ - исключение из вывода $Q$.

Примечание. Чтобы не утомлять читателя излишними детмалями, здесь мы намеренно избегаем конкретного варианта определения отношения исключения, рассмотренного выше, см. post284210.html#p284210.

В соответствии с пунктом 1 определения предыдущего поста post472251.html#p472251 индуктивное построение множества И-выводов мы начинаем с множества $T_0$ всех выводов системы $E$, которые не имеют исключений.

Если $T_0$ пусто, значит база индукции пуста, следовательно формальная система $E$ не имеет И-, Л-выводов. И значит в системе $E$ нет истинных или ложных слов (формул, выражений, ...).

Далее предполагаем, что множество $T_0$ не пусто.

[vek88]

В соответствии с пунктом 2 определения теперь мы можем построить множество $F_1$ Л-выводов, которые имеют исключения из $T_0$.

Затем, в соответствии с пунктом 3 мы строим множество $T_1$ И-выводов посредством расширения множества $T_0$ путем добавления выводов, все исключения из которых принадлежат $F_1$.

И т.д. В результате, пока в соответствии с обычной математичекой индукцией, мы построим две монотонно неубывющих (по включению) последовательности множеств:

$$T_0 \subseteq T_1 \subseteq \dots \subseteq T_n \subseteq \dots ,$$

$$F_1 \subseteq F_2 \subseteq \dots \subseteq F_n \subseteq \dots .$$

А теперь мы готовы сделать первый трансфинитный шаг, построив множества

$$T_\omega = \bigcup\limits_{n} T_n,$$

$$F_\omega = \bigcup\limits_{n} F_n.$$

Интуитивно этот шаг вполне очевиден - мы просто нашли "пределы" наших двух последовательностей множеств. А формально все тоже просто, если посмотреть на наше определение.

Действительно, каждый вывод из $F_\omega$ имеет исключением некоторый вывод из $T_\omega$, т.к. он принадлежит некоторому $F_n$.

В свою очередь, для любого вывода из $T_\omega$ все исключения находятся в $F_\omega$. Предлагаю доказать это в качестве упражнения.

[vek88]

А теперь вопрос к общественности - можно ли, применив пункты 2 и 3 определения к множествам $T_\omega, F_\omega,$ построить новые И-, Л-выводы? И, если можно, то как это сделать?

[vek88]

Видимо, сразу ответить на вопросы предыдущего поста сложно? Упрощаю задачу - будем волноваться поэтапно. Задам более простой вопрос.

Можно ли, применив пункт 2 определения к множеству $T_\omega,$ построить новые (т.е. отстутствующие в $F_\omega$) Л-выводы?

[vek88]

Чтобы совсем упростить задачу, позволю себе вообще убрать все ссылки на К-системы, тем самым представив конструкцию из post472251.html#p472251 в чистом виде.

Итак, дано произвольное множество $U,$ на котором задано произвольное бинарное отношение (обозначим $<$). С помощью этого отношения мы выделим два подмножества $T, F$ множества $U$ следующим образом.

Определение. Пусть $x, y \in U$.
1. Если $\neg \exists x < y$, то $y \in T$.
2. Если $x<y$ и $x \in T$, то $y \in F$.
3. Если $(\forall x<y)(x \in F)$, то $y \in T$.

Итак, дана элементарная конструкция: множество с определенным на нем бинарным отношением и простенькое определение. Требуется понять это простенькое определение в терминах трансфинитной индукции.

Вопрос, на который мы ждем ответ, см. в предыдущем посте post472641.html#p472641.

[vek88]

Блин, пункт 2 написал коряво. Короче, надо так:

Определение. Пусть $x, y \in U$.
1. Если $\neg \exists x < y$, то $y \in T$.
2. Если $(\exists x<y)(x \in T)$, то $y \in F$.
3. Если $(\forall x<y)(x \in F)$, то $y \in T$.

Для надежности повторяю совсем просто (отношение $<$ называю меньше, элементы $U$ - это объекты, элементы $T, F$ - это $T,F$-объекты):
1. Если для объекта не существует меньшего объекта, то это $T$-объект.
2. Если у объекта существует меньший $T$-объект, то он является $F$-объектом.
3. Если у объекта все объекты, меньшие чем он, являются $F$-объектами, то это $T$-объект.

[vek88]

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

Можно ли, применив пункт 2 определения к множеству $T_\omega,$ построить новые (т.е. отстутствующие в $F_\omega$) Л-выводы?

Нет, ничего нового мы не получим. Докажем это.

Предположим, что $(\exists x < y)(x \in T_\omega)$. Следовательно, по построению $T_\omega$ для некоторого натурального $n$ $x \in T_n$. Но тогда $y \in F_{n+1}$, а значит $y \in F_\omega$.

Следующий вопрос: можно ли, применив пункт 3 определения к множеству $F_\omega,$ построить новые (т.е. отстутствующие в $T_\omega$) И-выводы ($T$-объекты)?

[vek88]

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

Следующий вопрос: можно ли, применив пункт 3 определения к множеству $F_\omega,$ построить новые (т.е. отстутствующие в $T_\omega$) И-выводы ($T$-объекты)?

Да, в общем случае можно. Докажем это.

Предположим, что для некоторого $y$

$$(\forall x < y)(x \in F_\omega).$$

Возможны два случая:
1. Существует такое натуральное $n$, что $(\forall x<y)(x \in F_n)$.
2. Для всякого натурального $n$ $(\exists x<y)(x \notin F_n)$.

В первом случае мы ничего нового посредством пункта 3 не получим (доказательство аналогично предыдущему посту).

Во втором случае - докажите в качестве упражнения - мы действительно получим новые элементы, в частности, $y \in T$, хотя $y \notin T_\omega$. В результате мы построим большее множество $T$-элементов, которое естественно обозначить через $T_{\omega + 1}$.

ЗЫ. Господа! Проверяйте, е-мое, что это я тут написал.

[vek88]

Ну и дальше все аналогично - отправляясь от $T_{\omega+1}$ строим для всех натуральных $n$ $F_{\omega+n},$ $T_{\omega+n},$ затем предельный переход к $T_{2 \omega},F_{2 \omega},$ и т.д.

Проясняется и интуиция предельных и непредельных порядковых чисел. Например, $\omega, 2 \omega$ - предельные порядковые числа, а натуральные $n$ - непредельные.

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

Теперь понятен и смысл ряда

$$0,1,2, \dots, n, \dots, \omega, \omega +1, \omega+2, \dots, \omega+n, \dots.$$

Стали очевидными также формальное определение и аксиоматика порядковых чисел.

[vek88]

В post284468.html#p284468 мы дали определение И-, Л-выводов посредством некоторых условий. В последних постах мы рассмотрели эквивалентное определение по трансфинитной индукции. А теперь, видимо, будет кстати упомянуть определение в терминах неподвижной точки.

Итак, следуем стр. 115 книги "Представление в ЭВМ ...". Пусть $A$ - некоторое множество выводов. Множество $A^*$ выводов, для которых не существует исключений в $A$, называется сопряженным с $A$.

Если

$$A=A^*^*,$$

множество выводов $A$ называется допустимым.

Пусть $T$ - множество И-выводов некоторой К-системы. Можно показать, что $T$ - минимальное по включению допустимое множество выводов.

[vek88]

Мдя ... давненько не брал я в руки шашек.

Итак, пора вернуться к реальной математичекой практике. А она, зараза, - непротиворечива, невзирая на все потуги целого сонма аксиоматизаторов и прочих формализаторов.

Позволю себе бросить очередной камушек в аксиоматическое болото. Этот камушек связан с абсолютной неприспособленностью аксиоматических теорий к развитию.

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

Но математика в целом, или даже теория множеств - разве они вполне завершены и построены? Дык за каким же хреном мы пытаемся навязать им аксиоматику заранее и на все случаи жизни?

To be continued.

[vek88]

Попробую привести простой пример в традиционных терминах (т.е. пока без К-систем).

Итак, предположим у нас имеется некоторая теория, про которую нам известно следующее:
1. Она содержит аксиому $A \rightarrow B$.
2. Вывод утверждения $B$, если он существет, возможен только через эту импликацию.

Тогда для этой теории справедлива метатеорема

$$A \leftrightarrow B.$$

А теперь дополнительно предположим, что $A = \neg B$. Следовательно, мы имеем метатеорему

$$\neg B \leftrightarrow B.$$

И мы немедленно заключаем, что наша теория противоречива.

ЗЫ. Господа! Проверяйте меня, если это вас не затруднит. Мы с женой этим вечером приготовили и уложили 0,1 кубометра бетона (это около четверти тонны). Поэтому я очень уж сосредоточен на реальных проблемах, не только математических.

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

[vek88]

А теперь предположим, что мы добавили в нашу теорию аксиому $B$. Тогда противоечивая метатеорема

$$\neg B \leftrightarrow B.$$

уже не имеет места.

[vek88]

Хоть пытался обойтись без К-систем, следует добавить, что мое понимание теории все-таки специфическое - в моей теории, как и в К-системах, выводима истинность и ложность утверждений (слов, формул, ...). Короче, ... без К-систем все получается коряво и не очень понятно.

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

[vek88]

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

Формализация, в частности, предполагает формализацию логики рассматриваемых теорий. Вот - математически точный - пример на языке К-систем. Рассмотрим множество теорий (в К-системах), которые содержат правило вывода

$$\frac{A}{B}.$$

Предположим, что в этих теориях отсутствуют другие правила с заключением $B$. Тогда для этого множества теорий имеет место метатеорема

$$A \leftrightarrow B.$$

Предположим дополнительно, что $A = \neg B$. Тогда имеем метатеорему

$$\neg B \leftrightarrow B.$$

Следовательно, наши теории не полны. В частности, металогика этих теорий не является классической (это некое нетривиальное расширение интуиционистской логики - см. выше в теме).

To be continued