А что такое вообще правило введения?
Вот с этого и стоило начинать.
1. Есть формализмы, в которых есть только правила вывода (вообще, любую аксиому
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
можно заменить правилом вывода
![$\dfrac{}a$ $\dfrac{}a$](https://dxdy-01.korotkov.co.uk/f/c/6/1/c6179cc6553cb1c8ad3ab1adad4e286a82.png)
). Если взять для примера один из них, натуральную дедукцию, там все правила (кроме правил образования формул и термов) можно разделить на правила введения и удаления практически для каждого способа образования формул (соответствующих связкам, кванторам и пропозициональным константам типа
![$\bot$ $\bot$](https://dxdy-03.korotkov.co.uk/f/6/f/c/6fc05ced17ac7d77ba19372f815467dd82.png)
). Правило введения имеет заключением формулу, построенную соответствующим способом, и правило удаления имеет её среди посылок. Самый рафинированный пример дают правила
![$\dfrac{A,B}{A\wedge B}$ $\dfrac{A,B}{A\wedge B}$](https://dxdy-01.korotkov.co.uk/f/c/9/6/c965925dfeb90b8a82ac24aa5f789f6082.png)
введения и
![$\dfrac{A\wedge B}A,\;\dfrac{A\wedge B}B$ $\dfrac{A\wedge B}A,\;\dfrac{A\wedge B}B$](https://dxdy-01.korotkov.co.uk/f/c/5/0/c50dbd22563e80577aa141646aca9f3682.png)
удаления конъюнкции.
2. Понятно, многие правила такого вида и очень похожие на них являются одновременно и допустимыми правилами вывода для обычных исчислений. И если взять исчисление первого порядка, «пропозициональной» частью аксиом которого выбраны аксиомы, например, Клини, большинство их будет напоминать то или иное правило введения/удаления. Скажем, аксиома
![$(A\to C)\to(B\to C)\to A\vee B\to C$ $(A\to C)\to(B\to C)\to A\vee B\to C$](https://dxdy-02.korotkov.co.uk/f/1/a/e/1ae4b69f3e856d93f0f3905568da07db82.png)
напоминает правило удаления дизъюнкции. (MP = правило удаления импликации, а метатеорема о дедукции в нетривиальную из сторон соответствует правилу её введения.) Дополнительные аксиомы и правила вывода, говорящие о кванторах, тоже можно уложить в эту систему, выбирая, к примеру, правила Бернайса
![$$\frac{B\to A}{B\to\forall xA},\qquad\frac{A\to B}{\exists xA\to B}$$ $$\frac{B\to A}{B\to\forall xA},\qquad\frac{A\to B}{\exists xA\to B}$$](https://dxdy-03.korotkov.co.uk/f/2/b/6/2b64cea352d658639c40e3b54593a71582.png)
(введение
![$\forall$ $\forall$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea226b5977d1a327732124dccb896982.png)
, удаление
![$\exists$ $\exists$](https://dxdy-01.korotkov.co.uk/f/4/2/3/42353da95c0a3784bd8339b6e4fb126082.png)
;
![$B$ $B$](https://dxdy-03.korotkov.co.uk/f/6/1/e/61e84f854bc6258d4108d08d4c4a085282.png)
не содержит
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
параметром) и аксиомы
![$(\forall xA)\to A[t/x]$ $(\forall xA)\to A[t/x]$](https://dxdy-03.korotkov.co.uk/f/e/c/b/ecb1bba311f6fb5105efe1fc9bc0238782.png)
(удаление
![$\forall$ $\forall$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea226b5977d1a327732124dccb896982.png)
) и
![$A[t/x]\to\exists xA$ $A[t/x]\to\exists xA$](https://dxdy-03.korotkov.co.uk/f/2/a/f/2af452d1e596c6e359adbea3d1dd6daf82.png)
(введение
![$\exists$ $\exists$](https://dxdy-01.korotkov.co.uk/f/4/2/3/42353da95c0a3784bd8339b6e4fb126082.png)
) (в обеих замена должна быть корректной, конечно).
Так что имеет смысл сказать, что упомянутые выше
![$\exists!x \varphi\to\exists x\varphi$ $\exists!x \varphi\to\exists x\varphi$](https://dxdy-03.korotkov.co.uk/f/2/7/c/27ca5c2eb6d6874217a96a51cf3ce6ed82.png)
и
![$\exists!x\varphi\to\forall y\forall z(\varphi[y/x]\wedge\varphi[z/x]\wedge\psi\to\psi[z/y])$ $\exists!x\varphi\to\forall y\forall z(\varphi[y/x]\wedge\varphi[z/x]\wedge\psi\to\psi[z/y])$](https://dxdy-02.korotkov.co.uk/f/9/0/d/90de68dbcc77cdb441e59abb8b76274a82.png)
соответствуют правилам удаления
![$\exists!$ $\exists!$](https://dxdy-01.korotkov.co.uk/f/c/0/6/c0671c919e7fce0b1db6dbc679629b9582.png)
. Если мы хотим найти аксиому, соответствующую правилу введения, она должна иметь вид
![$\ldots\to\exists!x\varphi$ $\ldots\to\exists!x\varphi$](https://dxdy-01.korotkov.co.uk/f/4/2/1/42151b59ca86d794c688018ced0e9e0682.png)
(или
![$\ldots\to(\ldots\to\exists!x\varphi)$ $\ldots\to(\ldots\to\exists!x\varphi)$](https://dxdy-02.korotkov.co.uk/f/5/a/5/5a5500a00fe23ccd5990803a7ce0e58a82.png)
и т. д., но вспомнив про конъюнкцию, мы можем ограничиться только первым).
-- Пн май 22, 2017 19:58:21 --(Не претендую на полноту.)