Membuktikan $\alpha \implies \alpha$ dapat diturunkan

Question

Saya akan membahas "Topoi" Goldblatt, dan salah satu latihan di sana bergantung pada pembuktian bahwa sistem aksioma tertentu memerlukan $\alpha \implies \alpha$ untuk proposisi apa pun $\alpha$.

Sistem aksioma yang dimaksud adalah sebagai berikut (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 $

Satu-satunya aturan kesimpulan adalah modus ponens biasa.

Jadi, rasanya aksioma (9) bersama dengan (12) bisa digunakan sebagai langkah terakhir penurunan (instantiating $\alpha$ untuk $\alpha$, $\beta$ untuk $\lnot \alpha$ dan $\gamma$ untuk $\alpha \implies \alpha$). Kemudian, sisi kiri file$\land$dalam (9) dapat diturunkan menggunakan (5), dan sisi kanan dapat diturunkan menggunakan (10). Tapi bagaimana cara menggabungkannya di bawah a$\land$? Sepertinya saya tidak punya yang biasa$\land$-pengenalan aturan - sistem aksiomatik yang pernah saya lihat sebelumnya biasanya memiliki sesuatu dalam bentuk $\alpha \implies (\beta \implies (\alpha \land \beta))$.

Juga, menggunakan aksioma (non-konstruktif) dari bagian tengah yang dikecualikan untuk pernyataan yang jelas konstruktif ini terasa salah.

Jadi bagaimana cara membuktikannya? $\alpha \implies \alpha$ dalam sistem ini?

Answer 1

Nah, sebelum saya kehilangannya, inilah yang diberikan Prover9 kepada saya setelah diterjemahkan ke dalam notasi awalan. C (x, y) digunakan sebagai pengganti (x⟹y). K (x, y) bukan (x∧y). N (x) sebagai ganti$\lnot$x. Dan A (x, y) sebagai ganti (x$\lor$y) .:

% -------- Komentar dari bukti asli --------

% Bukti 1 pada 1,19 (+ 0,56) detik.

% Panjang pembuktian adalah 16.

% Tingkat pembuktian adalah 6.

% Berat klausa maksimum adalah 14.

% Diberikan klausul 812.

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

2 -P (C (x, y)) | -P (x) | P (y). [anggapan].

3 P (C (x, K (x, x))). [anggapan].

5 P (C (C (x, y), C (K (x, z), K (y, z)))). [anggapan].

7 P (C (x, C (y, x))). [anggapan].

11 P (C (K (C (x, y), C (z, y)), C (A (x, z), y))). [anggapan].

12 P (C (N (x), C (x, y))). [anggapan].

14 P (A (x, N (x))). [anggapan].

15 -P (C (c1, c1)). [menyangkal (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)). [hyper (2, a, 11705, a, b, 14, a)].

11724 $ F. [menyelesaikan (11723, a, 15, a)].