Доказательство $\alpha \implies \alpha$ выводится

Question

Я прохожу через «Топои» Голдблатта, и одно из упражнений там зависит от доказательства того, что определенная система аксиом влечет за собой $\alpha \implies \alpha$ для любого предложения $\alpha$.

Рассматриваемая система аксиом выглядит следующим образом (параграф 6.3):

1. $ \alpha \implies (\alpha \land \alpha) $
2. $ (\alpha \land \beta) \implies (\beta \land \alpha) $
3. $ (\alpha \implies \beta) \implies ((\alpha \land \gamma) \implies (\beta \land \gamma)) $
4. $ ((\alpha \implies \beta) \land (\beta \implies \gamma)) \implies (\alpha \implies \gamma) $
5. $ \beta \implies (\alpha \implies \beta) $
6. $ (\alpha \land (\alpha \implies \beta)) \implies \beta $
7. $ \alpha \implies (\alpha \lor \beta) $
8. $ (\alpha \lor \beta) \implies (\beta \lor \alpha) $
9. $ ((\alpha \implies \gamma) \land (\beta \implies \gamma)) \implies ((\alpha \lor \beta) \implies \gamma) $
10. $ \lnot \alpha \implies (\alpha \implies \beta) $
11. $ ((\alpha \implies \beta) \land (\alpha \implies \lnot \beta)) \implies \lnot \alpha $
12. $ \alpha \lor \lnot \alpha $

Единственное правило вывода - это обычный modus ponens.

Таким образом, создается ощущение, что аксиома (9) вместе с (12) может использоваться в качестве последнего шага вывода (создание экземпляра $\alpha$ к $\alpha$, $\beta$ к $\lnot \alpha$ и $\gamma$ к $\alpha \implies \alpha$). Тогда левая часть$\land$в (9) можно получить с помощью (5), а правую часть можно получить с помощью (10). Но как мне объединить те, что под$\land$? Похоже, у меня нет обычного$\land$-правило введения - аксиоматические системы, которые я видел раньше, обычно имеют что-то вроде $\alpha \implies (\beta \implies (\alpha \land \beta))$.

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

Итак, как правильно доказать $\alpha \implies \alpha$ в этой системе?

Answer 1

Что ж, пока я не потерял его, вот что дал мне Prover9 после перевода в префиксную нотацию. C (x, y) используется вместо (x⟹y). K (x, y) вместо (x∧y). N (x) вместо$\lnot$Икс. И A (x, y) вместо (x$\lor$y) .:

% -------- Комментарии к оригиналу доказательства --------

% Proof 1 на 1,19 (+ 0,56) секунды.

% Длина доказательства 16.

% Уровень доказательности 6.

% Максимальный вес статьи 14.

% Данные статьи 812.

1 P (C (x, x)) # label (non_clause) # label (цель). [Цель].

2 -P (C (x, y)) | -P (x) | P (y). [предположение].

3 P (C (x, K (x, x))). [предположение].

5 P (C (C (x, y), C (K (x, z), K (y, z)))). [предположение].

7 P (C (x, C (y, x))). [предположение].

11 P (C (K (C (x, y), C (z, y)), C (A (x, z), y))). [предположение].

12 P (C (N (x), C (x, y))). [предположение].

14 P (A (x, N (x))). [предположение].

15 -Р (С (c1, c1)). [отрицать (1)].

24 P (C (x, C (y, C (z, y)))). [гипер (2, а, 7, а, б, 7, а)].

55 P (K (C (N (x), C (x, y)), C (N (x), C (x, y)))). [гипер (2, а, 3, а, б, 12, а)].

99 P (C (K (x, y), K (C (z, C (u, z)), y))). [гипер (2, а, 5, а, б, 24, а)].

1001 P (K (C (x, C (y, x)), C (N (z), C (z, u)))). [гипер (2, а, 99, а, б, 55, а)].

11705 P (C (A (x, N (y)), C (y, x))). [гипер (2, а, 11, а, б, 1001, а)].

11723 P (C (x, x)). [гипер (2, а, 11705, а, б, 14, а)].

11724 $ F. [решить (11723, a, 15, a)].