Можно ли построить логику с помощью школьной математики?

[dgwuqtj]

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

Представьте себе алгебраическую систему

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

[epros]

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

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

Я же уже использовал её в примере, когда из $x=0 \to \forall x~x=0$ выводилось $(\exists x~x=0) \to (\forall x~x=0)$.

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

хотя я не знаю, как она выведена

Вряд ли Вы её выведете. Подсказка: квантор всеобщности должен обобщать конъюнкцию, а квантор существования - дизъюнкцию.

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

А вот по поводу «такое обобщение не имеет смысла» не согласен

Не имеет смысла по очевидной причине: незачем ставить квантор $\forall x$ на формулу, в которой нет переменной $x$.

[BorisK]

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

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

Начну издалека. Даю краткий пересказ определения интерпретации (Мендельсон (1971), с. 57 ). В Sixth edition то же самое.
Интерпретация языка первого порядка это система, в которой каждой предикатной букве $A^n_j$ соответствует некоторое $n$-местное отношение в $D$. Всякое $n$-местное отношение – это подмножество ДП $D^n$, элементами которого являются $n$-ки элементов множества $D$, названного областью интерпретации.
О функциональных символах мы пока не будем говорить, так как речь идет об аксиомах, правилах вывода и многих теоремах исчисления предикатов первого порядка, в записи которых не используются функциональные символы. Это не так уж и мало. А вообще $n$-местный функциональный символ можно представить как $n+1$-местное отношение с определенными свойствами.
Так что можно считать, что $D^n$ - это множество, а все его подмножества (т.е. интерпретации предикатов и формул) можно анализировать с использованием законов алгебры множеств по Куранту и Роббинсу, в которой помимо операций определено отношение включения. Разница лишь в том, что элементами этих множеств являются не только элементы множества $D$, но и $n$-ки элементов из $D$.
Вот Вам и алгебраическая система. Поскольку речь зашла о подробностях, то у меня нет иного выбора, как вести речь о конкретной алгебраической системе – об алгебре кортежей (АК), краткие сведения о которой я на днях разместил в Интернете.
В АК традиционная интерпретация расширена. В ней предусматриваются следующие особенности:
1) определены операции, для которых доказано, что они соответствуют логическим связкам ($\vee, \wedge, \neg, \forall, \exists$);
2) общезначимость импликации $A \to B$ интерпретируется как выполнимость соотношения $I(A) \subseteq I(B)$;
3) областью интерпретации является ДП $D_1 \times D_2, \times \dots, \times D_n$, в котором $D_i$ могут быть разными множествами;
4) законы алгебры множеств по Куранту и Роббинсу верны без исключения.

Цитата:

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

Во-первых, это не совсем обычные доказательства (см. выше), А про правило вывода могу добавить, что в АК интерпретацией упомянутого в прошлых сообщениях правила $GenDT$ является операция добавления фиктивного атрибута, с помощью которой отношения с разными схемами отношения легко преобразуются в однотипные (т.е. имеющие одинаковые схемы отношения). И поэтому в АК нельзя с помощью интерпретации правила $GenDT$ получить результат без исключений вроде $I(\neg \psi) = I(\forall x~\neg \psi)$, который является интерпретацией упоминавшейся ранее «равносильности»: $\neg \psi$ равносильно $\forall x~\neg \psi$.

-- 18.07.2025, 15:39 --

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

Я же уже использовал её в примере, когда из $x=0 \to \forall x~x=0$ выводилось $(\exists x~x=0) \to (\forall x~x=0)$.

Ваш пример не соответствует схеме аксиом $\bigl(\forall x~\varphi \to \psi\bigr) \to \bigl((\exists x~\varphi) \to \psi\bigr)$, где $\psi$ не имеет свободных вхождений $x$, так как в этой схеме используется формула $\psi$, которая в общем случае никак не зависит от $\varphi$. Допустим, она не содержит свободных вхождений $x$, но при этом она может не совпадать с $\forall x~\varphi$ (например, $\forall x~x=25$). А в Вашем примере получается $\bigl(\varphi \to \forall x~\varphi\bigr)$. В нем не видно формулы $\psi$, никак не связанной с формулой $\varphi$.

Цитата:

Вряд ли Вы её выведете. Подсказка: квантор всеобщности должен обобщать конъюнкцию, а квантор существования - дизъюнкцию.

Я попробую доказать общезначимость формулы $\bigl(\forall x~\varphi \to \psi\bigr) \to \bigl((\exists x~\varphi) \to \psi\bigr)$. Но не сегодня. А за подсказки спасибо. Только мне они (уж поверьте!) не нужны.

[epros]

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

Ваш пример не соответствует схеме аксиом $\bigl(\forall x~\varphi \to \psi\bigr) \to \bigl((\exists x~\varphi) \to \psi\bigr)$, где $\psi$ не имеет свободных вхождений $x$, так как в этой схеме используется формула $\psi$, которая в общем случае никак не зависит от $\varphi$.

Что это вообще значит, что одна формула "зависит" или "не зависит" от другой? И разве в схеме аксиом написано, что вторая формула должна "не зависеть" от первой? То, что использованы разные символы метапеременных, означает всего лишь, что подставляемые формулы могут быть разными. Но могут быть и вообще одинаковыми.

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

Допустим, она не содержит свободных вхождений $x$,

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

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

но при этом она может не совпадать с $\forall x~\varphi$ (например, $\forall x~x=25$). А в Вашем примере получается $\bigl(\varphi \to \forall x~\varphi\bigr)$. В нем не видно формулы $\psi$, никак не связанной с формулой $\varphi$.

Она даже не совпадает с формулой $\varphi$. А могла бы совпадать. Если, конечно, в $\varphi$ нет свободных вхождений $x$, иначе схему применять будет нельзя.

[BorisK]

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

Что это вообще значит, что одна формула "зависит" или "не зависит" от другой? И разве в схеме аксиом написано, что вторая формула должна "не зависеть" от первой? То, что использованы разные формулы метапеременных, означает всего лишь, что подставляемые формулы могут быть разными. Но могут быть и вообще одинаковыми.

Не понимаю Ваших возражений. В схеме аксиом разрешается в качестве $\psi$ использовать формулу $\forall x~x=25$, а в Вашем примере это запрещено!

[epros]

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

Не понимаю Ваших возражений. В схеме аксиом разрешается в качестве $\psi$ использовать формулу $\forall x~x=25$, а в Вашем примере это запрещено!

Каким образом мой пример может запретить использовать формулу $\forall x~x=25$ в другом примере? Он просто использует другую формулу: $\forall x~x=0$.

[BorisK]

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

Он просто использует другую формулу: $\forall x~x=0$.

Потому, что Вы задали $\varphi$ как $x=0$. Тогда $\psi$ может быть только $\forall x~x=0$, но никак не $\forall x~x=25$. Это и есть запрет.

[epros]

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

Потому, что Вы задали $\varphi$ как $x=0$. Тогда $\psi$ может быть только $\forall x~x=0$, но никак не $\forall x~x=25$. Это и есть запрет.

Ну так я же применяю схему к $x=0 \to \forall x~x=0$, а не к $x=0 \to \forall x~x=25$.

[BorisK]

Выполняю обещанное.
Нужно с помощью АК доказать общезначимость формулы $\bigl(\forall x~\varphi \to \psi\bigr) \to \bigl((\exists x~\varphi) \to \psi\bigr)$ ($\psi$ не имеет свободных вхождений переменной $x$), которую epros предложил как схему аксиом. Я все же буду использовать формулу
$\bigl(\forall x(A \to B)\bigr) \to \bigl((\exists x~A) \to B\bigr)$, в которой формула $B$ не имеет свободных вхождений переменной $x$.
Мне так удобней, а за лишнюю пару скобок и использование латиницы вместо греческого алфавита к суду не привлекут.
Далее будем называть эту формулу $eAS$.
Будет доказано, что левая часть формулы $eAS$ равносильна правой части. Так что здесь вроде бы имеет место быть перевыполнение плана.
Учитывая то, что мой пример опровержения формулы $BF$ не вызвал возражений и вопросов, то я буду в доказательстве использовать терминологию и сводку теорем АК. Схема доказательства будет следующей.

$(i)$ Поскольку в $eAS$ только одна переменная с квантором, то для ее обоснования достаточно рассмотреть бинарные отношения (достаточность можно доказать). Будем считать, что это АК-объекты со схемой отношения $[XY]$. Атрибут $X$ соответствует переменной $x$ в $eAS$. Тогда интерпретациями формул $A$ и $B$ в $eAS$ будут АК-объекты $I \bigl(A[XY] \bigr)$ и $I \bigl(B[XY] \bigr)$ или просто $I(A)$ и $I(B)$ с учетом того, что схемы отношений у них одинаковы. Тогда, если не оговорено противное, будем считать, что все упоминаемые далее интерпретации заданы в схеме отношения $[XY]$.

$(ii)$ Множества $X$ и $Y$ могут быть эквивалентными, но в доказательстве их элементы обозначаются по разному ($a_i, b_i$), чтобы показать, что они относятся к разным проекциям ($[X]$ или $[Y]$ соответственно).

$(iii)$ Докажем сначала, что для любой формулы $R$ и формулы $B$, не имеющей свободных вхождений переменной $x$, формулы $\forall x(R \vee B)$ и $(\forall x~R) \vee B$ равносильны.

$(iv)$ Заменив $R$ на $\neg A$, докажем равносильность $\forall x(A \to B)$ и $(\exists x~A) \to B$.

Приступим к доказательству.
1. Для бинарного отношения $I(R)$ выполним эквивалентное преобразование, которое назовем $Y$-разделением.
1.1. Выразим $I(R)$ в виде множества элементарных кортежей $(a_i,b_j)$.
1.2. Объединим кортежи с одинаковыми $b_j$ в $C$-кортежи. Например, кортежи $(a_1,b_3)$ и $(a_4,b_3)$ можно выразить как $C$-кортеж $\bigl[\{a_1, a_4\}~~\{b_3\} \bigr]$.
1.3. Используя Теорему 5 (пункт2) объединим все $C$-кортежи типа $\bigl[\ast~~\{b_j\} \bigr]$ в один $C$-кортеж $\bigl[\ast~~S_R \bigr]$ (напоминаю: $\ast$ - фиктивная полная компонента, здесь $\ast = X$).
1.4. $Y$-разделение для $I(B)$ не нужно, так как отношение $I(B)$ можно представить как $C$-кортеж $\bigl[\ast~~S_B \bigr]$, где $S_B \subseteq Y$ (Теоремы 5 (пункт 2), 31 и операция добавления фиктивного атрибута). Из этого следует, что $I(\forall x B) = I(B)$.

2. Докажем равенство $I(\forall x(R \vee B)) = I((\forall x~R) \vee B)$.
2.2. В $Y$-разделенной $C$-системе $I(R)$ помимо $C$-кортежа $\bigl[\ast~~S_R \bigr]$ могут содержаться $C$-кортежи типа $\bigl[X_i~~\{b_j\} \bigr]$, у которых $X_i \subset X$ (т.е. $X_i$ не полная компонента), а $b_i \notin S_R$.
2.3. $C$-кортежи $\bigl[\ast~~S_R \bigr]$ и $\bigl[\ast~~S_B \bigr]$ в $C$-системе $I(R) \cup I(B)$ можно выразить как один $C$-кортеж $Ast_{RB} = \bigl[\ast~~(S_R \cup S_B) \bigr]$ (Теорема 5). Поскольку в $Ast_{RB}$ компонента атрибута $X$ полная, то он включен в $I(\forall x(R \vee B))$.
2.4. Докажем, что $I(R \vee B) = I(R) \cup I(B)$ не содержит $C$-кортежей типа $\bigl[\ast~~\{b_j\} \bigr]$, у которых $b_j \notin (S_R \cup S_B)$. Чтобы такие $C$-кортежи в ней существовали, необходимо, чтобы в $I(R)$ содержался $C$-кортеж $\bigl[X_R~~\{b_j\} \bigr]$, а в $I(B)$ содержался $C$-кортеж $\bigl[X_B~~\{b_j\} \bigr]$ при следующих условиях: $b_j \notin (S_R \cup S_B)$ и $\bigl[X_R~~\{b_j\} \bigr] \cup \bigl[X_B~~\{b_j\} \bigr] = \bigl[\ast~~\{b_j\} \bigr]$ (Теорема 5, пункт 2).
2.5. Но $C$-кортеж $\bigl[X_B~~\{b_j\} \bigr]$ отсутствует в $I(B)$ по определению, а это означает, что кортежи типа $\bigl[\ast~~\{b_j\} \bigr]$, у которых $b_j \notin (S_R \cup S_B)$, не содержатся в $I(R \vee B)$. Отсюда $ I(\forall x(R \vee B)) = Ast_{RB} = \bigl[\ast~~(S_R \cup S_B) \bigr]$. Из этого следует равенство $I(\forall x(R \vee B)) = I((\forall x~R) \vee B)$ и равносильность формул $\forall x(R \vee B)$ и $(\forall x~R) \vee B$.

3. Рассмотрим результаты замены $R$ на $\neg A$. Тогда
3.1. Формула $\forall x(R \vee B)$ преобразуется в формулу $\forall x((\neg A) \vee B)$, которая равносильна формуле $\forall x(A \to B)$ и по пункту 2.5 формуле $(\forall x (\neg A)) \vee B$.
3.2. Формула $(\exists x~A) \to B$ равносильна формуле $\neg (\exists x~A) \vee B$.
3.3. Из равносильности $\forall x (\neg A)$ и $\neg (\exists x~A)$ следует равносильность формул $\forall x(A \to B)$ и $(\exists x~A) \to B$.

[BorisK]

В пункте 2 доказательства я с нумерацией накосячил: после 2. идет 2.2. Можно не исправлять, поскольку ссылка на пункт 2.5 правильная.

[BorisK]

Нашел опечатку. В конце пункта 2.2. вместо $b_i \notin S_R$ надо читать $b_j \notin S_R$. Но она, кажется, легко распознается по контексту.

[BorisK]

Что-то мои оппоненты долго не отвечают. Может быть, они сейчас отдыхают где-нибудь на берегу теплого моря, на перекатах или в связке на горном склоне? А, может быть, просто не нашли возражений?
Но у меня вопросы к знатокам появились.
1. Встречается ли в математике (в частности, в теории графов) что-то подобное методу $Y$-разделения бинарных отношений, с помощью которого решается проблема интерпретации выражений с кванторами?
2. Если не встречается, то как его лучше назвать? Варианты: $Y$-разложение, $Y$-ортогонализация.
3. Заслуживает ли полученный результат публикации в математическом журнале? Если да, то мне хотелось бы пригласить в соавторы самых активных моих критиков и вопрошателей по этой проблеме, потому что ваши вопросы и замечания вывели меня из спячки и заставили что-то придумать с вашей помощью. Как со мной можно связаться лично, вы, надеюсь, определите.

[BorisK]

Никто почему-то не ответил. Ладно, назову этот метод $Y$-разложением. А в теории графов есть представление графов списками смежных вершин. Что-то похожее, но не то. С помощью $Y$-разложения анализировать бинарные отношения (и графы тоже) проще и возможностей для анализа больше.
Предложенный метод доказательства теперь можно применять и для других выражений с кванторами. И нередко получается, что левые и правые части общезначимой импликации равносильны. Вот, например, аксиома $A5$ исчисления предикатов у Мендельсона:
$(\forall x_i)(B \to C) \to (B \to (\forall x_i)C)$ при условии, что формула $B$ не содержит свободных вхождений $x_i$. Здесь легко доказывается, что $(\forall x_i)(B \to C)$ и $B \to (\forall x_i)C$ равносильны.
Доказываем.
1. Из условия ясно, что $I(B) = \bigl[\ast~~S_B \bigr]$. Тогда $I(\neg B) = \bigl[\ast~~\overline {S_B} \bigr]$. Это означает, что в $I(\neg B)$ нет $C$-кортежей с неполными компонентами в проекции $[X]$.
2. Выполним $Y$-разложение $C$. В нем может содержаться $C$-кортеж типа $\bigl[\ast~~S_C \bigr]$, а также $C$-кортежи вида $\bigl[X_i~~\{b_j\} \bigr]$, у которых $X_i$ неполная компонента, а $b_j \notin S_C$.
3. В $I((\neg B) \vee C) = I(\neg B) \cup I(C)$ содержится $C$-кортеж $\bigl[\ast~~(\overline {S_B} \cup S_C) \bigr]$, а также $C$-кортежи вида $\bigl[X_i~~\{b_j\} \bigr]$, у которых $X_i$ неполная компонента, а $b_j \notin S_C$. Отсюда ясно, что в $I((\forall x_i)(\neg B) \vee C) = \bigl[\ast~~(\overline {S_B} \cup S_C) \bigr]$.
4. Ясно, что $I((\forall x_i)C) = \bigl[\ast~~S_C \bigr]$. Тогда $I((\neg B) \vee (\forall x_i)C) = \bigl[\ast~~(\overline {S_B} \cup S_C) \bigr]$. А это означает, что $(\forall x_i)(B \to C)$ и $B \to (\forall x_i)C$ равносильны.

В бинарных отношениях проще простого найти примеры, опровергающие равенство интерпретаций формул $D$ и $\forall x D$, равносильность которых можно «доказать» с помощью правила обобщения. Например, для опровержения достаточно формулу $D$ представить бинарным отношением, в $Y$-разложении которого присутствуют непустые $C$-кортежи $\bigl[X_i~~\{b_j\} \bigr]$, не включенные в $\bigl[\ast~~S_D \bigr]$. Тогда в $I(\forall xD)$ эти $C$-кортежи отсутствуют и о равенстве интерпретаций формул $D$ и $\forall x D$ можно только мечтать. Например, в универсуме $\{a,b,c\}^2$ такой интерпретацией является $C$-кортеж $\bigl[\{a,c\}~~\{c\} \bigr]$.
Мне, честно сказать, непонятно, чем привлекательно для математиков такое явное несоответствие между выводимой равносильностью и равенством в интерпретациях?
Чтобы этого несоответствия не было, достаточно только предложить еще одну версию исчисления предикатов с откорректированным правилом обобщения.
А, может быть, АК и есть интерпретация такой версии?

[BorisK]

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

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

Да, $\neg \psi$ равносильно $\forall x~\neg \psi$: В одну сторону оно следует в силу правила обобщения, а в другую сторону оно следует в силу схемы аксиом конкретизации всеобщности.

Равносильно в том смысле, что они друг из друга выводятся. При этом $\neg \psi \leftrightarrow \forall x \, \neg \psi$ не общезначима.

Уважаемые оппоненты! Это что же получается? Мы с вами ненароком обратную сторону теоремы Геделя о полноте опрокинули?

Напомню формулировку «В исчислении предикатов первого порядка доказуемы (т.е выводимы) только логически обоснованные (т.е. общезначимые) формулы». А тут, как чёртик из табакерки, вскакивает интерпретация, в которой выводимая равносильность на самом деле не общезначима. Причем процентик несоответствия немаленький. Давайте подсчитаем.

Итак, по аналогии с доказательством epros можно доказать, что формулы $\psi$ и $\forall x~ \psi$ равносильны. Рассмотрим сначала универсум $\{a,b,c\} \times \{a,b,c\}$. В нем 9 кортежей, из них можно составить $2^{9} - 1 = 511$ различных бинарных непустых отношений со схемой отношения $[XY]$. Эти отношения (точнее, их $Y$-разложения) будут различными интерпретациями $I(\psi)$ формулы $\psi$. Из них удовлетворяют условию $I(\psi) = I(\forall x~ \psi)$ только те, которые содержат единственный $C$-кортеж вида $\bigl[\ast~~S_Y \bigr]$, где $S_Y$ - непустое подмножество множества $\{a,b,c\}$. Количество таких $C$-кортежей будет $2^{3} - 1 = 7$. Тогда получается, что не удовлетворяют условию $I(\psi) = I(\forall x~ \psi)$ 504 примера из 511 возможных. Многовато! Впрочем, для опрокидывания хватило бы и одного примера.
Нетрудно подсчитать данное соотношение для областей истинности $X$ и $Y$ произвольной мощности, допустим, $N$. Тогда опрокидывающих интерпретаций будет $2^{N^2} - 1$, а «хороших» всего лишь $2^{N} - 1$.

[BorisK]

Прошу прощения за оговорку. Последняя фраза читается так:

Тогда всех непустых интерпретаций будет $2^{N^2} - 1$, а «хороших» всего лишь $2^{N} - 1$.