Кванторы и пропозициональные операции

[kernel1983]

Известно, что квантор общности дистрибутивен относительно конъюнкции, а квантор существования дистрибутивен относительно дизъюнкции. Казалось бы, это очевидный факт. Но при попытке доказать это возникает проблема...

Докажем, что $\forall x (P(x) \wedge Q(x)) \simeq \forall x P(x) \wedge \forall x Q(x)$. Пусть $A(x)$ и $B(x)$ - произвольные предикаты, заданные на каком угодно множестве $M$. Пусть высказывание $\forall x A(x) \wedge \forall x B(x)$ истинно. Тогда, по определению конъюнкции, высказывания $\forall x A(x) $ и $\forall x B(x)$ истинны. Следовательно, согласно определению квантора общности, предикаты $A(x)$ и $B(x)$ тождественно истинны. Тогда (почему?) предикат $A(x) \wedge B(x) $ тождественно истинен. Значит, высказывание $\forall x (A(x) \wedge B(x))$ истинно. Почему предикат $A(x) \wedge B(x)$ тождественно истинен? Чтобы доказать его тождественную истинность, нужно вывести из тождественной истинности предиката $A(x)$ (для любого $a \in M$ высказывание $A(a)$ истинно) и тождественной истинности предиката $В(x)$ (для любого $a \in M$ высказывание $B(a)$ истинно) тождественную истинность предиката $A(x) \wedge B(x)$ (для любого $a \in M$ высказывание $A(a) \wedge B(a)$ истинно). Но для этого уже нужно знать, что квантор общности проносится через конъюнкцию. Замкнутый круг?

Аналогичная проблема возникает при доказательстве дистрибутивности квантора существования относительно дизъюнкции.

P.S. Я знаю, что в исчислении высказываний это все доказывается. Но мне нужно доказать сугубо семантически.

[kernel1983]

Ещё немного поясню. Для доказательства теоремы $\forall x (P(x) \wedge Q(x)) \simeq \forall x P(x) \wedge \forall x Q(x)$ требуется знать, что предикат $A(x) \wedge B(x)$ тождественно истинен тогда и только тогда, когда предикат $A(x)$ тождественно истинен и предикат $B(x)$ тождественно истинен. Пусть $\mathcal{A}$ и $\mathcal{B}$ - множества истинности соответствующих предикатов, определённых на множестве $M$. Тогда последнее утверждение эквивалентно такому: $\mathcal{A} \cap \mathcal{B} = M$ тогда и только тогда, когда $\mathcal{A}=M$ и $\mathcal{B}=M$. Но как доказать это, не используя логику предикатов, в том числе и свойство дистрибутивности квантора всеобщности относительно конъюнкции?

[3D Homer]

Подразумевается, что сначала у нас есть возможность проводить математические рассуждения и строить доказательства. Потом мы доказываем определенное свойство формул, которое вы указали: $\forall x (P(x) \wedge Q(x)) \simeq \forall x P(x) \wedge \forall x Q(x)$. При доказательстве того, что тождественная истинность $A(x)$ и тождественная истинность $B(x)$ влекут тождественную истинность $A(x)\land B(x)$ мы используем принципы построения доказательств, как в любой другой области математики, и не используем свойство формул, указанное выше.

[kernel1983]

3D Homer в сообщении #1206951 писал(а):

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

Что это значит?

3D Homer в сообщении #1206951 писал(а):

принципы построения доказательств

Что за принципы такие?

И всё же как доказать эту теорему?

[mihaild]

kernel1983 в сообщении #1207469 писал(а):

И всё же как доказать эту теорему?

Определить, что значит "доказать семантически". Все известные мне доказательства при формализации в конечном итоге записываются в каком-то исчислении.
А без формализации получится что-то типа "конъюнкция коммутативна: действительно, переходим из формул в русский язык, там конъюнкция коммутативна, и переходим обратно".

[arseniiv]

kernel1983 в сообщении #1206918 писал(а):

Почему предикат $A(x) \wedge B(x)$ тождественно истинен? Чтобы доказать его тождественную истинность, нужно вывести из тождественной истинности предиката $A(x)$ (для любого $a \in M$ высказывание $A(a)$ истинно) и тождественной истинности предиката $В(x)$ (для любого $a \in M$ высказывание $B(a)$ истинно) тождественную истинность предиката $A(x) \wedge B(x)$ (для любого $a \in M$ высказывание $A(a) \wedge B(a)$ истинно). Но для этого уже нужно знать, что квантор общности проносится через конъюнкцию. Замкнутый круг?

Не замкнутый. Когда мы определяем значение формулы $\varphi\wedge\psi$, мы используем «не ту же самую» конъюнкцию значений $\varphi,\psi$ (и вообще никаких кванторов: «для любого $a\in M$ $A(a)$ истинно» — это на самом деле конъюнкция всевозможных значений $A(a_1),A(a_2),\ldots;\,a_i\in M$).

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

[george66]

Содержательный смысл в вопросе есть, но популярно ответить трудно. Что значит "доказать семантически"? Видимо, имеется в виду следующее: от формулы $\forall x \varphi(x)$ мы переходим к формуле $\varphi(x)$ со свободной переменной, с ней что-то делаем, а потом опять навешиваем квантор. В формуле со свободной переменной $\varphi(x)$ переменная $x$ обозначает "некоторый элемент, про который ничего не известно". Доказать какое-то свойство для этого элемента можно только в том случае, если свойство верно для всех элементов вообще, за счёт этого мы можем перейти от $\varphi(x)$ обратно к $\forall x \varphi(x)$. И вот что это за элемент такой, каков его смысл? Я правильно понял содержательный вопрос?

[kernel1983]

Вопрос у меня простой. Как доказать, что формула $\forall x (P(x) \wedge Q(x))$ равносильна формуле $\forall x P(x) \wedge \forall x Q(x)$? Больше ничего. Я, например, легко могу доказать законы де Моргана для кванторов и почти все другие равносильности логики предикатов первого порядка. Но тут - ступор!

-- 09.04.2017, 16:24 --

george66 в сообщении #1207743 писал(а):

Что значит "доказать семантически"?

Это значит, доказать, опираясь на определения операций и отношений между высказываниями и предикатами.

[george66]

Допустим, мы доказываем утверждения о целых числах
$(3+1)^2=3^2+2\cdot 3 + 1$
$(4+1)^2=4^2+2\cdot 4 +1$
и так далее. Можно это записать одной формулой
$(x+1)^2=x^2+2\cdot x+1$
Обозначим эту формулу $\varphi(x)$.
Здесь мы добавили к кольцу $\mathfrac{Z}$ новый элемент $x$ и получили кольцо многочленов $\mathfrac{Z}[x]$, в котором и записано последнее равенство. Поскольку про $x$ "ничего не известно", формула вида $\varphi(x)$ может быть верна только если она верна вообще для чего угодно, поэтому из $\varphi(x)$ можно вывести $\varphi(3)$, $\varphi(4)$ и так далее. Вот так же можно понимать свободные переменные и в общем случае. К исходной области (уже не кольцу, а более сложной конструкции) добавляются новые элементы $x,y,z\ldots$ "свободным образом". Формулу $\varphi(x)$ можно доказать если и только если можно доказать $\forall x\varphi(x)$, потому что "$x$ элемент общего вида, про который ничего не известно".

-- 09.04.2017, 16:56 --

Попробуем по-другому. Пусть истинно $\forall x P(x)\wedge \forall x Q(x)$. Тогда истинно $\forall x P(x)$ и $\forall x Q(x)$. Возьмём какой угодно элемент $y$. Истинно $P(y)$ и $Q(y)$. Поэтому истинно $P(y)\wedge Q(y)$. Поскольку $y$ любой, истинно $\forall x (P(x)\wedge Q(x))$. Можно это рассуждение записать формально и получится вывод в исчислении предикатов.

[arseniiv]

kernel1983 в сообщении #1207907 писал(а):

Вопрос у меня простой. Как доказать, что формула $\forall x (P(x) \wedge Q(x))$ равносильна формуле $\forall x P(x) \wedge \forall x Q(x)$? Больше ничего. Я, например, легко могу доказать законы де Моргана для кванторов и почти все другие равносильности логики предикатов первого порядка. Но тут - ступор!

Значит, вы ещё не совсем понимаете определение значения формулы в интерпретации. Попробуйте сделать это формально без всяких слов. Пусть значение формулы $\varphi$ на оценке переменных $u$ обозначается $I(u, \varphi)$ (для замкнутой формулы оно, конечно же, не зависит от оценки, но тут это всё равно не понадобится), и пусть конъюнкция логических значений $v_1,v_2\in\{0,1\}$ обозначается $v_1\wedge v_2$ — перепутать её с конъюнкцией формул всё же не получится — и конъюнкция значений $v_i$ для всех $i\in A$ обозначается $\bigwedge\limits_{i\in A} v_i$. Больше ничего не понадобится.

Эквивалентность формул $\varphi,\psi$: для любой оценки $u$, $I(u, \varphi) = I(u, \psi)$. Осталось найти по отдельности $I(u, \forall x(p\wedge q)$ и $I(u, \forall xp\wedge\forall xq$.

[У меня возникает соблазн обругать книгу Игошина, которая, боюсь, всё-таки и виновата.]

[george66]

Проблема есть, но чертовски трудно объяснить. Теоретико-множественная семантика ничего не "доказывает", она просто объясняет смысл символов $\forall$ и $\exists$. Можно дать вывод в исчислении предикатов. Но чтобы содержательно объяснить смысл кванторных правил, надо вдаваться в довольно глубокие глубины (типа "квантор всеобщности сопряжён справа к подстановке, поэтому сохраняет пересечения"). Поэтому лучше научитесь доказывать формально в исчислении предикатов, а уж потом семантика.

[arseniiv]

george66 в сообщении #1208048 писал(а):

Можно дать вывод в исчислении предикатов.

В таком случае он тоже ничего не доказывает, ибо обычно он вводится на основе уже имеющегося понятия общезначимости так, чтобы аксиомы были общезначимыми, а правила вывода порождали по общезначимым посылкам только общезначимые заключения. Конечно, можно в обратную сторону, но это, по крайней мере, вроде бы не то, чего хочется ТС.

george66 в сообщении #1208048 писал(а):

Но чтобы содержательно объяснить смысл кванторных правил, надо вдаваться в довольно глубокие глубины (типа "квантор всеобщности сопряжён справа к подстановке, поэтому сохраняет пересечения").

Может быть, на теоркатегорном языке это более ёмко (не знаю), но это не значит, что «содержательно объяснить» нельзя традиционным способом. (Я не против категорий, но будет ли это понятно спрашивающему?)

george66 в сообщении #1208048 писал(а):

Проблема есть, но чертовски трудно объяснить.

Тут при желании можно найти «проблему метатеории» — мы описываем наш исследуемый логический аппарат средствами (как правило, наивной) метатеории и опираемся на её свойства. Но тут уж не важно, теоркатегорно или нет, эту часть в любом случае придётся явно признать и явно понять, что ex nihilo nihil fit.

[george66]

arseniiv в сообщении #1208060 писал(а):

george66 в сообщении #1208048 писал(а):

Можно дать вывод в исчислении предикатов.

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

Нет, вывод даётся сам по себе из примерно таких соображений, как я попытался объяснить выше на примере с целыми числами и многочленами. А связь с общезначимостью потом доказывается в качестве довольно трудной теоремы (о полноте). Даже для исчисления высказываний это не так просто (доказать, что выводимо в точности то, что верно во всех булевских таблицах истинности). И вот содержательные соображения можно вполне строго изложить, но трудно это сделать популярно. Например, для примера выше с многочленами: почему из равенства многочленов
$(x+1)^2=x^2+2\cdot x+1$
следует
$(3+1)^2=3^2+2\cdot 3+1$ ?
А потому что для любого целого числа (в данном случае 3) есть "гомоморфизм подстановки" из $\mathfrac{Z}[x]$ в $\mathfrac{Z}$ (который в многочлен подставляет 3 вместо $x$, получается целое число).

[arseniiv]

george66 в сообщении #1208074 писал(а):

Нет, вывод даётся сам по себе из примерно таких соображений, как я попытался объяснить выше на примере с целыми числами и многочленами.

Можно так, а можно сразу связать.

george66 в сообщении #1208074 писал(а):

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

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

george66 в сообщении #1208074 писал(а):

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

А кто предлагал делать это популярно?

-- Пн апр 10, 2017 02:00:39 --

В общем, пока ТС не отпишется, можно, разумеется, ещё о многом поговорить… но для этого наверняка полезнее открыть $n$ отдельных тем, чтобы отделить разные ветки обсуждения.

[george66]

Могу объяснить через соответствие Галуа! Пусть даны два множества $X$ и $Y$, а также функция между ними $f\colon X\to Y$
Возьмём два упорядоченных множества $P(X)$ (множество подмножеств $X$) и $P(Y)$ (множество подмножеств $Y$).
Есть монотонное отображение $f^{-1}\colon P(Y)\to P(X)$ (взятие прообраза), которое по каждому подмножеству $Y$ выдаёт его прообраз относительно $f$.
Есть отображение в обратную сторону $\forall_f\colon P(X)\to P(Y)$, которое по каждому подмножеству $A\subseteq X$ выдаёт его "малый образ" (множество таких точек $Y$, прообразы которых целиком лежат в $A$)
$\forall_f(A)=\{y\in Y\mid f^{-1}\{y\}\subseteq A\}=\{y\in Y\mid\forall x\in X(f(x)=y\Rightarrow x\in A)\}$
Отображения $f^{-1}$ и $\forall_f$ определяют соответствие Галуа в следующем смысле
$f^{-1}(B)\subseteq A$ если и только если $B\subseteq \forall_f(A)$ для любых подмножеств $A\subseteq X$ и $B\subseteq Y$
Из этого сравнительно легко вывести, что отображение $\forall_f$ сохраняет пересечения. Честное слово, именно в этом суть дела и именно это отражают правила вывода для квантора $\forall$ в исчислении предикатов. "Семантически" легче объяснить нельзя.