İspat $\alpha \implies \alpha$ türetilebilir

Question

Goldblatt'ın "Topoi" sinden geçiyorum ve buradaki alıştırmalardan biri, belirli bir aksiyom sisteminin gerektirdiğini kanıtlamaya bağlı. $\alpha \implies \alpha$ herhangi bir teklif için $\alpha$.

Söz konusu aksiyom sistemi aşağıdaki gibidir (paragraf 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 $

Tek çıkarım kuralı olağan modus ponens'tir.

Dolayısıyla, aksiyom (9) (12) ile birlikte türetmenin son adımı olarak kullanılabilir (örnekleme) $\alpha$ -e $\alpha$, $\beta$ -e $\lnot \alpha$ ve $\gamma$ -e $\alpha \implies \alpha$). Ardından, sol taraf$\land$(9) 'da (5) kullanılarak türetilebilir ve sağ taraf (10) kullanılarak türetilebilir. Ama bunları bir altında nasıl birleştiririm$\land$? Görünüşe göre her zamanki gibi değilim$\land$-introduction kuralı - daha önce gördüğüm aksiyomatik sistemler tipik olarak formda bir şeye sahiptir $\alpha \implies (\beta \implies (\alpha \land \beta))$.

Ayrıca, açıkça yapıcı olan bu ifade için dışlanmış orta (yapıcı olmayan) aksiyomuna başvurmak yanlış geliyor.

Öyleyse kanıtlamanın doğru yolu nedir $\alpha \implies \alpha$ bu sistemde?

Answer 1

Ben onu kaybetmeden önce, işte Prover9'un önek gösterimine çevrildikten sonra bana verdiği şey buydu. (X⟹y) yerine C (x, y) kullanılır. (X∧y) yerine K (x, y). Yerine N (x)$\lnot$x. Ve (x yerine A (x, y)$\lor$y) .:

% -------- Orijinal ispattan yorumlar --------

1.19 (+ 0.56) saniyede% Proof 1.

% İspat uzunluğu 16'dır.

% İspat seviyesi 6'dır.

% Maksimum fıkra ağırlığı 14'tür.

% 812. maddeler verilmiştir.

1 P (C (x, x)) # label (non_clause) # label (hedef). [hedef].

2 -P (C (x, y)) | -P (x) | P (y). [Varsayım].

3 P (C (x, K (x, x))). [Varsayım].

5 P (C (C (x, y), C (K (x, z), K (y, z)))). [Varsayım].

7 P (C (x, C (y, x))). [Varsayım].

11 P (C (K (C (x, y), C (z, y)), C (A (x, z), y))). [Varsayım].

12 P (C (N (x), C (x, y))). [Varsayım].

14 P (A (x, N (x))). [Varsayım].

15-P (C (c1, c1)). [inkar (1)].

24 P (C (x, C (y, C (z, y)))). [hiper (2, a, 7, a, b, 7, a)].

55 P (K (C (N (x), C (x, y)), C (N (x), C (x, y)))). [hiper (2, a, 3, a, b, 12, a)].

99 P (C (K (x, y), K (C (z, C (u, z)), y))). [hiper (2, a, 5, a, b, 24, a)].

1001 P (K (C (x, C (y, x)), C (N (z), C (z, u)))). [hiper (2, a, 99, a, b, 55, a)].

11705 P (C (A (x, N (y)), C (y, x))). [hiper (2, a, 11, a, b, 1001, a)].

11723 P (C (x, x)). [hiper (2, a, 11705, a, b, 14, a)].

11724 $ F. [çözüm (11723, a, 15, a)].