Введение ∃!

[Z1X]

Цитата:

Жалко, правила введения $\exists!$ уже не получится.

Хочется спросить, а какое тут правило? И почему не получится?

[Dan B-Yallay]

Хочется ответить, но непонятно откуда, кто и в связи с чем. И почему должно получиться, если так.

[arseniiv]

Контекст:

Z1X в сообщении #1217471 писал(а):

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

звать $\exists!$ квантором (единственности и существования — или ещё как). И можно определить всё так, чтобы формулы с ним не были сокращением — в исчисление добавить правил вывода

Это очень интересный вопрос. Пусть у вас есть исчисление предикатов без равенства и вы хотите добавить в него все необходимые аксиомы, определяющие $\exists!$ (т.е. существование и единственность). Можно ли это сделать? Как это сделать? Мне пока в голову приходит только очевидная аксиома $\exists!x \ \varphi \rightarrow \exists x \ \varphi$. Что еще?

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

Если понимать под равенством неразличимость свойств, то еще получится $\exists! x \varphi(x) \to \forall y z(\varphi(y) \operatorname\& \varphi(z) \operatorname\& \psi(y) \to \psi(z))$.

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

Жалко, правила введения $\exists!$ уже не получится.

Не получится из-за того, что мы не можем выразить равенство. Конечно, в какой-то теории в языке, расширяющем этот, это может оказаться возможным, но не прямо здесь. Мы не можем просто «обратить» конъюнкцию ваших двух аксиом для каждой $\varphi$, потому что в схему Xaositect входит ещё $\psi$, а бесконечную конъюнкцию для всех $\psi$ мы составить не сможем.

В языке второго порядка, конечно, можно сделать $\forall\psi$ (тут это уже унарный предикатный символ), но там, кстати, и равенство выразимо, так что ничего удивительного.

-- Вс май 21, 2017 14:07:43 --

Ну, это, конечно, у меня не строгое доказательство, а так, на пальцах.

[Z1X]

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

Не получится из-за того, что мы не можем выразить равенство. Конечно, в какой-то теории в языке, расширяющем этот, это может оказаться возможным, но не прямо здесь.

А зачем вам потребовалось выразить равенство? Равенство нужно не выразить, а дать ему определение вроде: $\exists ! x\, \varphi(x) \leftrightarrow \exists x\, \varphi(x) \wedge \forall y\, \forall z\,((\varphi(y) \wedge \varphi(z)) \to y = z) $,
где квантор $\exists !$ уже задан аксиомами исчисления.

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

Мы не можем просто «обратить» конъюнкцию ваших двух аксиом для каждой $\varphi$, потому что в схему Xaositect входит ещё $\psi$, а бесконечную конъюнкцию для всех $\psi$ мы составить не сможем.

Я не понял, что вы хотите обратить, куда и зачем.

[arseniiv]

А как, по-вашему, должно выглядеть правило введения $\exists!$ ?

[Z1X]

А что такое вообще правило введения? Есть аксиомы, есть правила вывода. Если вопрос о том, какие правила вывода должны содержать новый квантор, то я могу предложить следующее: $\dfrac {\forall x \varphi \rightarrow \exists ! x \varphi,\;\exists ! x \varphi \to \forall x \varphi}{\forall x \varphi \wedge \exists ! x \varphi}$

[arseniiv]

Z1X в сообщении #1217919 писал(а):

А что такое вообще правило введения?

Вот с этого и стоило начинать.
1. Есть формализмы, в которых есть только правила вывода (вообще, любую аксиому $a$ можно заменить правилом вывода $\dfrac{}a$). Если взять для примера один из них, натуральную дедукцию, там все правила (кроме правил образования формул и термов) можно разделить на правила введения и удаления практически для каждого способа образования формул (соответствующих связкам, кванторам и пропозициональным константам типа $\bot$). Правило введения имеет заключением формулу, построенную соответствующим способом, и правило удаления имеет её среди посылок. Самый рафинированный пример дают правила $\dfrac{A,B}{A\wedge B}$ введения и $\dfrac{A\wedge B}A,\;\dfrac{A\wedge B}B$ удаления конъюнкции.
2. Понятно, многие правила такого вида и очень похожие на них являются одновременно и допустимыми правилами вывода для обычных исчислений. И если взять исчисление первого порядка, «пропозициональной» частью аксиом которого выбраны аксиомы, например, Клини, большинство их будет напоминать то или иное правило введения/удаления. Скажем, аксиома $(A\to C)\to(B\to C)\to A\vee B\to C$ напоминает правило удаления дизъюнкции. (MP = правило удаления импликации, а метатеорема о дедукции в нетривиальную из сторон соответствует правилу её введения.) Дополнительные аксиомы и правила вывода, говорящие о кванторах, тоже можно уложить в эту систему, выбирая, к примеру, правила Бернайса

$$\frac{B\to A}{B\to\forall xA},\qquad\frac{A\to B}{\exists xA\to B}$$

(введение $\forall$, удаление $\exists$; $B$ не содержит $x$ параметром) и аксиомы $(\forall xA)\to A[t/x]$ (удаление $\forall$) и $A[t/x]\to\exists xA$ (введение $\exists$) (в обеих замена должна быть корректной, конечно).

Так что имеет смысл сказать, что упомянутые выше $\exists!x \varphi\to\exists x\varphi$ и $\exists!x\varphi\to\forall y\forall z(\varphi[y/x]\wedge\varphi[z/x]\wedge\psi\to\psi[z/y])$ соответствуют правилам удаления $\exists!$. Если мы хотим найти аксиому, соответствующую правилу введения, она должна иметь вид $\ldots\to\exists!x\varphi$ (или $\ldots\to(\ldots\to\exists!x\varphi)$ и т. д., но вспомнив про конъюнкцию, мы можем ограничиться только первым).

-- Пн май 22, 2017 19:58:21 --

(Не претендую на полноту.)

[george66]

Z1X в сообщении #1217919 писал(а):

А что такое вообще правило введения? Есть аксиомы, есть правила вывода. Если вопрос о том, какие правила вывода должны содержать новый квантор, то я могу предложить следующее: $\dfrac {\forall x \varphi \rightarrow \exists ! x \varphi,\;\exists ! x \varphi \to \forall x \varphi}{\forall x \varphi \wedge \exists ! x \varphi}$

Ой! Что это?

[arseniiv]

О да. Z1X, заключение тут говорит об одноэлементности модели и при этом никак не следует из $\forall x\varphi\leftrightarrow\exists!x\varphi$, равносильного посылкам, т. к. оно выполняется не только в одноэлементных — достаточно, чтобы $\varphi$ была опровержима и истинна не ровно на одном элементе области интерпретации. Вы точно именно это хотели написать?