Бурбаки, кванторные теории

[FeelUs]

Читаю первый том Бурбаков, Теория множеств, дошёл до критерия C34:
$(\forall x)(\forall y)R\iff (\forall y)(\forall x)R$
$(\exists x)(\exists y)R\iff (\exists y)(\exists x)R$
$(\exists x)(\forall y)R\Rightarrow (\forall y)(\exists x)R$
Далее идёт комментарий, что $ (\forall y)(\exists x)R\Rightarrow (\exists x)(\forall y)R$ - неверно. С семантической точки зрения я с этим полностью согласен, но с синтаксической точки зрения я его могу доказать:
По C30 ( $(\forall x)R\{x\} \Rightarrow R\{T\}$ ) : $(\forall y)(\exists x)R\Rightarrow (\exists x)R$ .
По C27 ( $R \vdash (\forall x)R$ ) : $R \Rightarrow (\forall y)R$ .
По C31 ( $R \Rightarrow S \vdash (\exists x)R \Rightarrow (\exists x)S$ ) : $(\exists x)R \Rightarrow (\exists x)(\forall y)R$ .
И, наконец по C6 ( $A\Rightarrow B; B\Rightarrow C \vdash A\Rightarrow C$ ) : $ (\forall y)(\exists x)R\Rightarrow (\exists x)(\forall y)R$ .
Пояснения типа "x - не константа" я опустил, потому что давайте рассматривать теорию без констант.
Помогите найти ошибку

[warlock66613]

FeelUs в сообщении #1580734 писал(а):

По C30 ( $(\forall x)R\{x\} \Rightarrow R\{T\}$ ) : $(\forall y)(\exists x)R\Rightarrow (\exists x)R$ .

Вы понимаете что фигурные скобки слева не просто так, понимаете в чём разница между $R\{x\}$ и $R\{T\}$?

[FeelUs]

warlock66613 в сообщении #1580754 писал(а):

FeelUs в сообщении #1580734 писал(а):

По C30 ( $(\forall x)R\{x\} \Rightarrow R\{T\}$ ) : $(\forall y)(\exists x)R\Rightarrow (\exists x)R$ .

Вы понимаете что фигурные скобки слева не просто так, понимаете в чём разница между $R\{x\}$ и $R\{T\}$?

Понимаю. Бурбаки ещё это пишут так $(\forall x)R \Rightarrow (T|x)R$, где $(T|x)R$ означает найти в $R$ все $x$ и заменить их на произвольный (один и тот же) терм $T$, в качестве которого можно взять например букву $x$

[mihaild]

FeelUs в сообщении #1580734 писал(а):

По C27 ( $R \vdash (\forall x)R$ ) : $R \Rightarrow (\forall y)R$ .

А вот это как получено? Как из утверждения вида "если $a$ теорема, то $b$ теорема" получается "есть теорема $a \Rightarrow b$"?

[FeelUs]

mihaild в сообщении #1580769 писал(а):

FeelUs в сообщении #1580734 писал(а):

По C27 ( $R \vdash (\forall x)R$ ) : $R \Rightarrow (\forall y)R$ .

А вот это как получено? Как из утверждения вида "если $a$ теорема, то $b$ теорема" получается "есть теорема $a \Rightarrow b$"?

А это C14, его можно так сформулировать $A\Rightarrow B1; A\Rightarrow(B1\Rightarrow B) \vdash A\Rightarrow B$, и дальше применяется оно так: присоединим к имеющейся теории $A$, и получим новую теорию. В новой теории докажем (каким то образом, но всё равно так или иначе через силлогизм $X; X\Rightarrow Y \vdash Y$) $B1$, потом $B2$, ... и т.д. до $B$ .
И значит в исходной теории $A \Rightarrow A$ верно, $C \vdash A\Rightarrow C$ применим там где надо. И дальше по цепочке $A\Rightarrow B1$ верно, потом $A\Rightarrow B2$ верно, и т.д. $A\Rightarrow B$ верно (что и требуется).

[mihaild]

FeelUs в сообщении #1580797 писал(а):

А это C14

С14 для логических теорий. Для кванторных теорий в теореме о дедукции нужно потребовать, чтобы в выводе не было применения правила обобщения к посылке (а лучше чтобы посылка вообще была замкнутой).

[FeelUs]

mihaild в сообщении #1580810 писал(а):

FeelUs в сообщении #1580797 писал(а):

А это C14

С14 для логических теорий. Для кванторных теорий в теореме о дедукции нужно потребовать, чтобы в выводе не было применения правила обобщения к посылке (а лучше чтобы посылка вообще была замкнутой).

Но в кванторных теориях ведь верно всё, что верно для логических теорий, а именно схемы аксиом S1, S2, S3, S4 и силлогизм C1. А C14 в конечном итоге сводится именно к ним.
А что такое "правило обобщения к посылке"?
АААА, я понял! В доказательстве C27 используется C3 ($R\{x\} \vdash R\{T\}$), а C14 не рассчитан на это!

-- 08.02.2023, 21:07 --

Но почему тогда С31 ($R\{x\}\Rightarrow S\{x\} \vdash (\forall x)R\{x\}\Rightarrow (\forall x)S\{x\}$) они доказывают так:
Присоединим $(\forall x)R\{x\}$.
Тогда $R\{x\}$ (видимо по C30),
а следовательно и $S\{x\}$ (это по C1),
а следовательно и $(\forall x)S\{x\}$ (видимо по C27, которое использует C3).
Это значит что $(\forall x)R\{x\}\Rightarrow (\forall x)S\{x\}$ есть теорема (видимо по C14).

Почему здесь C14 работает?

[mihaild]

FeelUs в сообщении #1580822 писал(а):

А что такое "правило обобщения к посылке"

Правило обобщения - это как раз $\psi \vdash \forall x \psi$. В теореме о дедукции "если $\Gamma, A \vdash B$ то $\Gamma \vdash A \rightarrow B$" формула $A$ называется посылкой. И в условии теоремы о дедукции нужно написать, что в выводе $B$ из $\Gamma, A$ не применяется правило обобщения по свободным в $A$ переменным (это формулируется несколькими способами, если постараться, то можно запретить добавлять кванторы только на некоторых шагах, но как правило это не очень полезно).

FeelUs в сообщении #1580822 писал(а):

Почему здесь C14 работает?

Как раз потому что тут правило обобщения к $(\forall x)R$ не применяется.