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

[epros]

EminentVictorians, ответьте на такой вопрос: Если у нас есть множество, в которое входят последовательности нулей любой конечной длины, значит ли это, что в этом множестве есть бесконечная последовательность нулей?

[EminentVictorians]

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

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

Речь о множестве $X = \{0, 00, 000, 0000, ... \}$? Нет, в таком множестве бесконечной последовательности нулей нету.

Заранее догадываюсь, о чем пойдет речь дальше, поэтому можно сразу рассмотреть еще одно множество.
Пусть $A = 000..00..$ - бесконечная строчка, состоящая из нулей.
Рассмотрим множество $Y$ всевозможных её префиксных подстрок. (Подстрока не обязана быть конечной)
Тогда $X \subset Y$ и вместе с этим $X \ne Y$ (т.к. в $Y$ будет в качестве одного из элементов сама строка $A$)

Чувствуете разницу?

-- 04.03.2024, 23:39 --

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

[Mikhail_K]

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

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

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

В моём представлении, (бинарное) дерево - это множество вершин, для каждой из которых указано, к уровню с каким натуральным номером она принадлежит (причём к начальному уровню принадлежит только корень) и с какими вершинами (в количестве 0, 1 или 2) из следующего уровня соединена. Тогда для любой последовательности вершин, конечной или бесконечной, есть критерий, является ли эта последовательность ветвью или не является - для этого надо убедиться, что первая вершина в последовательности является корнем, каждая следующая имеет уровень на единицу больше чем предыдущая, и любые две соседние вершины в этой последовательности соединены.

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

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

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

А, это какая-то странная математика без множеств, но с логикой второго порядка?
Ну смотрите: в своём сообщении Вы стали говорить про "граф", не указав, в каком смысле Вы понимаете этот термин. По-моему, естественно воспринимать граф как множество с той или иной структурой - во всяком случае, если не оговорено что-то другое. Но ничего оговорено не было.

[manul91]

Ну уж если на таком уровне то пожалуй не стыдно привести свое доказательство что бесконечной ветви НЕТ.
Используем условие:

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

Итак, бинарное дерево - это граф, начинающийся с узла, именуемого "корнем", от каждого узла которого условно вниз, в сторону следующих узлов (потомков) отходят не более двух рёбер, условно "левое" и "правое". Это значит, что каждый узел бинарного дерева можно кодировать конечной двоичной последовательностью $p_1 p_2 \cdots p_n$, где каждая цифра $p_i$ означает шаг влево, если это нуль, и шаг вправо, если это единица (корень кодируется пустой строкой). Ветви, соответственно, кодируются конечными или бесконечными двоичными последовательностями. Кодировка конечной ветви совпадает с кодировкой её конечного узла.
Определим бинарное дерево как содержащее все ветви длиной $n \in \mathbb N$, для которых $p_n=1$ и $p_i=0$ для всех $i \ne n$. И добавим в определение следующую замечательную аксиому второго порядка: "Других ветвей у этого дерева нет".

1. Обозначим множество "все ветви длиной $n \in \mathbb N$, для которых $p_n=1$ и $p_i=0$ для всех $i \ne n$" как $V$.
2. Пусть $L$ - какая-то бесконечная ветвь. Бесконечная $L$ натуральную длину $n$ (где $n$ натуральное число $n \in \mathbb N$) не имеет по определению. Значит не принадлежит множеству ветвей $V$ (т.к. любая ветвь из $V$ обязана иметь длину $n$, $n \in \mathbb N$ по определению $V$.)
3. Допустим что $L$ принадлежит бинарному дереву.
4. Но из аксиому "Других ветвей у этого дерева нет" следует что $L$ дереву не принадлежит, ибо не принадлежит $V$. Противоречие, значит допущение 3) неверно. Следовательно, $L$ не принадлежит бинарному дереву.
Что не так? :)

[epros]

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

А, это какая-то странная математика без множеств, но с логикой второго порядка?

Reverse mathematics - это направление математических исследований, интересующееся вопросами оснований: какая математика из какой аксиоматики следует. Там не логика второго порядка, а только разные подмножества языка второго порядка используются для того, чтобы определить ту или иную систему. Система $\text{RCA}_0$ - самая слабая, в некотором смысле эквивалентна конструктивному анализу. Не то чтобы это было "без множеств", теории множеств как таковые не отвергаются, просто дело не в множествах.

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

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

Я ничего не имею против того, чтобы использовать понятие "множество", главное не тащить вслед за ним сильную аксиоматику типа ZFC.

[epros]

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

для любой последовательности вершин, конечной или бесконечной, есть критерий, является ли эта последовательность ветвью или не является

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

[EminentVictorians]

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

И это вопрос определения понятия "ветвь"

Так может приведете это определение? Но на нормальном, принятом в математике уровне строгости.

[talash]

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

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

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

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

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

[epros]

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

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

И это вопрос определения понятия "ветвь"

Так может приведете это определение? Но на нормальном, принятом в математике уровне строгости.

Определить можно по-разному. Я, разумеется, постараюсь определить так, чтобы это имело смысл не с точки зрения Вашей интуиции о "множествах", а с точки зрения $\text{RCA}_0$, которая всё рассматривает в аспекте алгоритмической разрешимости.

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

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

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

Для того дерева, которое было определено первоначальной постановкой задачи, алгоритм определения вершины, очевидно, должен работать так: Он проверяет, что все символы поданной ему на вход строки, кроме последнего, являются нулями. Если это так, то отвечает "Да", иначе отвечает "Нет". Точка останова для любой конечной строки заведомо есть, так что процедура определения вершин тривиальна.

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

[EminentVictorians]

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

Поэтому двоичное дерево определяется как алгоритм

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

Вообще, первоначально все начиналось вот с этого:

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

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

Вопрос стоит так: "Зачем нужна логика второго порядка, когда есть теория множеств первого порядка?". Что такого позволит, например, теория множеств второго порядка, чего не позволяет теория множеств первого порядка? Вот что интересно.

[manul91]

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

Бинарный граф будем называть множество из бинарных последовательностей (как конечных, так и бесконечных), причем последовательности в множестве удовлетворяют следующими требованиями:
1) Любая из конечных последовательностей в множестве, не является префиксом (и не совпадает с) какой-либо другой конечной последовательности из множества
2) Любая из конечных последовательностей в множестве, не является префиксом какой-либо бесконечной последовательности из множества
3) Любые две бесконечные последовательности в множестве отличаются (в обычном смысле - что существует натуральное $n$, для которого соответные разряды бесконечных последовательностей отличаются)

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

Теперь рассмотрим следующее рассуждение:

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

Предположим, что бесконечной ветки нету. Тогда путь от корня по левым вершинам с координатами вида 00..0 конечен.

Наш граф - множество содержащее все конечные последовательности нулей и оканчивающиеся на единицу.
Из того, что "бесконечней ветки нету" - отнюдь не следует что "путь от корня по левым вершинам с координатами вида 00..0 конечен".
Второе утверждение - это утверждение про "пути" (т.е. "последовательности подветок") - и таки да, у нас в множестве имеются ветки (и соотвенно подветки) с любым количеством нулей в начале. Но все они конечны (тем более, оканчиваются на 1) по определению.
Если перевести рассуждение на языке последовательностей (предерживаясь определению графа выше "через веток"), то хорошо видна его несостоятельность:
Этот граф определяется бесконечным множеством (счетном, их можно упорядочить даже) конечных последовательностей "ветвей":
1,
01
001,
0001,
......
Тогда:

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

Предположим, что бесконечной ветки нету.

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

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

Тогда путь от корня по левым вершинам с координатами вида 00..0 конечен.

переводится как "тогда найдется такое $n$ что в множестве нет последовательности с более чем $n$ нулей". ("путь" - это последовательный выбор подветок разных элементов из множества, с возрастающим количеством нулей в начале).
Очевидно что второе из первым никак не следует.
"путь от корня по левым вершинам с координатами вида 00..0" - хотя это и "путь" - но это же не ветка! : ) Поэтому из отсутствия бесконечной ветки, ничего не может следовать про конечности или бесконечности каких-то "путей"/(наборов "подветок").
В множестве бесконечной последовательности нет, все правильно.
Но это отнюдь не означает, что для какого-то $n$ не найдется последовательности с более чем $n$ нулями.
Наоборот, для любого $n$ найдется (притом бесконечное количество) последовательностей (веток) с больше чем $n$ нулей. Но тем не менее все они - конечные :)

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

Вывод - все дело в определении графа, и что такое "ветвь"...

[epros]

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

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

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

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

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

[epros]

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

Вообще, первоначально все начиналось вот с этого:

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

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

Вопрос стоит так: "Зачем нужна логика второго порядка, когда есть теория множеств первого порядка?". Что такого позволит, например, теория множеств второго порядка, чего не позволяет теория множеств первого порядка? Вот что интересно.

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

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

Но если уж возвращаться к теме, то скажите, если Вы подозреваете, что логика не сводится к исчислению предикатов (неважно какого порядка), то какие у Вас конкретные основания для этого? Можете ли Вы привести пример "обычного человеческого" рассуждения (но при этом безупречно логичного), которое не формализуется в исчислении предикатов?

[EminentVictorians]

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

Но если уж возвращаться к теме, то скажите, если Вы подозреваете, что логика не сводится к исчислению предикатов (неважно какого порядка), то какие у Вас конкретные основания для этого?

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

Я сам пару лет назад ради эксперимента формализовал несколько простейших теорем в формальной ZFC. Ощущение такое, что это была наверное самая бесполезная деятельность, которую я когда либо делал. Более того, ладно бы формализация всегда была бы просто более длинной и душной версией исходного человеческого рассуждения. Но ведь нет, иногда в процессе формализации приходится менять саму логическую структуру первоначального рассуждения, подстраивая её под требования формалистов. А учитывая, что реально формализована очень маленькая часть математики, нет никакой гарантии, что такое подстраивание всегда может быть реализовано.

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

[epros]

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

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

Это же просто означает, что все Ваши претензии относятся к чему-то, Вами же и воображаемому.

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

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

А кто запрещает людям рассуждать "обычным человеческим образом"? Мы в своей речи используем кучу понятий, которые определены "где-то в другом месте". Именно это даёт большую экономию бумаги и сил. И никакие "формалисты" против этого не возражают. Просто если вдруг выяснится, что какие-то понятия могут быть неоднозначно поняты, мы уточняем их определения. Вот выше Вы просили меня уточнить определения графа и ветви в графе, это нормально. Это же касается и логики: Если Вы в своих рассуждениях из некоторого $A$ выводите некоторое $B$, а собеседник Вас не понимает, то он просит Вас уточнить правила вывода и откуда Вы их взяли. Если Вы в конечном итоге скажете, что это согласно такой-то аксиоме исчисления высказываний или исчисления предикатов, то вроде бы больше вопросов быть не может. Вот это и есть формализация на самом деле.

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

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

Ну так наверняка это и была бесполезная деятельность. Любопытно было бы убедиться на примере.