Вывод формулы из формулы

[Qlin]

$ \forall x \exists y \ P(x \circ y) $
$ \exists y \ P(y) $

Можно ли из первой формулы получить вторую? Аксиомы и правила можно взять такие, как в лекциях у Шехтмана: lpcs.math.msu.su/vml2018/vml2018_lecture_11.pdf

В частности там есть аксиома $ [t/a]A \rightarrow \exists x \ [x/a]A$. Применительно к моему случаю это должно выглядеть так: $ P(x,y) \rightarrow \exists y \ P(y)$. Но воспользоваться MP я здесь не могу, потому что $P(x,y)$ не выведено.

-- 17.06.2019, 12:17 --

Можно, например, заменить $\forall$ на $\exists$:
$ \forall x \forall y \ P(x \circ y) \rightarrow \forall x \exists y \ P(x \circ y) $
Но в обратную сторону так не получится. Что тогда с этим делать?

[arseniiv]

А что такое $\circ$?

[Qlin]

Это функциональный символ, обозначающий некоторую двухместную операцию.

[arseniiv]

А аксиома 1 $\forall x.[x/a]A\to[t/a]A$ не применяется? Получите $\exists y.P(x\circ y)$, после этого нам надо получить $\exists y.P(x\circ y)\to\exists y.P(y)$, для этого мы применим аксиому 4 $\forall y.[y/a](B\to A)\to(\exists y.[y/a]B\to A)$. Нам понадобится вывести $\forall y.(P(x\circ y)\to\exists y.P(y))$, для этого мы могли бы применить Gen к аксиоме 2 $P(x\circ y)\to\exists y.P(y)$, но нельзя. Но ситуация уже значительно улучшилась, наверняка вы найдёте выход.

-- Пн июн 17, 2019 18:42:22 --

(Который заключается в $\alpha$-конверсии вовремя, чтобы переменные перестали совпадать где не надо.)

-- Пн июн 17, 2019 18:55:51 --

Вообще я бы лично предложил такой конструктивный вывод. Пусть имеется $t : \Pi(x : A).\Sigma(y : B).P(x*y)$, и надо найти $u : \Sigma(y : B).P(y)$, причём известно, что $A, B$ населены, имеется $a : A$ (в классическом исчислении предикатов предполагается, что области интерпретаций не могут быть пустыми; иначе аксиомы были бы опровержимы). Начинаем хоровод:
$ta : \Sigma(y : B).P(a*y)$;
$b:\equiv \mathsf{fst}(ta) : B$;
$c:\equiv \mathsf{snd}(ta) : P(a*b)$;
Тут надо остановиться и увидеть, что должно быть $P : \Pi(z : B)\ldots$ и ${*} : A\times B\to B$ из требований задачи.
Теперь так как $b' :\equiv a * b : B$ и $c : P(a*b) \equiv P(b')$, имеем наконец
$(b, c) : \Sigma(y : B).P(y)$.
Всё!

Теперь вы можете попробовать превратить его в обычный классический. Термы это доказательства, аппликация это склейка доказательств с помощью MP, абстракция была бы применением теоремы о дедукции, но здесь не использовалась. Чему соответствует выбор $a : A$… секрет.

-- Пн июн 17, 2019 18:57:20 --

Заметьте, как легко и приятно выходит. Совершенно прозрачно, что надо делать — как минимум в таком случае, когда было понятно и почему должна быть выводимость.

-- Пн июн 17, 2019 19:02:31 --

Не, я немного ошибся, но всё теперь исправлено.

[Qlin]

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

могли бы применить Gen к аксиоме 2, но нельзя

Интересно тоже, почему нельзя, то есть почему Gen сформулировано именно таким образом. Если я вывел формулу, содержащую свободную переменную, то что мешает именно по этой переменной навесить $\forall$ ? В прошлой теме мне объясняли про равнодоказуемость этих формул: http://dxdy.ru/post1399570.html#p1399570

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

заключается в $\alpha$-конверсии

$\alpha$-конверсией называется замена свободной переменной на другую?

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

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

$t : \Pi(x : A).\Sigma(y : B).P(x*y)$

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

$b:\equiv \mathsf{fst}(ta) : B$;
$c:\equiv \mathsf{snd}(ta) : P(a*b)$;

Как научиться понимать эти символы?

[arseniiv]

Qlin в сообщении #1399787 писал(а):

Если я вывел формулу, содержащую свободную переменную, то что мешает именно по этой переменной навесить $\forall$ ?

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

Дело в том, что свободные переменные, встречающиеся в выводе, могут иметь смысл не только произвольных значений, но и некоторых введённых из-за снятия $\exists$ констант. Если сделать Gen по такой константе, получится семантически недопустимый вывод.

[Qlin]

arseniiv, было бы интересно увидеть конкретный пример, когда получается семантически недопустимый вывод.

[arseniiv]

Qlin в сообщении #1399787 писал(а):

$\alpha$-конверсией называется замена свободной переменной на другую?

Как раз связанной. Свободная видна миру, её нельзя взять и втихую поменять, а про связанную никто не узнает. В нотации де Брёйна их вообще нет.

Qlin в сообщении #1399787 писал(а):

Словосочетание конструктивный вывод я вижу впервые.

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

Qlin в сообщении #1399787 писал(а):

Как научиться понимать эти символы?

Вообще это теория с зависимыми типами («зависимыми» здесь всегда означает терм, обозначающий тип, может включать термы, обозначающие значения типов; для других возможных вхождений приняты другие названия). По идее должно хватать теории, введённой Мартин-Лёфом. Зависимые типы нужны, чтобы выражать кванторы.

С другой стороны вы можете просто использовать интерпретацию Брауэра—Гейтинга—Колмогорова (BHK interpretation) интуиционистской логики. Это достаточно неформально, но даст то же.

-- Пн июн 17, 2019 22:05:42 --

Qlin в сообщении #1399795 писал(а):

arseniiv, было бы интересно увидеть конкретный пример, когда получается семантически недопустимый вывод.

Ну не, так не интересно. Посмотрите, что сломается в доказательстве теоремы 11.10, последней там, если убрать ограничение с Gen.

[george66]

Содержательно, берём какой угодно икс и получаем
$\exists y P(x\circ y)$
Дальше обозначаем $x\circ y$ через $z$ и получаем
$\exists z P(z)$
Формально, надо использовать правило вывода, позволяющее из формулы
$P(x\circ y)\Rightarrow\exists z P(z)$ (это кванторная аксиома)
вывести
$\exists y P(x\circ y)\Rightarrow \exists z P(z)$
(введение квантора существования слева).
P.S. Поправил (в последней строчке было написано "всеобщности" вместо "существования")