Доказательство (forall x, a -> b)/\ (существует x, a) -> (существует x, b)

Question

Я пытаюсь доказать: (forall x, a -> b) /\ (exists x, a) -> (exists x, b).

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

Мои доступные правила вывода включают МОДУС-поненс: a, a->b |- b

и обобщение: a(x) |- forall(x, a(x))

включают также стандартные правила замещения.

Мои аксиомы:
1) Любая тавтология в условной логике с 3 булевыми переменными или меньше.
(Предположим, что стандартные определения для булевых операций: ~,/\, V, ->, < ->).
2) (forall x, a(x)) -> a(t) (где Т 'замещаемая' для й в)
3) forall(x, a -> b) -> ((forall x, a) -> (forall x, b))
4) a -> (forall x, a) (если й не свободны в)
5) forall(x, a) <--> ~exists(x, ~a)

Некоторых современных теорем у меня уже производном, которые могут быть полезны:
(forall x, a /\ b) <--> (forall x, a) /\ (forall x, b)
(forall x, a) -> (exists x, b)

Моя система вывод не имеет возможность временно ввести предположения, что не доказаны, как вы могли бы ожидать в системе естественного вычета.

Answer 1

Кажется, я нашел свое решение. Для чего это стоит, эта проблема на самом деле должна была быть опубликована до https://math.stackexchange.com/, но сделано. Для тех из вас, кто может быть любопытен, вот решение. Кстати, правила заимствованы из логических аксиом Эндертона в «Математическом введении к логике». Однако аксиомы не совсем идентичны.

Прежде чем приступить к теореме, я должен ввести пару других теорем и мета-теорему, которую я доказал с этими аксиомами. (Я буду использовать их в выводе ниже).

Первый: (a -> b) /\ (b -> c)) -> (a -> c) (ГипотетическийSyllogism: тавтология).
Второе: exists(x, a) -> ~forall(x, ~a) (ExistsDefined. Производится с использованием правила 5).
Третий: (a->b) -> (~b -> ~a) (Contrapositive: тавтология).
Следующая: alpha, beta |- alpha /\ beta (Теорема о конъюнктуре).
Мета-теорема наблюдаема из следующей тавтологии в сочетании с modus-ponens:
(a->(b->(a /\ b))).
Наконец: Любая тавтология, независимо от того, сколько переменных, может быть выведена, используя только 3 переменные в качестве времени. Однако длина доказательства, в общем, быстро растет с числом переменных (если предположить, что NP! = CoNP). Я использую этот факт на шаге 15 дедукции ниже, где я использую 5 переменных вместо моего предела 3.

Вот теперь доказательство:

1. ~b -> ((a -> b) -> ~ a) (тавтология).
2. forall(x, ~b -> ((a -> b) -> ~a)) (со стадии 1).
3. forall(x, ~b -> ((a -> b) -> ~a)) -> (forall(x, ~b) -> (forall(x, (a -> b) -> ~a))) (Правило 3).
4. forall(x, ~b) -> forall(x, (a -> b) -> ~a) (ModusPonens с этапов 2 и 3).
5. forall(x, (a -> b) -> ~a) -> (forall(x, a -> b) -> forall(x, ~a)) (Правило 3).
6. (forall(x, ~b) -> forall(x, (a -> b) -> ~a)) /\ (forall(x, (a -> b) -> ~a) -> (forall(x, a -> b) -> forall(x, ~a))) -> (forall(x, ~b) -> (forall(x, a -> b) -> forall(x, ~a))) (from HypotheticalSyllogism).
7. (forall(x, ~b) -> forall(x, (a -> b) -> ~a)) /\ (forall(x, (a -> b) -> ~a) -> (forall(x, a -> b) -> forall(x, ~a))) (КонъюнкцияВведение шагов 4 и 5).
8. forall(x, ~b) -> (forall(x, a -> b) -> forall(x, ~a)) (ModusPonens, этапы 6 и 7).
9. (forall(x, ~b) -> (forall(x, a -> b) -> forall(x, ~a))) -> (~(forall(x, a -> b) -> forall(x, ~a)) -> ~forall(x, ~b)) (Contrapositive).
10. ~(forall(x, a -> b) -> forall(x, ~a)) -> ~forall(x, ~b) (ModusPonens, этапы 8 и 9).
11. exists(x, b) <-> ~forall(x, ~b) (ExistsDefined).
12. exists(x, a) <-> ~forall(x, ~a) (ExistsDefined).
13. (exists(x, a) <-> ~forall(x, ~a)) /\ (exists(x, b) <-> ~forall(x, ~b)) (КонъюнкцияВведение шагов 11 и 12).
14. (~(forall(x, a -> b) -> forall(x, ~a)) -> ~forall(x, ~b)) /\ (exists(x, a) <-> ~forall(x, ~a)) /\ (exists(x, b) <-> ~ forall(x, ~b)) (ConjunctionIntroduction steps 10, 13).
15. (~(a -> b) -> ~c) /\ (e <-> ~b) /\ (d <-> ~c) -> (a /\ e -> d) (Метатеория тавтологии).
16. (~(forall(x, a -> b) -> forall(x, ~a)) -> ~forall(x, ~b)) /\ (exists(x, a) <-> ~forall(x, ~a)) /\ (exists(x, b) <-> ~forall(x, ~b)) -> (forall(x, a -> b) /\ exists(x, a) -> exists(x, b)) (с шага 15).
17. forall(x, a -> b) /\ exists(x, a) -> exists(x, b) (ModusPonens, шаги 14, 16).