証明 $\alpha \implies \alpha$ 導出可能です

Question

私はゴールドブラットの「トポス」を経験していますが、そこでの演習の1つは、特定の公理システムが必要であることを証明することに依存しています。 $\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 $

唯一の推論規則は、通常のモーダスポネンスです。

したがって、公理（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が私にくれたものです。（x⟹y）の代わりにC（x、y）が使用されます。（x∧y）の代わりにK（x、y）。代わりにN（x）$\lnot$バツ。そして（xの代わりにA（x、y）$\lor$y）.:

％--------元の証明からのコメント--------

1.19（+ 0.56）秒での％証明1。

％証明の長さは16です。

％証明レベルは6です。

％最大句の重みは14です。

％与えられた条項812。

1 P（C（x、x））＃label（non_clause）＃label（goal）。[ゴール]。

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 -P（C（c1、c1））。[deny（1）]。

24 P（C（x、C（y、C（z、y））））。[hyper（2、a、7、a、b、7、a）]。

55 P（K（C（N（x）、C（x、y））、C（N（x）、C（x、y））））。[hyper（2、a、3、a、b、12、a）]。

99 P（C（K（x、y）、K（C（z、C（u、z））、y）））。[hyper（2、a、5、a、b、24、a）]。

1001 P（K（C（x、C（y、x））、C（N（z）、C（z、u））））。[hyper（2、a、99、a、b、55、a）]。

11705 P（C（A（x、N（y））、C（y、x）））。[hyper（2、a、11、a、b、1001、a）]。

11723 P（C（x、x））。[hyper（2、a、11705、a、b、14、a）]。

11724 $ F。[解決（11723、a、15、a）]。