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

[EminentVictorians]

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

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

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

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

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

Вы никогда не видели формальных доказательств? Вот пример доказательства в ZFC, что пустое множество единственно:



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

[epros]

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

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

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

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

Вы никогда не видели формальных доказательств?

Видел, и сам доказывал.

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

Вот пример доказательства в ZFC, что пустое множество единственно:

А Ваш вариант доказательства каков?

[EminentVictorians]

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

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

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

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

А Ваш вариант доказательства каков?

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

-- 07.03.2024, 12:25 --

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

А Ваш вариант доказательства каков?

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

Теорема.
Пустое множество единственно.

Доказательство:
Предположим, нашлись 2 различных пустых множества $\varnothing_1$ $\ne$ $\varnothing_2$. Раз они различны, значит существует элемент $x$, принадлежащий одному из них и не принадлежащий другому. Получаем 2 варианта:
1) $x \in \varnothing_1$ и $x \notin \varnothing_2$
2) $x \in \varnothing_2$ и $x \notin \varnothing_1$

Первый случай приводит к противоречию, т.к. получается, что пустое множество $\varnothing_1$ непусто (т.к. содержит элемент $x$). По этой же причине и второй случай приводит к противоречию. Получается, что к противоречию приводит наше предположение о существовании двух различных пустых множеств. Следовательно, пустое множество единственно, чтд.

[epros]

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

Я бы потом несколько страниц темы распинался бы про функцию Дирихле или сигнум, а в итоге оказалось бы, что и понятие функции, и понятие непрерывности Вы понимаете как в конструктивном анализе.

А я должен догадаться, что Вы принимаете всю аксиоматику ZFC, действительные числа понимаете как сечения Дедекинда, а функцию - как множество упорядоченных пар, таких что ... ?

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

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

И это называется аксиоматикой.

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

Предположим, нашлись 2 различных пустых множества $\varnothing_1$ $\ne$ $\varnothing_2$.

1) $\exists \varnothing_1, \varnothing_2~(\varnothing_1 \ne \varnothing_2) \land (\forall x~x \notin \varnothing_1) \land (\forall x~x \notin \varnothing_2)$ (гипотеза).

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

Раз они различны, значит существует элемент $x$, принадлежащий одному из них и не принадлежащий другому.

2) $\varnothing_1 \ne \varnothing_2$ (из 1).
3) $\exists x~(x \in \varnothing_1 \land x \notin \varnothing_2) \lor (x \notin \varnothing_1 \land x \in \varnothing_2)$ (из 2 и экзистенциальности).

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

Получаем 2 варианта:
1) $x \in \varnothing_1$ и $x \notin \varnothing_2$
2) $x \in \varnothing_2$ и $x \notin \varnothing_1$

Это уже сказано.

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

Первый случай приводит к противоречию, т.к. получается, что пустое множество $\varnothing_1$ непусто (т.к. содержит элемент $x$).

4) $x \notin \varnothing_1$ (из 1).
5) $(x \in \varnothing_1 \land x \notin \varnothing_2) \to \bot$ (из 4).

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

По этой же причине и второй случай приводит к противоречию.

6) $x \notin \varnothing_2$ (из 1).
7) $(x \notin \varnothing_1 \land x \in \varnothing_2) \to \bot$ (из 6).

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

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

8) $(\exists x~(x \in \varnothing_1 \land x \notin \varnothing_2) \lor (x \notin \varnothing_1 \land x \in \varnothing_2)) \to \bot$ (из 5 и 7).

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

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

9) $(\exists \varnothing_1, \varnothing_2~(\varnothing_1 \ne \varnothing_2) \land (\forall x~x \notin \varnothing_1) \land (\forall x~x \notin \varnothing_2)) \to \bot$ (из 8).
10) $\forall \varnothing_1, \varnothing_2~((\forall x~x \notin \varnothing_1) \land (\forall x~x \notin \varnothing_2)) \to (\varnothing_1 = \varnothing_2)$ (из 9 снятие двойного отрицания).

Есть какие-то претензии к такой формализации?

[EminentVictorians]

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

А я должен догадаться, что Вы принимаете всю аксиоматику ZFC, действительные числа понимаете как сечения Дедекинда, а функцию - как множество упорядоченных пар, таких что ... ?

Ну не просто же так такая математика называется классической.

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

1) $\exists \varnothing_1, \varnothing_2~(\varnothing_1 \ne \varnothing_2) \land (\forall x~x \notin \varnothing_1) \land (\forall x~x \notin \varnothing_2)$ (гипотеза).

В языке ZFC нету символов $\varnothing_1$ и $\varnothing_2$. Их надо явно прописывать через $\in$. Но в принципе это мелочи.

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

Есть какие-то претензии к такой формализации?

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

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

[epros]

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

В языке ZFC нету символов $\varnothing_1$ и $\varnothing_2$. Их надо явно прописывать через $\in$. Но в принципе это мелочи.

Ха, по правилам исчисления предикатов имеем право использовать неограниченное количество предметных переменных. Вот это они и есть. Или Вам обязательно нужно, чтобы были $x_1$ и $x_2$?

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

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

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

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

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

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

[A-u-uuu]

(Оффтоп)

Про графы, вершины и ветви. Было интересно, вот вопрос:

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

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

Существует ли простой циклический бесконечный граф ?
Его не существует во всех возможных мирах(универсумах), или только в некоторых ?

[epros]

A-u-uuu в сообщении #1632158 писал(а):

простой циклический бесконечный граф

Что это такое?

[EminentVictorians]

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

Или Вам обязательно нужно, чтобы были $x_1$ и $x_2$?

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

[epros]

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

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

Или Вам обязательно нужно, чтобы были $x_1$ и $x_2$?

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

Предлагаю трактовать $\varnothing$ как новую латинскую букву. А вообще-то я специально для Вас выбрал такие переменные, чтобы сразу была видна связь с Вашим текстом "на человеческом языке".

[A-u-uuu]

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

A-u-uuu в сообщении #1632158 писал(а):

простой циклический бесконечный граф

Что это такое?

Это окружность.
Почему-то, она неизбежно континуальна.

[tolstopuz]

A-u-uuu в сообщении #1632523 писал(а):

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

A-u-uuu в сообщении #1632158 писал(а):

простой циклический бесконечный граф

Что это такое?

Это окружность.

Что является вершинами и ребрами этого графа?