Математическая логика (по Мендельсону)

[Виктор Викторов]

«Пусть $x_{i_1}, \cdots, x_{i_k}$ — переменные и $\mathscr A$ —формула. Не обращая внимания на то, являются ли эти переменные свободными в $\mathscr A$ и существу ли в $\mathscr A$ другие свободные переменные, мы будем иногда применять запись $\mathscr A(x_{i_1}, \cdots, x_{i_k})$ для обозначения формулы $\mathscr A$ с тем, чтобы затем через $\mathscr A(t_{i_1}, \cdots, t_{i_k})$ обозначать результат подстановки термов $t_{i_1}, \cdots, t_{i_k}$ соответственно вместо свободных вхождений в $\mathscr A$ (если таковые имеются!) переменных $x_{i_1}, \cdots, x_{i_k}$ .» Страница 56.
Все было бы хорошо, если бы меня не тревожил один вопрос. Пусть у нас есть формула $\mathscr A(x, y)$. Обязана ли вообще быть в ней переменная $y$ (связанная или свободная всё равно)? Вопрос возник на странице 87 «(c) Пусть $\mathscr A(y, y)$ есть $y = z$ и $\mathscr A(y, x)$ есть $x=z$.» Я понимаю, что в формуле $x = z$ два терма $x$ и $z$ и я не обязан прописывать в $\mathscr A(y, x)$ терм $z$, но в $x = z$ отсутствует $y$! Также я понимаю, что $\mathscr A(y, y)$ написана так из-за того, что это частный случай формулы с двумя переменными (и автор хочет это подчеркнуть), но я не могу понять, когда я вижу на стр. 87 $\mathscr A(x, y)$ и $\mathscr A(y, x)$ одновременно. По тексту на странице 56 порядок в такой записи не имеет значения!

[Xaositect]

Виктор Викторов в сообщении #467398 писал(а):

Обязана ли вообще быть в ней переменная $y$ (связанная или свободная всё равно)?

Обычно не требуют.

[Виктор Викторов]

Следовательно $\mathscr A(y, x)$ есть $x=z$ нужно понимать, как $\mathscr A(y, x, z)$? А что означает изменение порядка в списке переменных?

[Xaositect]

Эта запись просто означает, что с какими-то переменными мы будем в ближайшее время работать. В формуле могут быть и другие переменные, а тех, что стоят в скобках, может не быть. Это просто для того, чтобы не писать громоздкие выражения с подстановками. $x=z$ можно обозначить и $\mathscr A(x, y, z)$, и $\mathscr A(y, x)$, и $\mathscr A(t)$

[Виктор Викторов]

$\mathscr A(x_{i_1}, \cdots, x_{i_k})$ -- формула $\mathscr A$ где $x_{i_1}, \cdots, x_{i_k}$ свободные переменные. Причем:
1. Возможно не все.
2. Возможно, что некоторые из них отсутствуют.
3. Переменную можно «разделить» $\mathscr A(x, x)$ -- это значит, что первое $x$ в нескольких местах формулы и второе $x$ в других местах той же формулы.
Теперь внимательно рассмотрим аксиому «(7) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$ (подстановочность равенства)» -- суть ясна вместо любых вхождений $x$ можно подставить $y$.
А можно ли эту аксиому записать так: «(7’) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(y, x))$? Как сейчас станет ясно это не мелкие придирки, а проблема. Дальше идет:
«Предложение 2.24. Во всякой теории первого порядка с равенством
(a) $\vdash t=t$ для любого терма $t$;
(b) $\vdash x=y\to y=x$;
(c) $\vdash x=y\to (y=z\to x=z)$.»

Рассмотрим часть доказательства (c): «Пусть $\mathscr A(y, y)$ есть $y = z$ [действительно в формуле $\mathscr A$ мы дважды выделили свободную переменную $y$, при этом один раз она присутствует, а второй отсутствует, а $z$ не выделили – имеем право] $\mathscr A(y, x)$ есть $x = z$ [все замечания аналогичны замечаниям в предыдущих квадратных скобках, но только надо добавить, что в формуле $\mathscr A(y, x)$ явно важен порядок записи переменных!]. Тогда, в силу (7) с взаимной заменой $x$ и $y$, $(y=x)\to (y=z\to x=z)$».

А теперь, оставив все рассуждения в том же виде, заменим последнее $z$ на $w$. Итак,
Пусть $\mathscr A(y, y)$ есть $y = z$ и $\mathscr A(y, x)$ есть $x = w$. Тогда, в силу (7) с взаимной заменой $x$ и $y$, $(y=x)\to (y=z\to x=w)$.
Но речь-то идет все-таки о самой обычной транзитивности! И мой вариант – полная чушь. Но как это показать и заодно увериться в правильности доказательства Мендельсона?

[Виктор Викторов]

Мне кажется, что проблема в обозначениях. По смыслу аксиомы (7) из того, что $y=x$ и $y = z$ следует, что в формуле $y = z$ можно заменить $y$ на $x$ и получить $x=z$. Но обозначения столь многозначны, что, если их использовать, то и моя «интерпретация» также вполне возможна, хотя и абсурдна.

[beroal]

Виктор Викторов в сообщении #467451 писал(а):

А теперь, оставив все рассуждения в том же виде, заменим последнее $z$ на $w$.

Очевидно, что нельзя заменять последнее $z$ на $w$. Тут надо формально определить, что означает запись «формула, затем в скобках термы». Я таких формальных определений не встречал. Обычно дают определения через подстановку, например, $\mathscr A[v:=t]$, то есть в формуле $\mathscr A$ вместо переменной $v$ подставить терм $t$.

Я бы определил так. В обозначении $\mathscr A(\ldots)$ $\mathscr A$ обозначает не формулу, а контекст. Мы определяем контекст так же, как формулу, с дополнительным продукционным правилом, что в качестве терма можно брать дыру (hole) с некоторым номером. $\mathscr A(t_0,t_1,\ldots)$ обозначает, что вместо 0-й дыры подставляем терм $t_0$, вместо 1-й дыры подставляем терм $t_1$ и так далее.

В вашем примере, $\mathscr A$ есть $hole_1=z$. И очевидно, что $z$ никуда не денется, не превратиться ни в $w$, ни во что другое.

-- Tue Jul 12, 2011 12:50:35 --

P.S. Хотя принципиальной разницы между контекстами и формулами нет. То есть вместо контекста можно взять формулу, а дыры считать специальными переменными. Но понятие контекста действительно существует, это не я выдумал.

[Виктор Викторов]

beroal в сообщении #467548 писал(а):

Очевидно, что нельзя заменять последнее $z$ на $w$.

Конечно, нельзя. Но обратите внимание на свой собственный комментарий. Для того, чтобы опровергнуть мою "интерпретацию", Вам понадобились дополнительные определения. А у Мендельсона их нет.

-- Вт июл 12, 2011 08:37:45 --

И ещё один момент:

beroal в сообщении #467548 писал(а):

Я бы определил так. В обозначении $\mathscr A(\ldots)$ $\mathscr A$ обозначает не формулу, а контекст. Мы определяем контекст так же, как формулу, с дополнительным продукционным правилом, что в качестве терма можно брать дыру (hole) с некоторым номером. $\mathscr A(t_0,t_1,\ldots)$ обозначает, что вместо 0-й дыры подставляем терм $t_0$, вместо 1-й дыры подставляем терм $t_1$ и так далее.

Мендельсон разрешает иметь одну переменную в списке несколько раз. Так что «брать дыру (hole) с некоторым номером» будет весьма и весьма хлопотно.

[Виктор Викторов]

«Часто встречаются теории первого порядка, в которых равенство $=$ может быть определено. Это значит, что в такой теории К имеется формула $\mathscr E(x, y)$, для которой, если $\mathscr E(t, s)$ обозначить через $t = s$, формулы (6), (7) выводимы в К.» Страница 90.
Напоминаю, как выглядят (6) и (7).
(6) $\forall x_1(x_1 = x_1)$ (рефлексивность равенства);
(7) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$ (подстановочность равенства).

Переводчик пропустил «свободные переменные». Эта фраза должна выглядеть так: «Часто встречаются теории первого порядка, в которых равенство $=$ может быть определено. Это значит, что в такой теории К имеется формула $\mathscr E(x, y)$ со свободными переменными $x$ и $y$, для которой, если $\mathscr E(t, s)$ обозначить через $t = s$, формулы (6), (7) выводимы в К.»

Мне бы хотелось понять смысл переобозначения $x$ в $s$ и $y$ в $t$. Чтобы изменилось, если бы было написано: ««Часто встречаются теории первого порядка, в которых равенство $=$ может быть определено. Это значит, что в такой теории К имеется формула $\mathscr E(x, y)$ со свободными переменными $x$ и $y$, для которой, если $\mathscr E(x, y)$ обозначить через $x = y$, формулы (6), (7) выводимы в К.»

Теперь рассмотрим интерпретацию с областью $\mathbb{N}$. И определим, что $t = s$ тогда и только тогда, когда $t$ и $s$ одно и тоже натуральное число. Аксиомы (6) и (7) выполняются. Тогда высказывание $4=4$ истинно, а высказывание $4=5$ ложно. А теперь вопрос: а что такое $4=3+1$? Что такое $3+1$? Такого элемента в $\mathbb{N}$ не существует. Итак, $3+1$ есть терм – предметная константа и $s^*(3+1)=4$ в данной интерпретации. Правильно я это понимаю? А чем является число $4$ в формуле $4=3+1$? Это тоже терм со значением $s^*(4)=4$?

[Xaositect]

Виктор Викторов в сообщении #468983 писал(а):

«Часто встречаются теории первого порядка, в которых равенство $=$ может быть определено. Это значит, что в такой теории К имеется формула $\mathscr E(x, y)$, для которой, если $\mathscr E(t, s)$ обозначить через $t = s$, формулы (6), (7) выводимы в К.» Страница 90.
Напоминаю, как выглядят (6) и (7).
(6) $\forall x_1(x_1 = x_1)$ (рефлексивность равенства);
(7) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$ (подстановочность равенства).

Переводчик пропустил «свободные переменные». Эта фраза должна выглядеть так: «Часто встречаются теории первого порядка, в которых равенство $=$ может быть определено. Это значит, что в такой теории К имеется формула $\mathscr E(x, y)$ со свободными переменными $x$ и $y$, для которой, если $\mathscr E(t, s)$ обозначить через $t = s$, формулы (6), (7) выводимы в К.»

Мне бы хотелось понять смысл переобозначения $x$ в $s$ и $y$ в $t$. Чтобы изменилось, если бы было написано: ««Часто встречаются теории первого порядка, в которых равенство $=$ может быть определено. Это значит, что в такой теории К имеется формула $\mathscr E(x, y)$ со свободными переменными $x$ и $y$, для которой, если $\mathscr E(x, y)$ обозначить через $x = y$, формулы (6), (7) выводимы в К.»

Обычно $x$ и $y$ - это метасимволы для переменных, а $s$ и $t$ - для термов. Т.е. первое $\mathscr{E}(x, y)$ означает некоторую фиксированную формулу от фиксированных переменных $x$ и $y$, а $\mathscr{E}(s,t)$ - подстановку в эту формулу произвольных термов.

Цитата:

Теперь рассмотрим интерпретацию с областью $\mathbb{N}$. И определим, что $t = s$ тогда и только тогда, когда $t$ и $s$ одно и тоже натуральное число. Аксиомы (6) и (7) выполняются. Тогда высказывание $4=4$ истинно, а высказывание $4=5$ ложно. А теперь вопрос: а что такое $4=3+1$? Что такое $3+1$? Такого элемента в $\mathbb{N}$ не существует. Итак, $3+1$ есть терм – предметная константа и $s^*(3+1)=4$ в данной интерпретации. Правильно я это понимаю? А чем является число $4$ в формуле $4=3+1$? Это тоже терм со значением $s^*(4)=4$?

Да, это термы. $3 + 1$ - это не предметная константа, это сложный терм. В интерпретации ему приписывается значение на основе оценок констант $3$ и $1$ и бинарного функционального символа $+$. А $4$ - это предметная константа (и, следовательно, тоже является термом).

[Виктор Викторов]

Xaositect в сообщении #469182 писал(а):

Да, это термы. $3 + 1$ - это не предметная константа, это сложный терм. В интерпретации ему приписывается значение на основе оценок констант $3$ и $1$ и бинарного функционального символа $+$. А $4$ - это предметная константа (и, следовательно, тоже является термом).

Все понял. У Мендельсона нет термина сложный терм. У него, собственно, нет вообще никакого термина для этого понятия. Есть только $f^n_i(t_1, \cdots, t_n)$ -- "функциональная буква, интерпретируемая операцией $g$". Огромное спасибо.

А вот тут не понимаю:

Xaositect в сообщении #469182 писал(а):

Обычно $x$ и $y$ - это метасимволы для переменных, а $s$ и $t$ - для термов. Т.е. первое $\mathscr{E}(x, y)$ означает некоторую фиксированную формулу от фиксированных переменных $x$ и $y$, а $\mathscr{E}(s,t)$ - подстановку в эту формулу произвольных термов.

Я понимаю, что $s$ и $t$ – термы (переменные или постоянные?) и, соответственно, $\mathscr{E}(s,t)$ - подстановка в эту формулу произвольных термов. А вот с фиксированными переменными $x$ и $y$ хуже. Никаких метасимволов и фиксированных переменных у Мендельсона нет. У него есть только термы: предметная переменная, предметная константа и "функциональная буква, интерпретируемая операцией $g$" (то, что Вы называете сложным термом).

[Виктор Викторов]

«В теориях первого порядка с равенством для выражений вида «существует один и только один предмет $x$ такой, что...» можно использовать следующее Определение. $\exists_1 x \mathscr A(x)$ означает $\exists x \mathscr A(x) \wedge \forall x \forall y(\mathscr A(x) \wedge \mathscr A(y) \to x=y)$.» Страница 90.

А теперь пусть «равенство» (эквивалентность) определено как $x \equiv y(mod3)$ и $\mathscr A(x)$ также $x \equiv y(mod3)$. Тогда (вроде как) всё утряслось, но об единственности говорить не приходится. Правда переводчик отбросил примечание (позже введенное в основной текст): «Новая переменная $y$ предполагается первой переменной отсутствующей в $\mathscr A(x)$».

Поэтому исправим наш пример так: ... пусть «равенство» (эквивалентность) определено как $x \equiv z(mod3)$ и, соответственно, $\exists_1x (x \equiv z(mod3))$ означает $\exists x (x \equiv z(mod3)) \wedge \forall x \forall y(x \equiv z(mod3) \wedge z \equiv y(mod3) \to x\equiv y)$.»

[Виктор Викторов]

Меня весьма не устроило моё понимание параграфа «Теории первого порядка с равенством». Тогда я полез в начало параграфа и понял, что надо вернуться к введению кванторов. Итак, что такое квантор всеобщности? Смотрим на странице 53: «Чтобы сделать более прозрачной структуру сложных высказываний, удобно ввести специальные обозначения для некоторых часто встречающихся выражений. Если $P(x)$ означает, что $x$ обладает свойством $P$, то договоримся посредством $\forall xP(x)$ обозначать утверждение: «для всякого предмета $x$ свойство $P$ выполнено», или, другими словами, «все $x$ обладают свойством $P$»».
И чуть ниже: «В выражении $\forall xP(x)$ часть $\forall x$ называется квантором всеобщности, ...» Что же такое квантор всеобщности — часть $\forall x$ в формуле $\forall xP(x)$? Специальное обозначение? Полез в Вики в статью «Квантор» и упал под стол. Вот, что я там обнаружил: «Не путать с: Кантор».
Попробуем подойти с другой стороны: была формула $P(x)$ появилась формула $\forall xP(x)$. Весьма похоже на оператор. Сравним с оператором отрицания $\neg$. В Вики: «Отрица́ние в логике — унарная операция над суждениями, результатом которой является суждение». Аналогично, квантор всеобщности — унарная операция над формулами. Но если унарная операция отрицания требует на входе только формулу, то унарная операция квантор всеобщности требует на входе формулу и переменную. Дальше уже проще: «В выражении $(\forall y\mathscr A)$ «$\mathscr A$» называется областью действия квантора $\forall y$.» Страница 54. И с помощью понятия «терм свободный для переменной» мы избавляемся от неприятной двусмысленности при подстановке термов.
А теперь только с синтаксической точки зрения, как эта унарная операция определена в теории K? Ответ на этот вопрос на странице 66: «(4) $\forall x_i\mathscr A(x_i)\to \mathscr A(t)$, где $\mathscr A(x_i)$ есть формула теории К и $t$ есть терм теории К, свободный для $x_i$ в $\mathscr A(x_i)$.»
Итак, с синтаксической точки зрения от посылки $\forall x_i\mathscr A(x_i)$ и импликации $\forall x_i\mathscr A(x_i)\to \mathscr A(t)$ с помощью MP можно перейти к $\mathscr A(t)$, где $t$ любой терм теории К. И имеется только одно ограничение: «... свободный для $x_i$ в $\mathscr A(x_i)$.»
Здесь же, по сути дела, поясняется некоторая терминология:

Xaositect в сообщении #469182 писал(а):

Обычно $x$ и $y$ - это метасимволы для переменных, а $s$ и $t$ - для термов. Т.е. первое $\mathscr{E}(x, y)$ означает некоторую фиксированную формулу от фиксированных переменных $x$ и $y$, а $\mathscr{E}(s,t)$ - подстановку в эту формулу произвольных термов.

В аналогичном случае (в той же аксиоме 4) Мендельсон пишет: «Заметим, что $t$ может совпадать с $x_i$ и тогда мы получаем аксиому $\forall x_i\mathscr A(x_i)\to \mathscr A(x_i)$.»
Здесь $x_i$ — предметная переменная (терм, конечно, но не предметная постоянная или сложный терм (совершенно необходимый термин, отсутствующий у Мендельсона!)), а $t$ — любой терм. Теперь становится ясным и комментарий Xaositect.
Осталось только добавить, что для манипулирования квантором всеобщности импликацией вводится ещё одна аксиома:
«(5) $\forall x_i(\mathscr A\to \mathscr B)\to (\mathscr A\to \forall x_i\mathscr B)$, если формула $\mathscr A$ не содержит свободных вхождений $x_i$.»

[Виктор Викторов]

Первые результаты подробной кванторной «разборки» с синтаксической точки зрения. «(6) $\forall x_1(x_1 = x_1)$ (рефлексивность равенства);» Что можно сделать с 6-ой аксиомой? Ответ очевиден: применить 4-ую аксиому и получить следующий вывод:
$\vdash \forall x_1(x_1 = x_1)$
$\vdash \forall x_1(x_1 = x_1)\to (t = t)$
$\vdash t = t$ для каждого терма $t$ по MP.
Осталось только выяснить зачем Мендельсону для этого доказательства потребовалось правило A4.

Несколько элегантнее можно доказать симметричность: «(b) $\vdash x=y \to y=x$». Действительно, если считать, что $\mathscr A(x, x)$ это $x = x$ и $\mathscr A(x, y)$ — $y = x$, то согласно (7) $\vdash (x = y)\to (x = x\to y=x)$ и так как мы уже доказали, что $\vdash x = x$, то для нужного вывода просто переставим посылки в $(x = y)\to (x = x\to y=x)$ с помощью тавтологии $(A\to (B\to C))\to (A\to (B\to C))$.

[Виктор Викторов]

«(7) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$ (подстановочность равенства), где $x$ и $y$ — предметные переменные, $\mathscr A(x, x)$ — произвольная формула, a $\mathscr A(x, y)$ получается из $\mathscr A(x, x)$ заменой каких-нибудь (не обязательно всех) свободных вхождений $x$ вхождениями $y$, с соблюдением условия, чтобы $y$ было свободно для тех вхождений $x$, которые заменяются.» Страница 86.

В этом определении сказано, что «$\mathscr A(x, x)$ — произвольная формула». Если я правильно понимаю, то «произвольность» полностью снимает возможность подогнать под это определение эквивалентность? И тогда обратного хода нет, т. е. из предложения 2.14 (рефлексивность, симметричность и транзитивность) подстановочность не выводится.