Построение формального вывода теорем

[vinchkovsky]

Здравствуйте.

Нужно доказать (построить формальный вывод) такие две (выбрал те, которые совсем не знаю; возможно, в случае подсказки добавлю еще одну) теоремы:
$\exists x (A(x) \vee B(x))\to (\exists x A(x) \vee \exists x B(x))$
$\exists x \forall y A(x,y)\to \forall x \exists y A(x,y)$

Схемы аксиом такие:
$A1: F\to (G\to F)$
$A2: (F\to (G\to H))\to((F\to G)\to (F\to H))$
$A3: (\neg G\to \neg F)\to ((\neg G\to F)\to G)$
$A4: \forall x F(x)\to F(t)$, если $t$ - свободный
$A5: \forall x(F\to G)\to (F\to \forall x G)$

Правила вывода - МП и Gen:
С $С F(x) $ выводится \forall x F(x)$

А вот те теоремы, которыми можно пользоваться в формальном выводе:
$a) \neg \neg F\to F$
$b) F\to \neg \neg F$
$c) \neg F\to (F\to G)$
$d) (\neg G\to \neg F)\to (F\to G)$
$e) (F\to G)\to (\neg G\to \neg F)$
$f) F\to (\neg G\to \neg (F\to G))$
$g) (F\to G)\to ((\neg F\to G)\to G)$

В арсенале еще теорема дедукции (конечно, с ограничением на Gen) вместе с силлогизмами как следствиями.
Никак не могут покорится теоремы со кванторами существования; буду благодарен за помощь

[vinchkovsky]

Решил/разобрался ;)

[Maslov]

И вторую решили?

vinchkovsky в сообщении #308488 писал(а):

$\exists x \forall y A(x,y)\to \forall x \exists y A(x,y)$

Вы, наверное, ошиблись в условии.
Возьмите, например, $A(x, y) \equiv x + y = y$.

Скорее всего, имелось в виду $\exists x \forall y A(x,y)\to \forall y \exists x A(x,y)$

[vinchkovsky]

Да, извиняюсь за ошибку.