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

[AlexDem]

Мне всё видится следующим образом. Возьмём две грамматики $A$ и $B$ над одним и тем же алфавитом, причём $B \subset A$, то есть все слова, порождаемые $B$, порождаются и $A$. На множестве всех слов $A$ зададим функцию отрицания $\neg$, такую, что $a = \neg\neg a$. Все слова $A$ назовём множеством всех синтаксически корректных формул, все слова $B$ - множеством выводимых формул, а правила грамматики $B$ - правилами вывода нашей формальной системы. Тогда, для полной формальной системы должно соблюдаться правило: $\forall x \in A (x \in B \vee \neg x \in B)$, а для непротиворечивой: $\forall x \in B \not \exists y \in B (x = \neg y)$. В книге К.М. Подниекса приводится теорема о категоричности: Всякая модель аксиом Пеано изоморфна стандартной модели.

Легко видеть, что грамматика $B$ задаёт алгебраическую структуру на подмножестве формул $A$ - если из $x, y$ по правилам $B$ выводимо $z$, можно написать $xy = z$. Насколько я понимаю, теорема Гёделя говорит, что невозможно построение такой алгебры, которая бы соответствовала стандартной модели и одновременно соблюдалось бы свойство: $A \setminus B = \neg B$.

В случае нефинитной формализации мы могли бы ткнуть пальцем в каждую из формул и назначить её истинной или ложной по нашему желанию аксиоматически. Но в случае конечного набора правил мы этого сделать не можем, поэтому обеспечить условие $A \setminus B = \neg B$ не так просто. К-системы позволяют нам перейти к дополнениям, используя в правилах исключения, вместо самих переменных, но число правил всё же остаётся конечным и нет гарантии того, что они обеспечат условие $A \setminus B = \neg B$.

Впрочем, если я понимаю всё неверно - поправляйте...

[vek88]

AlexDem в сообщении #431213 писал(а):

Мне всё видится следующим образом. Возьмём две грамматики $A$ и $B$ над одним и тем же алфавитом, причём $B \subset A$, то есть все слова, порождаемые $B$, порождаются и $A$. На множестве всех слов $A$ зададим функцию отрицания $\neg$, такую, что $a = \neg\neg a$. Все слова $A$ назовём множеством всех синтаксически корректных формул, все слова $B$ - множеством выводимых формул, а правила грамматики $B$ - правилами вывода нашей формальной системы. Тогда, для полной формальной системы должно соблюдаться правило: $\forall x \in A (x \in B \vee \neg x \in B)$, а для непротиворечивой: $\forall x \in B \not \exists y \in B (x = \neg y)$.

Буду отвечать поэтапно и постепенно - по мере осмысления Ваших вопросов. Для начала выбрал первый абзац из поста post431213.html#p431213.

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

Далее, естественно вводить отрицание в К-системе так, чтобы это отрицание было согласовано с определениями истинности/ложности в К-системе. Т.е. отрицание истинного (ложного) слова должно быть ложным (соответственно, истинным). Такое отрицание вводится правилом

$$\frac{\ominus x}{\neg x}.$$

Примечание. Разумеется, вольному - воля. Т.е. мы можем вводить в К-системе и другие "отрицания". Но это уже другая песня и в данной теме это ИМХО не интересно.

Если отрицание в К-системе определено указанным правилом (и только этим правилом), то К-система непротиворечива в том смысле, что не могут быть в К-системе истинными какое-либо слово и его отрицание.

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

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

To be continued

[AlexDem]

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

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

С этим я, пожалуй, согласен - насколько помню, символ $\neg$ не используется нигде в правилах вывода, кроме правила

$$\frac{\ominus x}{\neg x}$$

. Поэтому в моих обозначениях Вы сперва получаете грамматику $B$, а потом с помощью $\neg B$ дополняете её до некоторого $A' \subseteq A$.

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

Если отрицание в К-системе определено указанным правилом (и только этим правилом), то К-система непротиворечива в том смысле, что не могут быть в К-системе истинными какое-либо слово и его отрицание.

А оба ложными они могут быть? Например, если не существует никакого вывода ни у одного из них? Если могут, то это решает вопрос пополнения $A'$ до $A$, но тогда возникает проблема $A \setminus B \ne \neg B$ - то есть ложных формул больше, чем истинных. Если они оба ложными быть не могут, то я пока не вижу, откуда это следует...

[robez]

И индукция в К-системах отсутствует, судя по всему.

[vek88]

AlexDem в сообщении #431286 писал(а):

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

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

С этим я, пожалуй, согласен - насколько помню, символ $\neg$ не используется нигде в правилах вывода, кроме правила

$$\frac{\ominus x}{\neg x}$$

. Поэтому в моих обозначениях Вы сперва получаете грамматику $B$, а потом с помощью $\neg B$ дополняете её до некоторого $A' \subseteq A$.

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

Если отрицание в К-системе определено указанным правилом (и только этим правилом), то К-система непротиворечива в том смысле, что не могут быть в К-системе истинными какое-либо слово и его отрицание.

А оба ложными они могут быть? Например, если не существует никакого вывода ни у одного из них? Если могут, то это решает вопрос пополнения $A'$ до $A$, но тогда возникает проблема $A \setminus B \ne \neg B$ - то есть ложных формул больше, чем истинных. Если они оба ложными быть не могут, то я пока не вижу, откуда это следует...

Пусть $a$ - слово в некоторой К-системе. Рассмотрим его отрицание $\neg a$. Оно (отрицание слова $a$) - по нашему определению отрицания - имеет единственный вывод

$$\frac{\ominus a}{\neg a}.$$

Теперь давайте попытаемся сделать так, чтобы оба $a, \neg a$ были ложны.

Чтобы слово $\neg a$ было ложно, необходимо и достаточно (по определению ложности в К-системе), чтобы все выводы этого слова были Л-выводами. А оно имеет ровно один вывод, следовательно, этот вывод является Л-выводом.

Теперь по определению И-, Л-выводов заключаем, что существует И-вывод, являющийся исключением из этого вывода - по определению исключения на множестве выводов это непременно И-вывод слова $a$. Следовательно, слово $a$ имеет И-вывод, а значит оно истинно.

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

Да и как же может быть иначе. Ведь определение истинности/ложности слов в К-системе симметрично в следующем смысле. Пусть дана произвольная К-система. Пометим ее схемы меткой $E$ и добавим правило

$$\frac{\ominus Ex}{x}.$$

Мы построили К-систему, в которой слово истинно (ложно) тогда и только тогда, когда оно ложно (соответственно, истинно) в исходной К-системе.

Соответственно, если мы признаем, что слово и его отрицание не могут быть одновременно истинными в К-системе, то значит они не могут быть и одновременно ложными в К-системе.

ЗЫ. Остались еще вопросы без ответа - продолжу как только у меня появится возможность (сейчас я в цейтноте).

[AlexDem]

AlexDem в сообщении #431286 писал(а):

насколько помню, символ $\neg$ не используется нигде в правилах вывода, кроме правила ...

Проврался я тут, используется. А то все формулы вида $...(a\wedge\neg b)$ не выводились бы. Отвечу попозже.

[vek88]

AlexDem в сообщении #431436 писал(а):

AlexDem в сообщении #431286 писал(а):

насколько помню, символ $\neg$ не используется нигде в правилах вывода, кроме правила ...

Проврался я тут, используется. А то все формулы вида $...(a\wedge\neg b)$ не выводились бы. Отвечу попозже.

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

Итак, конечно, в других правилах знак отрицания используется, но только в посылках. Для того мы его и ввели (=определили), чтобы далее, наряду с кванторами и другими логическими связками, использовать в посылках правил для записи тех или иных логических формул.

Продолжаю отвечать на ранее заданные вопросы.

AlexDem в сообщении #431213 писал(а):

Легко видеть, что грамматика $B$ задаёт алгебраическую структуру на подмножестве формул $A$ - если из $x, y$ по правилам $B$ выводимо $z$, можно написать $xy = z$. Насколько я понимаю, теорема Гёделя говорит, что невозможно построение такой алгебры, которая бы соответствовала стандартной модели и одновременно соблюдалось бы свойство: $A \setminus B = \neg B$.

В случае нефинитной формализации мы могли бы ткнуть пальцем в каждую из формул и назначить её истинной или ложной по нашему желанию аксиоматически. Но в случае конечного набора правил мы этого сделать не можем, поэтому обеспечить условие $A \setminus B = \neg B$ не так просто. К-системы позволяют нам перейти к дополнениям, используя в правилах исключения, вместо самих переменных, но число правил всё же остаётся конечным и нет гарантии того, что они обеспечат условие $A \setminus B = \neg B$.

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

А теперь о самом главном в Вашем вопросе - об обеспечении условия $A \setminus B = \neg B$. ИМХО здесь все зависит от места Ваших множеств $A, B$ в иерархии множеств. Если мы говорим об арифметике, то значит мы говорим об арифметических (по Геделю) множествах, т.е. о множествах, которые строятся из рекурсивно перечислимых множеств посредством применения логических связок и кванторов.

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

Последние два абзаца я написал очень кратко и, возможно, не очень аккуратно. Поэтому за деталями (и полезными ссылками) отсылаю к разделу 8.4 книги "Представление в ЭВМ ...". См. http://narod.ru/disk/2413304001/%D0%9A% ... .djvu.html.

Если же мы осмелимся представить в полной К-системе более "серьезные" множества, например, произвольные К-множества ..., то мы вляпаемся снова в историю, аналогичную попыткам представления арифметики в финитных формальных системах. Снова мы получим аналог теорем Геделя со всеми вытекающими последствиями.

Похоже, я ответил на вопросы AlexDem.

Через некоторое время надеюсь дозреть для ответа на вопрос robez о математической индукции в К-системах. Вопрос очень хороший и не такой простой как может показаться на первый взгляд.

[AlexDem]

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

Пусть $a$ - слово в некоторой К-системе. Рассмотрим его отрицание $\neg a$. Оно (отрицание слова $a$) - по нашему определению отрицания - имеет единственный вывод

$$\frac{\ominus a}{\neg a}.$$

А как быть, если слово не настолько просто? Пусть это будет формула $a \vee b$, её отрицание - $\neg a \wedge \neg b$, почему какая-то из них должна иметь единственный вывод?

[vek88]

AlexDem в сообщении #431610 писал(а):

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

Пусть $a$ - слово в некоторой К-системе. Рассмотрим его отрицание $\neg a$. Оно (отрицание слова $a$) - по нашему определению отрицания - имеет единственный вывод

$$\frac{\ominus a}{\neg a}.$$

А как быть, если слово не настолько просто? Пусть это будет формула $a \vee b$, её отрицание - $\neg a \wedge \neg b$, почему какая-то из них должна иметь единственный вывод?

Итак, пусть это будет формула $a \vee b$. Тогда ИМХО её отрицание - это формула $\neg (a \vee b)$. И она имеет единственный вывод - т.е. все как я говорил раньше.

Вы же отрицание исходной формулы заменили на $\neg a \wedge \neg b$. Это Вы сделали на основе метатеоремы

$$\neg (a \vee b) \leftrightarrow \neg a \wedge \neg b.$$

Имеете право - но это "другая песня", которая не может изменить полноты и непротиворечивости полной К-системы. Ведь упомянутая метатеорема - это логический закон, справедливый в любой полной К-системе. А в классе полных К-систем работает классическая логика. См. выше в данной теме post293513.html#p293513. Детали см. в статье, указанной в post294016.html#p294016.

Впрочем, для проверки давайте рассмотрим вывод формулы $\neg a \wedge \neg b$. Предположим она истинна. Значит есть ее И-вывод - в корне этого вывода применение правила, определяющего связку $ \wedge $. Значит истинны слова $\neg a, \neg b$. Ну а уж эти слова выводимы только через правило, вводящее отрицание, т.е. $a, b$ ложны. Следовательно, $a \vee b$ ложна (т.к. обе посылки ложны, следовательно все выводы данной формулы являются Л-выводами).

Предположим теперь, что $\neg a \wedge \neg b$ ложна. Тогда все ее выводы - Л-выводы. В корне правило, вводящее $\wedge $. Значит все выводы хотя бы одной из посылок этого правила - Л-выводы. Значит хотя бы одна из посылок ложна. Пусть ложна $\neg a$. Значит $a$ истинно. Следовательно, истинна $a \vee b$.

ЗЫ. Мы здесь не уточняли определение правильно построенной формулы, поэтому пользуемся интуитивной нотацией. Надеюсь, это не приведет к недоразумениям.

[AlexDem]

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

$a, b$ ложны. Следовательно, $a \vee b$ ложна (т.к. обе посылки ложны, следовательно все выводы данной формулы являются Л-выводами).

Так ведь в противоречивой системе это не мешает существованию вывода формулы $a \vee b$ из какой-нибудь истинной формулы. Тогда обе формулы $a \vee b$ и $\neg a \wedge \neg b$ становятся истинными, а правило:

$$\frac{\ominus a}{\neg a}$$

- перестаёт играть роль.

==
Буду писать реже, времени тоже очень мало.

[vek88]

AlexDem в сообщении #431658 писал(а):

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

$a, b$ ложны. Следовательно, $a \vee b$ ложна (т.к. обе посылки ложны, следовательно все выводы данной формулы являются Л-выводами).

Так ведь в противоречивой системе это не мешает существованию вывода формулы $a \vee b$ из какой-нибудь истинной формулы. Тогда обе формулы $a \vee b$ и $\neg a \wedge \neg b$ становятся истинными, а правило:

$$\frac{\ominus a}{\neg a}$$

- перестаёт играть роль.

==
Буду писать реже, времени тоже очень мало.

Что-то я потерял нить наших рассуждений. Придется отступить назад и сказать другими словами.

Итак, даны два множества: множество $A$ геделевских номеров всех правильно построенных замкнутых (т.е. все свободные переменные "обложены" кванторами) формул арифметики и множество $B$ геделевских номеров истинных формул из множества $A$.

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

Множество $A$ - это РП множество. А относительно $B$ известно, что: (см. раздел 8.4 "представление в ЭВМ ...")

Цитата:

Множество истинных замкнутых формул арифметики (т.е. множество $B$) является полным неарифметическим К-множеством.

Следовательно, в полной К-системе, представляющей множество $B$ геделевские номера всех ложных формул из $A$ ложны.

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

[vek88]

Блин, отрубили - не дали доредактировать. Так что продолжу в новом посте.

Итак, множество $B$ - полное К-множество. Следовательно, $A \setminus B$ - тоже полное К-множество. Таким образом, каждая формула из $A$ попадает (посредством своего геделевского номера) в одно и только одно из множеств $B$ или $A \setminus B$ в зависимости от своей истинности/ложности (в первое - истинные и только они, во второе ложные и только они).

Следовательно, наша формализация арифметики в К-системах полна и непротиворечива.

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

Обращаю также внимание на промелькнувшую выше интересную "мелочь" - множество всех истинных формул арифметики - это не арифметическое множество. Т.е. арифметическая истина не арифметична (=невыразима средствами арифметики). Это теорема Тарского для арифметических множеств.

Кстати, теорема Тарского имеет место и для полных К-систем. И звучит так: множество геделевских номеров полных К-систем в заданном алфавите не является полным К-множеством. Т.е. в К-системах "полная истина неполна". См. теорему 8.9 в "Представление в ЭВМ ...".

-- Ср апр 06, 2011 10:20:28 --

Наконец я добрался до вопроса robez.

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

И индукция в К-системах отсутствует, судя по всему.

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

Тем не менее вопрос о математической индукции мне нравится, поскольку он напомнил мне, что следует более подробно поговорить о метатеориях над К-системами. При этом все зависит от класса К-систем, для которых мы хотим строить метатеории. Например, если мы строим метатеорию, справедливую для любой К-системы, то мы получим логику Крипке-Клини, построенную выше. Если мы ограничиваем себя полными К-системами, то мы получим классическую логику. См. выше в данной теме post293513.html#p293513. Детали см. в статье, указанной в post294016.html#p294016.

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

Конкретно, с учетом вопроса robez, предлагаю далее рассмоатреть класс полных К-систем, содержащих стандартное определение множества натуральных чисел.

[vek88]

Соответственно, возникает вопрос - что еще, кроме классической логики, содержит метатеория этого класса полных К-систем?

ИМХО, как минимум, должна появиться метатеорема, утверждающая справедливость принципа математической индукции.

Что думает общественность по этому поводу?

ЗЫ. Я ведь агитирую за К-системы, поскольку считаю их формальной системой, подходящей для представления нашего наивного (=интуитивного) математического мышления. Следовательно, я просто обязан показать (в меру сил), как основы нашего наивного математического мышления представляются в полных К-системах и в метатеориях над ними. Исходя из этого и предлагаю рассмотреть математическую индукцию.

[vek88]

Итак, рассматриваем класс всех полных К-систем, содержащих определение натуральных чисел. Пусть, например, это определение в каждой такой К-системе задано в виде

Знак $|$
Вспомогательный знак $N$
Переменная $x$
Правила $N$ $\frac{Nx}{Nx|}$
Здесь выводимы в точности слова $N,N|,N||, … $.

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

Разумеется, любая тавтология классической логики является таким "законом", поскольку любая тавтология является "законом" и более общего класса - класса всех полных К-систем.

Но, поскольку мы сузили класс всех полных К-систем, по всей видимости, должны появиться и какие-то дополнительные "законы"? Которых не могло быть в классе всех полных К-систем.

Какие это законы?

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

Пример. Если $m$ - натуральное чило, то $m||$ тоже натуральное число. В формальной записи этот "закон" выглядит так

$$\forall m (Nm \rightarrow Nm||).$$

Доказательство. Пусть $m$ натуральное число. Следовательно, имеется И-вывод слова $Nm$. Достроим этот И-вывод двумя очевидными применениями правила вывода $\frac{Nx}{Nx|}$. Получим И-вывод слова $Nm||$. Следовательно, $m||$ - натуральное число. Метатеорема доказана.

Конечно, это плюшевый закон, мало кому интересный. Но мы, по крайней мере, получили подсказку как найти все "законы".

[vek88]

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

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

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

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