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

[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$. Но она, кажется, легко распознается по контексту.