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

[epros]

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

Если консеквент представлен формулой $\forall x~(x=0)$, то тогда консеквентом является формула $\forall x~\varphi$, а не какая-то $\psi$, как Вы утверждаете.

Здесь $\forall x~\varphi$ и есть $\psi$ - формула без свободных вхождений $x$.

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

Если же имеется в виду формула $\forall x~(x)=0$

А это вообще непонятно что. Какой смысл заключать в скобки переменную?

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

Других вариантов расстановки скобок я не вижу.

А их и нет, так что экономия скобок оправдана.

[BorisK]

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

Здесь $\forall x~\varphi$ и есть $\psi$ - формула без свободных вхождений $x$.

Я очччень Вас прошу: давайте в полемике обойдемся без двусмысленностей. Если Вы предлагаете формулу $\psi$, то это может быть не только $\forall x~\varphi$, но и какая-то другая формула, которая здесь совершенно не нужна.

Цитата:

А это вообще непонятно что. Какой смысл заключать в скобки переменную?

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

[epros]

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

Я очччень Вас прошу: давайте в полемике обойдемся без двусмысленностей. Если Вы предлагаете формулу $\psi$, то это может быть не только $\forall x~\varphi$, но и какая-то другая формула, которая здесь совершенно не нужна.

У меня нет ни одной двусмысленности. Я указал, какие правила вывода и аксиомы применяются к формуле вида $\varphi \to \psi$, где $\psi$ не имеет свободных вхождений $x$. Это - общий случай. И я объяснил, как это всё применяется в частном случае, когда в качестве $\varphi$ подставляется $x=0$, а вместо $\psi$ подставляется $\forall x~x=0$.

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

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

Между прочим, я не сказал, что это ошибка. Я сказал, что это непонятно зачем.

[BorisK]

Должен признаться, что мой прогноз оказался ложным: я не смог пока что доказать, что формула $\bigl(\varphi \to \psi\bigr) \to \bigl(\varphi \to (\forall x~\psi)\bigr)$ является тавтологией при условии, что переменная $x$ не входит свободно в $\varphi $. И опровергнуть, кстати, тоже не получилось.
Зато ясно, что формула $\varphi \to \forall x~\varphi$ не тавтология, и в подтверждение этому найдено много примеров.
В то же время можно доказать, что формула $\varphi \to \forall x~\varphi$ при условии, что переменная $x$ не входит свободно в $\varphi$, - тавтология. Но этого условия я не встречал в формулировках правила обобщения типа $\frac {\varphi}{\forall x~\varphi}$, по крайней мере, в книгах Мендельсона его точно нет.
Все же я убежден, что мы с epros обсуждали примеры к формуле $\varphi \to \forall x~\varphi$, но никак не к формуле $\bigl(\varphi \to \psi\bigr) \to \bigl(\varphi \to (\forall x~\psi)\bigr)$. Здесь, по-моему, пока не все ясно.
Если что-то придумаю интересное в этом плане, то обещаю поведать об этом на форуме. А, может быть, кто-то из участников этой дискуссии найдет решение проблемы. Буду рад.

[dgwuqtj]

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

В то же время можно доказать, что формула $\varphi \to \forall x~\varphi$ при условии, что переменная $x$ не входит свободно в $\varphi$, - тавтология. Но этого условия я не встречал в формулировках правила обобщения типа $\frac {\varphi}{\forall x~\varphi}$, по крайней мере, в книгах Мендельсона его точно нет.

Это потому что импликации и правила вывода — разные вещи. Они и интерпретируются по-разному для обычных теоретико-множественных моделей. Импликация, как и любая формула, просто задаёт предикат. А правило вывода говорит, что если в числителе тождественно истинные предикаты, то и в знаменателе тождественная истина.

[epros]

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

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

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

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

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

Зато ясно, что формула $\varphi \to \forall x~\varphi$ не тавтология, и в подтверждение этому найдено много примеров.

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

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

В то же время можно доказать, что формула $\varphi \to \forall x~\varphi$ при условии, что переменная $x$ не входит свободно в $\varphi$, - тавтология. Но этого условия я не встречал в формулировках правила обобщения типа $\frac {\varphi}{\forall x~\varphi}$, по крайней мере, в книгах Мендельсона его точно нет.

Потому что обобщать и имеет смысл тогда, когда свободная переменная в формуле есть. Например, в арифметике Пеано есть одна из аксиом, определяющих умножение натуральных чисел: $x \times 0 = 0$. Её можно записывать без квантора всеобщности на переменной $x$, потому что по правилу обобщения он всегда может быть проставлен.

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

Все же я убежден, что мы с epros обсуждали примеры к формуле $\varphi \to \forall x~\varphi$, но никак не к формуле $\bigl(\varphi \to \psi\bigr) \to \bigl(\varphi \to (\forall x~\psi)\bigr)$. Здесь, по-моему, пока не все ясно.

Вы спрашивайте. Выше я написал, что мой пример был про подстановку в формулу $\varphi \to \forall x~\varphi$ на место метапеременной $\varphi$ формулы $x=0$, но вместо этого можно применить подстановку эквивалентной формулы $0=0 \to x=0$. Это понятно?

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

[BorisK]

Выполняю обещанное.
Здесь представлю лишь схему доказательства того, что формула $\bigl(\varphi \to \psi\bigr) \to \bigl(\varphi \to (\forall x~\psi)\bigr)$ является тавтологией при условии, что в $\varphi$ нет свободных вхождений переменной $x$.
Если какой-либо пункт предлагаемой схемы кому-то покажется сомнительным, то постараюсь рассмотреть его более подробно. Доказательство основано на интерпретации с использованием АК (алгебры кортежей). Чтобы мне не повторяться, предлагаю собеседникам воспользоваться краткой сводкой определений и теорем АК, которые выложены в Интернете. Можно считать, что АК является интерпретацией логики первого порядка с той лишь разницей, что в ней определены операции и проверки включения для $n$-местных отношений, а вместо несущего множества $D^n$ можно использовать несущее множество (универсум) $D_1 \times D_2, \times \dots, \times D_n$, в котором $D_i$ могут быть разными множествами.
Для краткости обозначим $BF$ (формула Бернайса) формулу $\bigl(\varphi \to \psi\bigr) \to \bigl(\varphi \to (\forall x~\psi)\bigr)$ при условии, что в $\varphi$ нет свободных вхождений переменной $x$.
Обозначим $I(F)$ интерпретацию логической формулы $F$ в структурах АК.
Схема доказательства
P1. Для доказательства того, что $BF$ тавтология, достаточно доказать, что в подформуле $\bigl(\varphi \to \psi\bigr)$ не существует выполняющей подстановки, которая не является выполняющей подстановкой в подформуле $\bigl(\varphi \to (\forall x~\psi)\bigr)$.
P2. Поскольку в $BF$ только одна переменная с квантором, то для ее обоснования достаточно рассмотреть бинарные отношения. Будем считать, что это АК-объекты со схемой отношения $[XY]$. Атрибут $X$ соответствует переменной $x$ в $BF$. Тогда интерпретациями формул $\varphi$ и $\psi$ будут АК-объекты $I(\varphi)[XY]$ и $I(\psi)[XY]$ или просто $I(\varphi)$ и $I(\psi)$ с учетом того, что схемы отношений у них одинаковы. Тогда, если не оговорено противное, будем считать, что все упоминаемые далее интерпретации заданы в схеме отношения $[XY]$.
P3. Подформула $\bigl(\varphi \to \psi\bigr)$ тавтология, если выполняется соотношение $I(\varphi) \subseteq I(\psi)$ (Теорема 33, которая является интерпретацией одного важного частного случая теоремы дедукции).
P4. Рассмотрим условия, при которых выполняется $I(\varphi) \subseteq I(\psi)$. Формулы, у которых нет свободных вхождений переменной $x$, в АК представлены $C$-системами, у которых в атрибуте $X$ содержатся только полные фиктивные компоненты ($\ast$). Это утверждение основано на Теоремах 31, 32 и на операции добавления фиктивного атрибута. В силу Теоремы 5 (пункт 2) такую $C$-систему в бинарных отношениях можно выразить как $C$-кортеж $[\ast~~A]$, где $A\subset Y$. Тогда, чтобы выполнялось соотношение $I(\varphi) \subseteq I(\psi)$, необходимо и достаточно, чтобы в $I(\psi)$ присутствовал $C$-кортеж $[\ast~~B]$, такой, что $A \subseteq B$ (Теорема 1).
P5. Поскольку в $I(\psi)$ содержится $C$-кортеж $[\ast~~B]$, то он остается неизменным и в интерпретации формулы $\forall x~\psi$ (символ $\ast$ в данном случае - это множество всех значений атрибута $X$, что соответствует области определения переменной $x$). Отсюда ясно, что любая выполняющая подстановка подформулы $\bigl(\varphi \to \psi\bigr)$ является выполняющей подстановкой подформулы $\bigl(\varphi \to (\forall x~\psi)\bigr)$. Тем самым доказано, что $BF$ тавтология.

[epros]

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

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

Предлагаю Вам подставить вместо $\varphi$ формулу $0=0$ (как видите, в ней нет свободных вхождений переменной $x$), а вместо $\psi$ подставить формулу $x=0$. И попробуйте проделать Ваши рассуждения для получившейся формулы. Это я к тому, что эта формула в нормальной арифметике будет очевидно ложной, не знаю, как Вы будете её доказывать.

[BorisK]

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

Предлагаю Вам подставить вместо $\varphi$ формулу $0=0$ (как видите, в ней нет свободных вхождений переменной $x$), а вместо $\psi$ подставить формулу $x=0$. И попробуйте проделать Ваши рассуждения для получившейся формулы. Это я к тому, что эта формула в нормальной арифметике будет очевидно ложной, не знаю, как Вы будете её доказывать.

Уточняю: «нет свободных вхождений переменной $x$» означает, что в формуле либо переменная $x$ находится в зоне действия квантора, либо ее нет вообще.
Вы же предлагаете выражение для $\varphi$, в котором переменная $x$ присутствует неявно. В языке первого порядка выражение $0=0$ означает двуместный предикат (обозначим его $E(x,y)$), единственной выполняющей подстановкой которого является кортеж $(0,0)$ при условии, что области определения переменных $x$ и $y$ - числа с нулем.

-- 15.07.2025, 18:42 --

[Mikhail_K]

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

Предлагаю Вам подставить вместо $\varphi$ формулу $0=0$ (как видите, в ней нет свободных вхождений переменной $x$)

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

Уточняю: «нет свободных вхождений переменной $x$» означает, что в формуле либо переменная $x$ находится в зоне действия квантора, либо ее нет вообще.
Вы же предлагаете выражение для $\varphi$, в котором переменная $x$ присутствует неявно. В языке первого порядка выражение $0=0$ означает двуместный предикат (обозначим его $E(x,y)$), единственной выполняющей подстановкой которого является кортеж $(0,0)$ при условии, что области определения переменных $x$ и $y$ - числа с нулем.

Итак, оказывается, формула $0=0$ содержит-таки свободную переменную $x$, только "неявно"!
Это очень оригинальная мысль.

Кстати, я правильно понял, что Вы не видите разницы между записями $0=0$ и $x=y=0$?

[BorisK]

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

Итак, оказывается, формула $0=0$ содержит-таки свободную переменную $x$, только "неявно"!
Это очень оригинальная мысль.

Речь здесь идет о языке первого порядка и его возможных интерпретациях. Формула $0=0$ не есть выражение на языке первого порядка. Вот когда Вы ее выразите на этом языке, тогда и будет, о чем спорить.

[Mikhail_K]

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

Формула $0=0$ не есть выражение на языке первого порядка

Это очень печально :(

[BorisK]

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

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

Формула $0=0$ не есть выражение на языке первого порядка

Это очень печально :(

Ладно, предлагаю еще одно уточнение: исчисление первого порядка с равенством и его аксиомы здесь не используются. Без него тоже можно получить интересные результаты. И есть что пообсуждать.

[dgwuqtj]

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

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

Тогда подставьте $\varphi = (\forall y\enskip P(y)) \vee \neg (\forall y\enskip P(y))$ и $\psi = Q(x)$, где $P$ и $Q$ предикатные символы от одной переменной.

[BorisK]

Опровержение я нашел в бинарных отношениях. Завтра его здесь покажу. И, выходит, с доказательством я поторопился. Спасибо всем!