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

[man]

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

1. Вам это очевидно. И мне тоже. Об этом я и писал в post370720.html#p370720. А вот Лукомор считает, что подобное условие/правило вводить нельзя, а противоречия никакого нет (если я правильно его понял). Вот мы с ним и пытаемся договориться.

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

Может быть их нетривиальность в том, что это невозможно.
Для доказательства противоречивости достаточно единственного примера. Его тоже нет.

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

2. А вот разрешением парадокса путем добавления второго брадобрея я не занимался. На самом деле я пытался на примерах рассмотреть разные случаи "нехороших" построений.

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

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

Итак, увеличим количество брадобреев в деревне - для начала пусть их два: А и В. Далее все просто:
1. Брадобрей А бреет всех тех и только тех, кто не бреется у брадобрея В.
2. Брадобрей В бреет всех тех и только тех, кто не бреется у брадобрея А.

Задаемся вопросом бреет ли брадобрей А самого себя? Отношение $x$ бреется у $y$ обозначим $x \in y$. Тогда наш вопрос формулируется в виде: истинно или ложно $A \in A$?
В К-системе это представляется в виде

$$\frac{x \notin B}{x \in A}, \frac{x \notin A}{x \in B}.$$

А чтобы уменьшить объем писанины и сделать наглядной структуру исключений, опустим "обозначения" для $\notin$ и $\neg$:

$$\frac{\ominus(x \in B)}{x \in A}, \frac{\ominus(x \in A)}{x \in B}.$$

Понятно, что для всех остальных жителей деревни каким-то образом определено, у какого брадобрея они бреются. Вопрос в том, у кого бреются сами брадобреи. Разберемся с А. Мы видим, что для слов $A \in A, A \in B$ имеются выводы

$$P=\frac{\ominus(A \in B)}{A \in A}, Q=\frac{\ominus(A \in A)}{A \in B}.$$

По определению исключений на множестве выводов $P<Q, Q<P$. С учетом этого выводы $P,Q$ не являются ни И-выводами, ни Л-выводами. Следовательно, слова $A \in A, A \in B$ неразрешимы.

Или противоречивы ?

А, так:
1. Брадобрей А бреет всех тех и только тех, кто не бреется у брадобрея В.
2. Брадобрей В бреет всех тех и только тех, кто не бреется у брадобрея А.
$\frac{x \in B}{x \notin A}, \frac{x \in A}{x \notin B}$
Cлова $A \in A, A \in B$ разрешимы ?

-- Пн ноя 08, 2010 23:03:50 --

Лукомор в сообщении #372523 писал(а):

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

И я хочу сделать так, чтобы $B_1 \in B_1 \leftrightarrow B_1 \notin B_1.$ Почему незя так хотеть?

Потому что $B_1 \in B_1 \or B_1 \notin B_1.$ всегда истинно...

Только по отдельности. Истинность одного исключает истинность другого.
А... заметил надо писать $\lor$.

[vek88]

Лукомор в сообщении #372523 писал(а):

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

И я хочу сделать так, чтобы $B_1 \in B_1 \leftrightarrow B_1 \notin B_1.$ Почему незя так хотеть?

Потому что $B_1 \in B_1 \bigcup B_1 \notin B_1.$ всегда истинно...

Мы с Вам пошли на второй или третий круг. Разногласие у нас с Вами в следующем:
- Вы считаете, что правило запрещено, если оно приводит к противоречию;
- я считаю, что все правила разрешены, но бывают "нехорошие" правила.
При этом мы с Вами сходимся в том, что бывают "нехорошие" правила. Вы их не разрешаете, а я разрешаю. Так что в главном мы с Вами согласны, а расхождение связано с "чувством свободы". Кстати я уже писал, что Вы имеете право так делать:

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

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

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

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

А я предпочитаю ИМХО более удобный путь:
1. Разрешать любые правила.
2. Но при этом в К-системе проверять полноту.
3. Если К-система полна, то значит правила "хорошие" и можно с ними работать в традиционной классической логике.
4. А если К-система не полна, то правила "плохие". Но мы можем работать с ними, понимая при этом, что классическая логика уже не применима. См. post291626.html#p291626
5. А можем и запретить такие правила и продолжать работать в полной К-системе на основе классической логики (это будет Ваш подход).

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

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

-- Вт ноя 09, 2010 11:13:55 --

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

Или противоречивы ?

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

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

А, так:
1. Брадобрей А бреет всех тех и только тех, кто не бреется у брадобрея В.
2. Брадобрей В бреет всех тех и только тех, кто не бреется у брадобрея А.

$$\frac{x \in A} {x \notin B}, \frac{x \in B}{x \notin A}.$$

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

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

И переопределять ее не следует (имеем право, но это изменит традиционную семантику отрицания). Вы своими правилами фактически пытаетесь переопределить отрицание.

[man]

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

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

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

И переопределять ее не следует (имеем право, но это изменит традиционную семантику отрицания). Вы своими правилами фактически пытаетесь переопределить отрицание.

Речь идет о переводе великого и могучего на язык формул.
Почему Вы рассматриваете

$$\frac{\ominus(x \in B)}{x \in A},\frac{\ominus(x \in A)}{x \in B}$$

и не рассматриваете

$$\frac{x \in A}{\ominus(x \in B)}, \frac{x \in B}{\ominus(x \in A)}$$

[Лукомор]

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

Только по отдельности. Истинность одного исключает истинность другого.
А... заметил надо писать $\lor$.

Уже исправил!
"Потому что $B_1 \in B_1 \lor B_1 \notin B_1$ всегда истинно..."
Так должно быть...

[vek88]

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

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

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

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

И переопределять ее не следует (имеем право, но это изменит традиционную семантику отрицания). Вы своими правилами фактически пытаетесь переопределить отрицание.

Речь идет о переводе великого и могучего на язык формул.
Почему Вы рассматриваете

$$\frac{\ominus(x \in B)}{x \in A},\frac{\ominus(x \in A)}{x \in B}$$

и не рассматриваете

$$\frac{x \in A}{\ominus(x \in B)}, \frac{x \in B}{\ominus(x \in A)}$$

Вывод в К-системе определен в post284210.html#p284210. В К-системе $\ominus$ – особый знак. Этот знак используется в служебных целях и только для маркировки посылок.

Определение вывода в К-системах обобщает традиционное понятие вывода в финитных формальных системах, см. post283784.html#p283784.

[man]

Пока не понял, как Вы отличаете неполноту от противоречивости.
В $\frac {\ominus x}{\neg x}$ что такое $x$ ?

[vek88]

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

Пока не понял, как Вы отличаете неполноту от противоречивости.
В $\frac {\ominus x}{\neg x}$ что такое $x$ ?

Подробности о К-системах приведены ранее в этой теме (см. несколько постов, начиная с post284210.html#p284210). Еще более подробно см. книгу "Представление в ЭВМ неформальных процедур" (есть в Интернете).

Здесь ограничусь пояснением сути на примере.

Итак, дана К-система в алфавите

$$A,B$$

с переменной

$$x$$

с аксиомой

$$A$$

и правилами вывода

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

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

Пояснение. Слова из букв $A$ выводятся из аксиомы с применением первого правила вывода (все как в обычных финитных формальных системах). Соответствующие выводы не имеют исключений (т.к. не содержат знака $\ominus$) - поэтому они И-выводы. А значит выводимые с их помощью слова истинны.

Все остальные слова не имеют выводов, следовательно, они ложны.

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

ЗЫ. Писал наспех - проверяйте.

[man]

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

ЗЫ. Писал наспех - проверяйте.

Все нормально. Теперь стало яснее. Заморочки с отрицанием. Определим отрицание так, чтобы противоречие нельзя было сформулировать.
С формулой

$$\frac{\ominus(x \in B)}{x \in A},\frac{\ominus(x \in A)}{x \in B}$$

и выводами, теперь понятно.
Намеки на ZFC обрели смысл. Определение множества через отрицание (например, пустого) является нехорошим. Так ?

[vek88]

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

Определение множества через отрицание (например, пустого) является нехорошим. Так ?

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

А вот в посылках правил (над чертой) можно использовать любые формулы, построенные из логических связок (включая отрицание) и кванторов $\exists, \forall$.

В частности, если говорить об определении пустого множества, то определять его можно по-разному - и в этом К-система не указ. Например, я могу сказать, что при определении отношения $\in$ в К-системе я зарезервировал служебный знак $\Lambda$, причем этот знак не используется в правой части определения отношения $\in$. Тогда автоматически любое слово вида $x \in \Lambda$ будет ложным (т.к. для него не существует вывода), следовательно, слово $x \notin \Lambda$ будет истинным.

А могу сказать, что множество $x$ пустое, если $\forall y (y \notin x)$, т.е.:

$$\frac{ \forall y (y \notin x)}{x \verb

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

ЗЫ. А как в Latex обозначается обычный знак пустого множества? Че то я не нашел.

[vek88]

Нашел! Стандартное обозначение пустого множества задается командой \varnothing - получаем символ $\varnothing$. Знак $\emptyset$ все-таки у нас как-то не очень принят.

[man]

См. стр. 84 монографии, последний абзац.
Каноническое исчисление $E$ задано пустым словом (алфавитом).
Рассматривается пересечение $E$ с любым одноэлементным алфавитом канонического исчисления $F$. Формула $\{a\} \bigcup E = \varnofing$ объявляется неразрешимой, иначе $a \in E$ разрешимо для любого $a$, что противоречит теореме о алгоритмической неразрешимости эквивалентности множеств, определяемых рекурсивно каноническими исчислениями $E,F$.


Это к вопросу о финитности. В финитных канонических (конструктивных) системах тождество пустых множеств тривиально доказуемо. В нефинитных оно неразрешимо (отрицание не финитно переопределено).

Стр.135 в следствии вводится символ $R$ не являющийся частью алфавита, это эквивалентно предикату второго порядка в обычном исчислении предикатов.
Неразрешимость $R \in R$ преподносится, как нечто необычное. Это естественно, т.к. согласно теореме Геделя теория с предикатами второго порядка или неполна или противоречива.
В качестве примера, использования символа, не содержащегося в алфавите, смотрите:
АЛФАВИТ: $A,B$
ПЕРЕМЕННЫЕ $x,y$
ВСПОМОГАТЕЛЬНЫЕ ЗНАКИ: N,M

ПРАВИЛА ВЫВОДА:
$\frac{x}{Ax}$
$\frac {Ax}{x \in N}$

$\frac{x}{Bx}$
$\frac {Bx}{x \in M}$

$\frac{N \in M}{x \in x}$
$\frac {M \in N}{x \in x}$

$N \in M \lor M\in N$ неразрешимо.

[vek88]

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

См. стр. 84 монографии, последний абзац.
Каноническое исчисление $E$ задано пустым словом (алфавитом).
Рассматривается пересечение $E$ с любым одноэлементным алфавитом канонического исчисления $F$. Формула $\{a\} \bigcup E = \varnofing$ объявляется неразрешимой, иначе $a \in E$ разрешимо для любого $a$, что противоречит теореме о алгоритмической неразрешимости эквивалентности множеств, определяемых рекурсивно каноническими исчислениями $E,F$.

Давайте волноваться поэтапно. Итак, что Вы хотели сказать в этом абзаце?

Сравнил со стр. 84 монографии - блин, даже монография развалилась - пришлось клеить. Там $E$ - любое РП множество. А Вы взяли $E$ пустое.

Короче, не понял связь Вашего абзаца с последним абзацем стр.84 монографии.

[man]

[vek88]

Итак, здесь написано следующее.

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

Далее, пусть $a$ - произвольное слово в алфавите исчисления $E$. Ему сопоставим исчисление $G$ с аксиомой $a$. Построим исчисление, определяющее пересечение этих двух исчислений (см. выше в книге - это конструктивная операция). Множество, определяемое этим исчислением равно $\varnothing$ тогда и только тогда, когда $a \notin E$. Следовательно, алгоритмически разрешима проблема распознавания $a \notin E$.

Так Вам больше нравится? И в чем состоит Ваш вопрос?

[man]

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

Так лучше?

Так эквивалентно
Написано же $a \in E$ неразрешимо.

-- Чт ноя 11, 2010 21:07:39 --

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

Далее, пусть $a$ - произвольное слово в алфавите исчисления $E$.
... тогда и только тогда, когда $a \notin E$.

Это как ?