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

[AlexDem]

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

[vek88]

Тема 2. Нефинитное обобщение канонических систем

Насколько мне известно, у математиков особого базара по поводу «злокозненного» логического отрицания не было. А вот где действительно лет 25 назад случился большой базар – это логическое программирование в связи с языком Пролог (Programming in Logic). Вникать в подробности мы не будем, но кратко пояснить суть проблемы отрицания, видимо, необходимо.

Предположим, я определил некоторое множество $A$ натуральных чисел. Разумеется, всем очевидно, что для любого натурального числа $n$ выражение $\neg (n \in A)$ истинно тогда и только тогда, когда $n \notin A$.

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

Следуя книге «Представление в ЭВМ неформальных процедур», рассмотрим обобщение канонической системы, позволяющее представлять логическое отрицание. Указанное обобщение называется К-система. Теперь правило вывода – это фигура вида

$$\frac {t_1…t_n \verb

где $t,t_1, t_2,…,t_{n+m}$ – термы, а $\ominus$ – особый знак. Этот знак используется в служебных целях и только для маркировки посылок.

Понятие вывода теперь определяется следующим образом:
1. Применение аксиомы – вывод этого применения.
2. Если $P_1,…,P_n$ – выводы соответственно слов $a_1,…,a_n$ и

$$\frac {a_1…a_n \verb

– применение некоторого правила, то

$$\frac {P_1…P_n \verb

– вывод слова $a$.

Пусть дана некоторая К-система. Рассмотрим множество всех выводов в этой К-системе. Посылки, помеченные знаком $\ominus$, позволяют ввести полезное для целей представления отрицания бинарноое отношение на множестве выводов К-системы.

Определение. Пусть $P, Q$ - выводы в некоторой К-системе. Если вывод $Q$ содержит выражение $\ominus a$, где $a$ - слово, и $P$ - вывод слова $a$, то вывод $P$ - исключение из вывода $Q$. В этом случае используем запись $P<Q$.

Далее с помощью отношения исключения мы выделим два вида выводов: И-выводы и Л-выводы. Первые будут использоваться для вывода истинных слов, вторые для вывода ложных слов.

[vek88]

Истинность и ложность в К-системе

Пусть задана К-система. На множестве ее выводов определим два подмножества выводов, называемых И-выводами и Л-выводами, как наименьшие (по включению) подмножества, удовлетворяющие условиям:

1. Вывод, все исключения из которого Л-выводы, является И-выводом.
2. Вывод, имеющий исключением И-вывод, является Л-выводом.

Обратим внимание, что вывод, не имеющий исключений, подпадает под пункт 1.

Слово истинно в К-системе, если существует его И-вывод.

Множество слов в данном алфавите, истинных в некоторой К-системе, называется К-множеством.

К-множество К-разрешимо, если его дополнение до множества всех слов в вданном алфавите является К-множеством.

Слово ложно в К-системе, если все его выводы являются Л-выводами (или оно вообще не имеет вывода).

К-система, все слова которой разрешимы - истинны или ложны - называется полной. К-множество полно, если оно представимо в полной К-системе.

Свойства замкнутости К-множеств

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

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

Доказательство теоремы элементарно и вполне конструктивно (сводится к выписыванию нескольких простых правил вывода). Детали доказательства см. в уже упомянутой книге "Представление в ЭВМ неформальных процедур". Здесь мы ограничимся доказательством пункта 2 Теоремы в части дополнения. Пусть дано полное К-множество $E$ в некотором алфавите (представленное в полной К-системе). Пометим его правила меткой $E$ и добавим правило

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

Построенная К-система определяет (полное) дополнение $\overline E$ К-множества $E$ до множества слов в том же алфавите.

[vek88]

Выразительные возможности полных К-систем

Итак, теперь мы умеем представлять в К-системах $\vee, \wedge, \neg, \exists, \forall$. Поскольку мы хотим работать в классической логике, естественно ограничить себя классом полных К-систем. Подчеркнем, что приняв такое ограничение, мы исключили из рассмотрения неполные К-системы, например, К-систему, содержащую два правила

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

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

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

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

$$A \leftrightarrow \neg A.$$

Однако нас эта теорема не пугает – она просто сигнализирует нам о неполноте построенной К-системы. Конкретно о том, что слово $A$ - неразрешимо (ни истинно, ни ложно).

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

При конструктивном подходе мы ограничиваемся построениями в полных К-системах.

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

[vek88]

Конструктивизм

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

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

Теорема 1. Всякое множество счетно.

Из этой теоремы следует, что все бесконечные множества в конструктивизме равномощны друг другу.

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

Пусть $E$ и $F$ – множества. Множеством подмножеств множества $E$ естественно назвать любое отношение $R \subset F \times E$. С учетом свойств замкнутости класса множеств отсюда заключаем, любое счетное объединение и пересечение множеств является множеством. А поскольку в конструктивизме все множества счетные, класс множеств замкнут относительно произвольных объединений и пересечений.

Следующая теорема служит обоснованием аксиомы выбора в конструктивизме.

Теорема 2. Для любого бинарного отношения $R$ существует функция $f \subset R$ с той же областью определения.

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

Теорема 3. Множество геделевских номеров полных К-систем в заданном алфавите не является полным К-множеством.

Доказательство этой теоремы производится по стандартной диагональной схеме. При этом используются геделевская нумерация и универсальная К-система.

Впрочем невозможность говорить о множестве всех подмножеств множества $N$ можно доказать и элементарными средствами посредством стандартного диагонального построения: предположим задана последовательность подмножеств $N_i \subset N$. Строим новое множество $M$ по правилу

$$\frac {i \notin N_i}{i \in M}.$$

Предположение о том, что для некоторого $i_0$ $M=N_{i_0}$ приводит к противоречию.

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

Подчеркнем, что конструктивист не может интерпретировать эту теорему как утверждение о существовании несчетных множеств – их в конструктивизме нет, и не может быть.

[vek88]

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

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

Уважаемый Владимир Рогожин! Как только я написал эту фразу, сразу вспомнил приведенную Вами цитату:

Владимир Рогожин в сообщении #279239 писал(а):

1. "...истина должна быть нарисована и предъявлена "неограниченному кругу" зрителей." (А.Зенкин "Научная контрреволюция в математике" http://science.ng.ru/magnum/2000-07-19/5_mathem.html)

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

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

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

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

[vek88]

Конструктивизм - продолжение

На первый взгляд, конструктивизм слишком ограничивает математику. Однако вспомним, что даже в более ограниченном варианте конструктивизма – в РП-конструктивизме – все не так уж плохо, в частности, удается построить конструктивный вариант математического анализа.

А в рассматриваемом здесь варианте конструктивизма все гораздо лучше. Даже справедлива аксиома выбора. А главное в том, что мы можем формулировать определения практически традиционным способом, используя отрицание, логические связки и кванторы классической логики. В частности, мы можем определить действительное число как фундаментальную последовательность рациональных чисел. Напомним, что под такой последовательностью мы понимаем полную К-функцию, отображающую множество натуральных чисел в множество рациональных чисел, и такую, что для всякого натурального $n$ существует натуральное $m$, такое, что разность любых членов последовательности с номерами больше $m$ по модулю меньше $\frac{1}{n}$.

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

Упражнение. Докажите непрерывность конструктивных действительных чисел.

Домашнее задание. Напишите дипломную работу или кандидатскую диссертацию на тему «Конструктивный математический анализ на основе полных К-систем».

Далее мы переходим к самому интересному – к классической (интуитивной) теории множеств. Поскольку вопрос серьезный, мы начнем новую Тему 3.

[vek88]

Тема 3. Классическая теория множеств в полных К-системах

Итак, мы подошли к самому интересному – к представлению классической теории множеств в полных К-системах. Напомним, что мы уже имеем к настоящему времени.

Фактически, мы имеем все … за маленьким исключением. Мы можем рассуждать так, как мы это обычно делаем в математике. Для этого только следует заботиться о представлении всех наших объектов (множеств, отношений, функций, предикатов и т.д.) в полных К-системах. Если мы не играем в парадоксы, сделать это достаточно просто в силу свойств замкнутости класса полных К-систем относительно логических связок, отрицания и кванторов классической логики. Но даже и парадоксы нам не страшны при таком способе рассуждений, поскольку появление парадоксов автоматически означает, что где-то мы ошиблись и вышли за пределы полных К-систем.

А маленькое исключение? Да, к сожалению, в конструктивизме невозможно работать с несчетными множествами. Но давайте подумаем, как можно это исправить так, чтобы и конструктивизм по возможности сохранить, и несчетные множества позволить.

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

Но может ли математика полагаться на предположения о внешнем мире!? Вопрос вполне законный и, на первый взгляд, очень серьезный. Тем не менее, ответ тривиальный – мы никаких предположений о свойствах самих числовых множеств вовсе и не делаем – эти множества по-прежнему определены конструктивно и никаких новых свойств мы им не приписываем. Мы только лишь сказали, что все эти числовые множества мы не можем одновременно представить в полной К-системе, но предположили, что они все одновременно представлены в некоторой внешней полной системе. А чтобы общаться с этими числовыми множествами, мы можем использовать гипотетические «внешние устройства» – или оракулы.

Как в компьютерах внешние устройства, оракулы могут быть устроены по-разному. Здесь в качестве наиболее конструктивного примера мы рассмотрим оракул, определяющий по любому натуральному числу на входе, является ли оно геделевским номером подмножества множества натуральных чисел или нет. Естественно обозначить этот оракул предикатом $n \in 2^N$ (числовое множество с геделевским номером $n$ является элементом множества $2^N$). Далее предполагается, что для любого натурального $n$ этот (внешний!) предикат полон – либо истинен, либо ложен.

Теорема. Множество $2^N$ несчетно.

Напомним, что счетность у нас понимается конструктивно, как существование полной К-биекции

$$f: N \rightarrow 2^N.$$

Напомним также, что в силу теоремы Тарского множество геделевских номеров полных К-систем в заданном алфавите не является полным К-множеством.

[vek88]

Оракулы

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

Пусть дана К-система $E$, некоторые правила которой содержат в посылках метку $P$, причем символ $P$ - вспомогательный знак, не используемый в заключениях правил $E$. Если добавить к $E$ конечный набор правил, помеченных меткой $P$, то скажем, что задана внутренняя (= средствами К-системы) интерпретация предиката $P$.

Если же для определения истинности или ложности посылок с меткой $P$ допустить использование оракула, то будем говорить о внешней интерпретации предиката $P$, или о К-системе с оракулом для $P$. Содержательно, оракулам соответствуют органы чувств, геометрическая интуиция и т.д. Внутренняя структура оракула несущественна – например, можно считать, что он содержит аксиомы $Pa$ для всех истинных слов с меткой $P$ и только для них.

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

Расширяется и смысл переменных и кванторов. Так в выражении $\forall \xi A(\xi)$ при конструктивном подходе переменная $\xi$ принимала в качестве значений любые слова в фиксированном алфавите – имя, по существу, отождествлялось со значением. Теперь, при классическом подходе, переменная $\xi$ именует произвольный объект внешнего мира: отрезок прямой, функцию, и т.д. Таким образом, квантор всеобщности $\forall \xi$ следует понимать как "пусть $\xi$ обозначает произвольный объект внешнего мира" или "для любого объекта внешнего мира с именем $\xi$".

Квантор существования в классике утверждает существование некоторого объекта внешнего мира, вообще говоря, без явного указания как его найти. Существование, таким образом, понимается весьма широко и не обязательно конструктивно. Напомним, что в конструктивизме существование всегда доказывается построением соответствующей К-системы.

Внося подобную «внешнюю» семантику в понимание множеств мы фактически высказываем гипотезы об устройстве внешнего мира. Рассмотрим какими средствами мы располагаем для проверки этих гипотез. Разумеется, физический эксперимент не подходит, т.к. все реальные оракулы: глаза, уши, измерительные приборы и т.д. – с учетом их неидеальности обладают ограниченной пропускной способностью. Следовательно, невозможно экспериментально проверить даже простейшие факты, связанные с понятием бесконечности, например, что сумма любых двух действительных чисел есть действительное число.

Остается единственная возможность – мысленный эксперимент. Это предполагает внутреннюю интерпретацию внешних оракулов. Если при этом удастся вывести противоречие, то значит гипотезы о внешнем мире были неправильными. А если эти гипотезы не приводят к противоречию? Что это доказывает? Это доказывает, что мы имеем право принять или не принять эти гипотезы о внешнем мире в качестве аксиом.

Каковы же наши «мысленные» средства? Очевидно, что они ограничены конструктивизмом! Отсюда следует простой способ построения аксиом классической теории на основе конструктивных теорем, гарантирующий непротиворечивость.

Теорема 1. Всякая теорема конструктивной теории множеств является утверждением классической теории множеств, неопровержимым конструктивно.

В качестве примера подобного утверждения можно привести аксиому выбора.

Теорема 2. Классическая аксиома выбора конструктивно неопровержима.

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

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

Упражнение. Приведите примеры аксиом теории множеств, доказуемых конструктивно.

[vek88]

Примеры

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

Пример 1. Рассмотрим множества натуральных чисел (далее – числовые множества). Множество всех таких множеств определяется следующим образом.

Знак типа «множество всех числовых множеств» $2^N$
Внешняя переменная типа «числовое множество» $X$
Переменная типа «натуральное число» $n$
Правило

$$\frac {\forall n (n \in X \rightarrow n \in N)}{X \in 2^N}.$$

Разумеется, мы здесь предполагаем, что множество натуральных чисел уже определено, т.е. имеется полная К-система, в которой определен предикат $n \in N$.

Упражнение 1. Докажите, предикат $X \in 2^N$, введенный этим определением, является полным в любой внутренней интерпретации внешнего предиката (=оракула) $ n \in X $.

Упражнение 1a. Докажите, что для введенного определения имеет место теорема

$$\forall n (n \in X \rightarrow n \in N) \leftrightarrow X \in 2^N.$$

Итак, множество $2^N$ определено корректно. Рассмотрим теперь пример некорректного определения множества.

Пример 2. Предположим, что мы сформулировали следующее определение.

Знак типа «множество Рассела» $R$
Внешняя переменная типа «множество» $X$
Правило

$$\frac {X \notin X }{X \in R}.$$

Упражнение 2. Докажите, что предикат $X \in R$, введенный этим определением, не является полным в любой внутренней интерпретации внешнего предиката (=оракула) $ X \notin X $.

Упражнение 2a. Докажите, что для определения Примера 2 имеет место теорема

$$X \in X \leftrightarrow X \notin X.$$

Таким образом, определение Примера 2 не может быть признано корректным в нашей идеологии полноты определений.

-- Ср фев 03, 2010 12:48:21 --

P.S. Уважаемые коллеги! Цель, продекларированная

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

достигнута. Засим завершаю мой затянувшийся монолог.

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

[vek88]

Ну вот, даже никто не заметил ошибку. В Упражнении 2а в теореме вместо $X$ везде должно быть $R$.

[vek88]

В дополнение к книге "Представление в ЭВМ неформальных процедур" рекомендую статью о связи К-множеств и $\Pi_1^1$-множеств: Скворцов Д.П. О связи К-систем (формальных систем с исключениями) и аналитической иерархии числовых множеств // Семиотика и информатика. Вып. 29. - 1989. - с. 145-163. Замечу, что статья очень специальная и доступна, видимо, только профессионалам.

В этой статье, в частности, доказано, что К-множество полно тогда и только тогда, когда оно К-разрешимо.

[vek88]

Напомню, что:
- в первой половине этой темы (далее - Часть 1) мы говорили о возможностях мышления человека на примере оснований математики;
- а во второй (далее - Часть 2) была сделана попытка изложить некий вариант оснований математики.

Теперь настал момент расставить некоторые акценты. Итак в первой части большой сыр-бор разгорелся по вопросу определения понятий через самих себя. Теперь, после изложения Части 2 мы все понимаем, что этот сыр-бор возник в результате термнологического разнобоя. На самом деле, например, оба определения множества $N$ - мое и общепринятое (как множество слов, выводимых в определенном каноническом исчислении) - не противоречат друг другу. Хотя лично мне это общеприятое определение и не нравится, поскольку оно предполагает наличие лишего правила

$$\frac {Nx}{x \in N}.$$

Посмотрите как меня поправляли, когда я пытался сказать, что определяю $N$ в канонической системе, например,
-- Пт фев 05, 2010 14:36:52 --

Xaositect в сообщении #277463 писал(а):

Очень хорошо.
Определение такое: Множество натуральных чисел - это множество всех строк $x$ таких, что формула $Nx$ выводима в формальной системе с аксиомой(которую Вы забыли) $\vdash N$ и правилом вывода $Nx\vdash Nx|$.

В правой части определения множества натуральных чисел нет.

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

Пример 1. Посмотрите как в Части 2 строятся формальные теории. Мы добавляем в теорию любые (1) правила в качестве определений, при единственном условии полноты определений. Причем это условие, если речь идет об обычной математической практике, легко проверяемо! И этот стиль математических рассуждений близок к обычным интуитивным математическим рассуждениям. В том числе, в динамике! Т.е. в процессе развития математических конструкций. Именно поэтому в Части 2 удалось реабилитировать наивную теорию множеств.

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

И эти люди запрещают нам ковыряться в носу!!!???

Пример 2. А теперь покажем, что мы предоставляем математикам больше воли, чем люди, загоняющие математику в аксиоматический тупик. Это выражается в том, что мы разрешаем и циклические определения, в которых понятие определяется само через себя, но, разумеется, при условии полноты. И у нас все просто. Парадокс Рассела? Пожалуйста - определяйте множество Рассела - что, Данила - мастер, не выходит камень самоцветный? - О-О-О-й не выходит - ну что ж, вы получили, что хотели.

Или вот другой пример циклического определения:

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

Заметьте, что здесь справедливы две теоремы

$$A \leftrightarrow \neg B,$$

$$B \leftrightarrow \neg A.$$

При традиционном подходе противоречия нет, но возможны две интерпретации. И что же здесь делать? Тогда как в полных К-системах вопрос даже не возникает - данное определение не является полным! Докажите это в качестве упражнения.

Но мы не запрещаем циклические определения, например, мы можем "исправить" это определение, добавив аксиому $A$. Цикличность осталась, а К-система стала полной. Докажите это в качестве упражнения.

И все? И все!

[vek88]

Заседание продолжается, господа присяжные заседатели!

Позволю себе сделать маленькое разъяснение по поводу "уровня конструктивности" конструктивного и классического подходов в полных К-системах. Это разъяснение навеяно рассуждениями в теме topic17718.html

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

А вот множество всех действительных чисел (далее - ДЧ) или множество всех подмножеств множества $N$ - эти множества мы не можем охватить мысленным взором целиком. Можем охватывать только их счетные (счетные в конструктивном смысле) подмножества. Это низкий уровень конструктивизма.

Конкретно это выражается в том, что мы не знаем что там в множестве всех ДЧ на самом деле!!! Но если мы не можем опровергнуть в полных К-системах гипотезы/предположения о свойствах всех ДЧ, мы предполагаем, что эти гипотезы/предположения о свойствах всех ДЧ истинны.

А это в чистом виде применение закона двойного отрицания!

Например, определив ДЧ как фундаментальную последовательность рациональных чисел и определив обычным образом сложение ДЧ, мы бодро доказываем (мета) теорему (переменные $X, Y$ типа действительные числа)

$$\forall X \forall Y (X+Y=Y+X).$$

Но при этом мы не могли конструктивно доказать это - мы доказали только, что мы не можем опровергнуть это!

Не так ли, господа присяжные?

[vek88]

Вот еще камень в огород сторонников аксиоматических теорий множеств. Чтобы пояснить идею камня, начну с интуитивной арифметики.

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

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

Так вот, с моей точки зрения, интуитивная теория множеств жива и будет жить вечно. Более того, для нее аналогично арифметике любая финитная формализация неполна (надеюсь, это всем очевидно). Следовательно, любая ее финитная аксиоматика "обедняет" теорию множеств. А народу это не нужно.

Руки прочь от наивной теории множеств. Да здравствует наивная теория множеств!

И как был прав Гильберт, сказав: "Никто не изгонит нас из рая, созданного Кантором!"

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

Кто-нибудь еще против наивной теории множеств? Тогда мы идем к вам.