Сводится ли логика к исчислению предикатов?

[EminentVictorians]

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

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

Это мне очень интересно. Можете вкратце рассказать или дать ссылки на какую-нибудь литературу?

[talash]

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

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

А эта система строго установленных правил может быть автоматизирована? Чтобы логику машина проверяла.

[epros]

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

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

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

Это мне очень интересно. Можете вкратце рассказать или дать ссылки на какую-нибудь литературу?

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

Я здесь писал про слабую лемму Кёнига и приводил пример определения бесконечного двоичного дерева, не имеющего бесконечной ветви (т.е. эту лемму нарушающего). Так вот, в определении существенна аксиома, являющаяся утверждением второго порядка: "Других ветвей у этого дерева нет". Что Вы об этом думаете?

-- Пн мар 04, 2024 17:05:56 --

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

А эта система строго установленных правил может быть автоматизирована? Чтобы логику машина проверяла.

Так автоматизируют же.

[Mikhail_K]

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

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

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

Множества в ZFC - это не только те, которые могут быть конструктивно построены, а "все" множества - ровно в том же смысле (и с той же степенью осмысленности), как и в логике второго порядка свойства - это не только выразимые в языке, а "все".

[epros]

Mikhail_K, Вы правильно говорите. Но дело в том, что в теории множеств первого порядка даже не всем свойствам соответствуют множества. Так что квантификация по всем множествам не равна квантификации по всем свойствам.

[EminentVictorians]

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

Я здесь
писал про слабую лемму Кёнига и приводил пример определения бесконечного двоичного дерева, не имеющего бесконечной ветви (т.е. эту лемму нарушающего). Так вот, в определении существенна аксиома, являющаяся утверждением второго порядка: "Других ветвей у этого дерева нет". Что Вы об этом думаете?

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

$$\xymatrix{ & & & & \\& & A \ar[dl]_{} & & \\ & B \ar[dl]_{} \ar[dr]_{} & & &\\D & & C & & \\ }$$

вершина $A$ кодируется пустой строкой, вершина $B$ строкой "0", вершина $C$ строкой "01", а вершина $D$ строкой "00". Пока все правильно?

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

[Mikhail_K]

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

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

И вершины, и ветви кодируются двоичными последовательностями. Чтобы закодировать ветвь, мы проходим её от корня к конечной вершине и на каждом шаге выписываем число 0, если шаг был влево и число 1, если шаг был вправо. Каждая вершина кодируется так же, как ведущая к ней (единственная) ветвь. Например, ветвь $ABC$ (как и вершина $C$) кодируется строкой "01", а ветвь $ABD$ (как и вершина $D$) строкой "00". Единственная разница в том, что ветви могут быть бесконечными, и тогда они кодируются бесконечными двоичными последовательностями, а вершины могут кодироваться только конечными.

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

[EminentVictorians]

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

И вершины, и ветви кодируются двоичными последовательностями. Чтобы закодировать ветвь, мы проходим её от корня к конечной вершине и на каждом шаге выписываем число 0, если шаг был влево и число 1, если шаг был вправо. Каждая вершина кодируется так же, как ведущая к ней (единственная) ветвь. Например, ветвь $ABC$ (как и вершина $C$) кодируется строкой "01", а ветвь $ABD$ (как и вершина $D$) строкой "00". Единственная разница в том, что ветви могут быть бесконечными, и тогда они кодируются бесконечными двоичными последовательностями, а вершины могут кодироваться только конечными.

А, т.е. ветвь обязана идти из корня, хорошо.

А из вершины может быть одна стрелка? (как на моем графе из вершины $A$) Или обязательно либо 2 либо 0?

-- 04.03.2024, 18:39 --

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

-- 04.03.2024, 18:46 --

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

Определим бинарное дерево как содержащее все ветви длиной $n \in \mathbb N$, для которых $p_n=1$ и $p_i=0$ для всех $i \ne n$.

Вот еще этот фрагмент не могу расшифровать. Я правильно понял, что по определению, бинарное дерево содержит каждую из ветвей вида 01, 001, 0001, 00001, .... ?

[Mikhail_K]

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

Вот еще этот фрагмент не могу расшифровать. Я правильно понял, что по определению, бинарное дерево содержит каждую из ветвей вида 01, 001, 0001, 00001, .... ?

Да. epros считает, что можно постулировать отсутствие любых других ветвей, кроме этих (конечных с единственной единичкой на конце). Слабая лемма Кёнига считает, что если дерево содержит все перечисленные ветви, то оно содержит и бесконечную ветвь 0000...

[EminentVictorians]

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

Да. epros считает, что можно постулировать отсутствие любых других ветвей, кроме этих (конечных с единственной единичкой на конце). Слабая лемма Кёнига считает, что если дерево содержит все перечисленные ветви, то оно содержит и бесконечную ветвь 0000...

Очевидно же, что бесконечная ветка существует.

Доказательство:

Пусть $V$ - множество вершин нашего дерева
$\mathbb N$ - множество натуральных чисел. Будем считать, что оно начинается с единицы.
В доказательстве будет использоваться понятие частичной функции, поэтому напомню пару элементарных фактов о них.
Частичной функцией называется упорядоченная тройка $f = (X, G, Y)$ такая, что
1) $G \subset X \times Y$
2) Если $(x, y) \in G$ и $(x, z) \in G$, то $y = z$.

Множество $\{x \in X| (\exists y \in Y) (x, y) \in G\}$ будем называть действительной доменной областью частичной функции $f$ и обозначать $\operatorname{dom} F$

Ветвью будем называть любую частичную инъективную функцию $f: \mathbb N \to V$ такую, что
1)Её действительная доменная область $S \subset \mathbb N$ представляет собой либо все $\mathbb N$ целиком, либо его начальный отрезок, не совпадающий с $[1, 1]$. (все начальные отрезки будем считать для удобство непустыми по определению).
2) ($\forall i \in S, i >1$) существует стрелка в графе, идущая из вершины $F(i-1)$ в вершину $F(i)$.

Будем называть ветвь бесконечной, если $\operatorname{dom} F = \mathbb N$ и конечной в противном случае.


Каждому $n \in \mathbb N, n > 1$ поставим в соответствие вершину с координатой $00...0$ ($n-1$ нолей). Число $1$ отобразим в корневую вершину. Данная функция является корректно определенной. Действительно, какой бы $n > 1$ мы бы ни взяли, существует вершина $x \in V$ нашего дерева с координатами $00..0$ ($n-1$ нолей). [по условию]. Имеем инъекцию $F: \mathbb N \to V$, $\operatorname{dom} F = \mathbb N$, которая в точности является искомой бесконечной ветвью нашего дерева. ЧТД.

-- 04.03.2024, 20:31 --

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

[epros]

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

Я, конечно, верю в слабую лемму Кёнига и думаю, что в примере epros бесконечная ветвь из нулей есть, а его "аксиома второго порядка" противоречит построению.

Интересно, как (чему именно противоречит)? Построение таково, что в дереве оказываются только те ветви, которые в него добавлены. Т.е. если мы добавили ветви $1$, $01$ и $001$, то в нём будут только эти три ветви, никакая четвёртая ветвь появиться не может. После того, как мы добавляем бесконечное количество таких (конечных) ветвей, мы последней аксиомой объявляем, что никаких больше ветвей в дерево добавляться не должно. Откуда возьмётся бесконечная ветвь?

Напомню, что точно такая же логика применяется при построении множества натуральных чисел: Каждое последующее число больше предыдущего, но при этом конечно. В множество добавлено бесконечное количество таких (конечных) чисел. После этого мы аксиомой индукции объявляем, что других чисел в это множество добавляться не должно. Напомню, что здесь проходили жаркие баталии с целью доказать всем сомневающимся, что никакого "бесконечного натурального числа" в множестве натуральных чисел нет.

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

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

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

Ну давайте попробуем. Но вообще-то хочу сразу предупредить, что слабая лемма Кёнига потому и лежит в основании системы $\text{WKL}_0$ (и не лежит в основании системы $\text{RCA}_0$), что она невыводима из остальной аксиоматики $\text{RCA}_0$.

[EminentVictorians]

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

Построение таково, что в дереве оказываются только те ветви, которые в него добавлены. Т.е. если мы добавили ветви $1$, $01$ и $001$, то в нём будут только эти три ветви, никакая четвёртая ветвь появиться не может. После того, как мы добавляем бесконечное количество таких (конечных) ветвей, мы последней аксиомой объявляем, что никаких больше ветвей в дерево добавляться не должно.

???

epros, откуда Вы все это берете? Я настолько странных текстов в жизни не видывал.


Неориентированный граф - это просто упорядоченная тройка $(V, E, \varphi)$, где $V$ - множество вершин, $E$ - множество ребер, а $\varphi$ - это функция, ставящая в соответствие каждому ребру $e \in E$ некоторую (неупорядоченную) пару $\{u, v\}$ вершин.

Ориентированный граф - это упорядоченная четверка $(V, E, \varphi, \psi)$, где
$V$ - множество вершин,
$E$ - множество ребер,
$\varphi$ - это функция домена, ставящая в соответствие каждому ребру $e \in E$ некоторую вершину из $V$
$\psi$ - это функция кодомена, ставящая в соответствие каждому ребру $e \in E$ некоторую вершину из $V$


Нету тут никаких построений, бесконечных процессов, объявлений аксиом и всего такого подобного. Граф - это просто множество.

[epros]

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

Ваше "доказательство" я нахожу излишне замороченным и при этом страдающим от неоднозначности формулировок.

[manul91]

Определение что называть "ветвью" в данном случае, вроде уже дано в условии?

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

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

Но

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

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

Используя "свое" определение ветви ("ветви по EminentVictorians"), вы доказываете что-то о "ветвeй по EminentVictorians" а не про ветвей из оригинальной задаче (по меньшей мере, обратное далеко не очевидно).

[EminentVictorians]

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

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

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

Предположим, что бесконечной ветки нету. Тогда путь от корня по левым вершинам с координатами вида 00..0 конечен. Значит, существует вершина с координатами 00..0 ($n$ нолей) и вместе с этим не существует вершины с координатами 00..0 ($n+1$ нолей). По условию, в дереве существует ветка 00..01 ($n+1$ нолей и единица в конце). Следовательно, раз ветки кодируются своими конечными точками, существует точка с координатами 00..01 ($n+1$ нолей и единица в конце), а значит существует и точка с координатами 00..0 ($n+1$ нолей) [просто убрали последнюю единичку]. Получается, что точка с координатами 00..0 ($n+1$ нолей) одновременно и существует, и не существует. Получили противоречие, следовательно бесконечная ветка есть.