Re: [請益] 邏輯證明

[MathTurtle (恩典)]

※ 引述《a53530 (Susu)》之銘言：
: 1.(x)(Px≡Qx)
: 2.(x)[Px→(Qx→Rx)]
: 3.(Ｅx)Qx v (Ｅx)Px
: /(Ｅx)Rx v (Ｅx)Sx
: 用→替代horseshoe
:     用v    替代或
:     用^    替代且
:     用(Ｅx)替代有些x
: 我算了好久算不出來
: 請強者幫忙解答
: 將以1000P幣作為酬謝
我來試試。(有些推論規則的名稱我忘了)

1.(x)(Px≡Qx)                   Ass
2.(x)[Px→(Qx→Rx)]             Ass
3.(Ｅx)Qx v (Ｅx)Px             Ass
4. ~(Ex)Px                      Ass for RAA
5. (Ex)Qx                       4, 3. DS.
6. Qa                           5. EI
7. Pa≡Qa                       1. UI
8. (Pa→Qa) ^ (Qa→Pa)          from 7
9. (Qa→Pa)                     8 Simp
10. Pa                          6, 9. MP
11. (x)~Px                      from 4
12. ~Pa                         11. UI
13. Pa^~Pa                      10, 12
14. (Ex)Px                      4-13. RAA
15. Pb                          14, EI
16. (Pb≡Qb)                    1. UI
17. (Pb→Qb)^(Qb→Pb)           from 16
18. (Pb→Qb)                    17 Simp
19. Qb                          15, 18 MP
20. [Pb→(Qb→Rb)]              2. UI
21. (Qb→Rb)                    15, 20 MP
22. Rb                          19, 21 MP
23. (Ex)Rx                      22. EU (note that b was introduced
                                        in 15 by EI, so that's fine)
24. (Ex)Rx v (Ex)Sx             23, Add

--
※ 發信站: 批踢踢實業坊(ptt.cc) 
◆ From: 86.30.200.58
推 dementia:"Ass"改成"Premise"會不會比較好??
→ dementia:"EI"通常會被當成一種assumption 是不是有步驟省略了??
推 dementia:就我所知 應該用Constructive Dilemma比較輕鬆 推出
→ dementia:"(Ex)Rx v (Ex)Rx"再用Tautology得到"(Ex)Rx"就可以了
→ MathTurtle:樓上的解法很漂亮...我都忘了有constructive dilemma
→ MathTurtle:可以用了...