Re: [問題] 關於universal generalization 的restr …
※ 引述《rodyforeter (rodyforeter)》之銘言：
: 標題: Re: [問題] 關於universal generalization 的restr …
: 時間: Sat Jul 3 08:58:17 2010
:
: OK 所以我想CP 的這種情況是可以做UG
:
: 那麼我又想 IP 的這種情況會是如何？？？？
:
: 假設有個論證如下:
:
: 1. /
:
: 2.~Ax AIP
: 3.
: 4.
: 5.
: 6.Ax 2-5IP
:
: 重點來了 這裡6.的自由變元可以做UG嗎？
:
: 我認為應該不行...難道有什麼神乎其技的方法能夠像CP那樣把這裡也做UG？
其實兩個都可以。
所謂 CP/IP證明的限制, 是指說在還沒有關起來的中間做UG,
像是以下兩種證明都是不行的:
1. Fx ACP
2. (x)Fx UG
3. Fx->(x)Fx CP
4. (x)(Fx->(x)Fx) UG
其中第二步的UG是不行的。
1. (Fx & ~Fa) ACI
2. (x)(Fx & ~Fa) UG
3. (Fa & ~Fa) 2, UI
4. ~(Fx & ~Fa) 1-3 CP
5. (x)[~(Fx & ~Fa)] 4, UG
這裡第二步的UG也是不行的。
而你說的那種情況做UG是可以的。因為UG其實是以下的後設定理的運用:
Theorem: If a formula φ(x) with x as its free variable can be proved,
then the formula (x)φ(x) can be proved。
而運用這個meta-theorem, 在你提到的CP和IP的證明當中其實是可以用的。
:
: --
: ※ 發信站: 批踢踢實業坊(ptt.cc)
: ◆ From: 61.231.226.220
: ※ 編輯: rodyforeter 來自: 61.231.226.220 (07/03 09:01)
: → a3435357:5錯了，應該是Bz 07/03 10:06
: → a3435357:可能沒有這個必要，ip證法通常是假設結論的否定，求矛盾 07/03 20:59
: → a3435357:因為有矛盾故推翻假設，結論因此而得證，當run完一回ip證 07/03 21:00
: → a3435357:證明也結束了，也沒有做UG的必要 07/03 21:01
這個講法應該沒錯。
假設我們有一個證明, 是在做後一步用UG, 如以下形式:
1. ~φ(x)
...
... contradiction
n. φ(x) IP
n+1. (x)φ(x) UG
我們總是相對應的有以下的證明:
1. ~(x)φ(x)
2. (Ex)~φ(x)
3. ~φ(a)
...
... contradiction
n. (x)φ(x) IP
這應該很容易在自然演譯法的系統中當成一個後設定理證明出來。
這裡主要的原因是, 如果在你的自然演譯法系統中, 兩個量詞 (x)和(Ex)
都是原初, 且你又有EG, UG, EI, UI, 而且你還有兩者轉換的公式,
那麼其實它會有些是多餘的, 因為UG其實相應於EI。
而如果你想要讓你的系統簡單一點, 像很多邏輯書的作者會這麼做,
你可以只保留universal quantifier, 然後定義 (Ex) 為 ~(x)~
這麼做的話, 你有的是UG和UI而已, 也就是量詞的introduction rule
和elimination rule (這也比較符合自然演譯法的精神),
那麼你會發現你會需要在某些證明的最後一步做UG,
而無法直接假設否定導矛盾。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 81.107.38.67
推
07/04 07:54, , 1F
07/04 07:54, 1F
→
07/04 07:55, , 2F
07/04 07:55, 2F
這邊如果你的1只是假設的前提, 而你還沒證出什麼東西來時,
是不能做2.這一步的。
→
07/04 07:58, , 3F
07/04 07:58, 3F
→
07/04 08:00, , 4F
07/04 08:00, 4F
※ 編輯: MathTurtle 來自: 81.107.38.67 (07/04 19:06)
討論串 (同標題文章)
本文引述了以下文章的的內容：
完整討論串 (本文為第 10 之 10 篇)：