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

[Xaositect]

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

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

Да, именно подстановочность выделяет равенство среди всех отношений эквивалентности.

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

Итак, «подвал» страницы 90.

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

$\mathscr E(x, y)$ — это формула вида $E_1^2(x_1, x_2)$ где $x_1$ и $ x_2$ только имеющиеся в формуле предметные переменные или $x$ и $y$ выделенные переменные с которыми мы собрались работать и в формуле могут быть и другие переменные? Дальше идет странный для меня оборот речи «если $\mathscr E(t, s)$ обозначить через $t = s$». Если посмотреть в определение на странице 86, то там «Будем для сокращения писать $t = s$ вместо $A_1^2$», но тогда и $\mathscr E(x, y)$ есть $x = y$? Но это приводит к проблеме в следующем куске текста:

«При этом только следует условиться считать, что если $t$ и $s$ — термы, не свободные соответственно для $x$ и $y$ в $\mathscr E(x, y)$, то $t = s$ служит сокращенным обозначением не для $\mathscr E(t, s)$, а для некоторой формулы $\mathscr E^{*}(t, s)$, которая получена из $\mathscr E(t, s)$ подходящим переименованием связанных переменных (см. следствие 2.22) таким образом, чтобы $t$ и $s$ оказались свободными соответственно для $x$ и $y$ в $\mathscr E^{*}(t, s)$.»

Если речь идет о том, что формула $\mathscr E(x, y)$ является формулой $x = y$, то как $t$ и $s$ могут быть не свободны соответственно для $x$ и $y$ в $\mathscr E(x, y)$?

«Для таких теорий К могут быть доказаны предложения, аналогичные предложениям 2.25 и 2.26, в предположении, что (7) является теоремой в К для соответствующих типов формул $\mathscr E^{*}(t, s)$. (Предоставляется читателю в качестве упражнения.)
В теориях первого порядка с равенством для выражений вида «существует один и только один предмет $x$ такой, что...» можно использовать следующее
Определение. $\exists _1x\mathscr A(x)$ означает $\exists x \mathscr A(x)\wedge \forall x\forall y(\mathscr A(x)\wedge \mathscr A(y)\to x=y)$.»

Благодаря предыдущему замечанию Xaositect, вопрос с последним определением полностью прояснился. Спасибо!

[Xaositect]

По поводу определения равенства.
В теории первого порядка с равенством по определению имеется двуместный предикатный символ $=$. В этом случае, разумеется, любой терм свободен в $x = y$ для $x$ или $y$, и ничего оговаривать не надо.
Эта конструкция говорит о том, что иногда, рассматривая теорию без равенства, в ней можно некоторую формулу взять за определение равенства и представить эту теорию как теорию с равенством.
Рассмотрим простой пример: теорию с функциональным символом $+$, предикатом $Z$ и такими аксиомами:
$\forall x Z(x + x)$
$\forall x y (Z((x+x)+y)\leftrightarrow Z(y))$
$\forall x y (Z(x)\& Z(y)\rightarrow Z(x+y))$
$\forall x y z(Z(x+(y+z))\leftrightarrow Z((x+y)+z))$
$\forall x y(Z(x+y)\leftrightarrow Z(y+x))$
И рассмотрим $\mathscr E(x, y) = Z(x + y)$
Тогда из первой аксиомы $\forall x \mathscr E(x, x)$, а c помощью остальных из $\mathscr E(x, y)$ можно вывести $\forall z\mathscr E(x+z, y+z)$, $\forall z\mathscr E(z+x, z+y)$, и $Z(x)\rightarrow Z(y)$ и индукцией по построению формулы $\mathscr A$ доказать, что $\mathscr E(x, y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$.
Теперь мы можем построить новую теорию с символом $=$, добавив к нашей аксиому $\forall x y (x = y\leftrightarrow \mathscr E(x, y))$, и она будет теорией с равенством. При этом она является по сути той же теорией (консервативное расширение: любая теорема исходной теории остается теоремой в новой, а любая теорема новой теории является теоремой исходной, если не содержит символов, не принадлежащих алфавиту исходной теории)

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

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

Эта конструкция говорит о том, что иногда, рассматривая теорию без равенства, в ней можно некоторую формулу взять за определение равенства и представить эту теорию как теорию с равенством.

Учитывая, что аксиома подстановки исключает эквивалентность, это стало понятным. Пример «некоторой формулы» -- разность.

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

Рассмотрим простой пример: теорию с функциональным символом $+$, предикатом $Z$ и такими аксиомами:
$\forall x Z(x + x)$
$\forall x y (Z((x+x)+y)\leftrightarrow Z(y))$
$\forall x y (Z(x)\& Z(y)\rightarrow Z(x+y))$
$\forall x y z(Z(x+(y+z))\leftrightarrow Z((x+y)+z))$
$\forall x y(Z(x+y)\leftrightarrow Z(y+x))$

А вот с пониманием простого примера у меня проблемы. Идея понятна. Проблемы с инструментарием. У Мендельсона нет понятия «функциональный символ». Поэтому я вынужден понимать $x+y$ как сложный терм. Прежде чем разбирать дальнейшее я бы хотел узнать где можно прочитать про «функциональный символ».

[Xaositect]

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

«функциональный символ»

У Мендельсона - функциональная буква. Здесь я просто пишу $t+s$ вместо $+^2(t, s)$

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

Спасибо. Разобрался. Красиво Вы свойства симметрической разности использовали.

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

Все было так хорошо и вдруг на странице 91: «Для всякой модели теории первого порядка К с равенством отношение $E$, соответствующее в этой модели предикатной букве $=$, является отношением эквивалентности (в силу предложения 2.24).» Да, конечно, но дальше:
«Если в области некоторой модели это отношение $E$ оказывается отношением тождества, то эта модель называется нормальной.» Но ведь на основании аксиомы (7) $(x=y)\to (\mathscr A(x, x)\to \mathscr A(x, y))$ (подстановочность равенства) «это отношение $E$» является отношением тождества!

[Xaositect]

Вообще говоря нет. Это минимальное отношение эквивалентности, которое теория может "различить". Всегда можно построить модель, в котором будут два нетождественных в модели, но равных в теории объекта. Например, просто взять произвольную модель и "раздвоить" каждый элемент области интерпретации.

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

Вот этого я как раз и не понимаю.

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

Да, именно подстановочность выделяет равенство среди всех отношений эквивалентности.

Как учитывая, аксиому (7) получить «два нетождественных в модели, но равных в теории объекта»?

[Xaositect]

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

Как учитывая, аксиому (7) получить «два нетождественных в модели, но равных в теории объекта»?

Возьмем чистое исчисление предикатов с равенством.
Возьмем некоторую его модель(нормальную) с областью интерпретации $D$ и выделим некоторый элемент $a\in D$ , в которой равенству соответсвует отношение тождества.
Построим новую модель. Возьмем область $D'$, в которой вместо $a$ есть элементы $a_0$ и $a_1$ и определим функцию $f\colon D'\to D$, отображающую любой элемент, кроме $a_i$ в себя, а $a_i$ в $a$. Оценку остальных предикатов построим на основе исходной модели: $P(c_1,\dots c_n)$ будет истинным тогда и только тогда, когда в исходной модели истинно $P(f(c_1),\dots f(c_n))$. Предикат равенства при этом задается так: любой элемент равен самому себе, и $a_0 = a_1$, $a_1 = a_0$.
Все формулы, истинные в исходной интерпретации, истинны и в новой. В новой интерпретации $a_0$ и $a_1$ нетождественны, но в теории нет средств для того, чтобы это выразить. Подстановочность выполняется.
Подстановочность является характеризующим свойством равенства: она эквивалентна тому, что отношение равенства является минимальным среди всех отношений эквивалентности, соответствующих формулам теории, но может не является минимальным в модели (но синтаксическая теория этого "не видит")

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

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

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

Вот это, как раз, и есть, то, что я не понимаю. Я думал, что, если

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

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

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

Да, именно подстановочность выделяет равенство среди всех отношений эквивалентности.

, то выполнимость для «каждой формулы» в аксиоме (7) и гарантирует тождественность. Что же нам тогда дает подстановочность? Возвращаемся, например, к эквивалентности по модулю?

[Xaositect]

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

, то выполнимость для «каждой формулы» в аксиоме (7) и гарантирует тождественность. Что же нам тогда дает подстановочность? Возвращаемся, например, к эквивалентности по модулю?

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

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

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

[Xaositect]

С точностью до эквивалентности.
Соответственно, если в качестве легальных моделей рассматриваются только нормальные - то единственный.

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

Итак, то что я понял «до моделей» т. е. с синтаксической точки зрения. У нас есть понятие «терм». Причем термы нельзя сравнивать (либо это тот же самый терм (последовательность символов) либо другой терм). В этом смысле «3+1» и «4» просто различные термы.

Аксиома (6) $\forall x_1(x_1 = x_1)$ гарантирует нам, что при подстановке одного и того же терма в предикат равенства формула выводима при каждом $x_1$, но аксиома умалчивает, что произойдет, если в эту формулу подставлены различные термы.

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

При этом формула $\exists x \mathscr A(x)\wedge \forall x\forall y(\mathscr A(x)\wedge \mathscr A(y)\to x=y)$ означает единственность в том смысле, что, если такие термы при которых данная формула выводима существуют, то формула равенства для них выводима.
Мой глаз поймал намек на интерпретацию в фразе: «В теориях первого порядка с равенством для выражений вида «существует один и только один предмет $x$ такой, что...» можно использовать следующее
Определение. $\exists _1x\mathscr A(x)$ означает $\exists x \mathscr A(x)\wedge \forall x\forall y(\mathscr A(x)\wedge \mathscr A(y)\to x=y)$.»
Но это просто ещё одна вольность переводчика. В оригинале слово «предмет» отсутствует. "There exists one and only one $x$ such that..."