我覺得重點在於, 在一個proof theory裡(例如: natural deduction), 引入恆真句並不是一件理所當然的事情, 你通常會需要一些meta-theory來允許你這麼做, 其中一個可能會用到的, 如: 完備性定理, (即: 凡是真的皆可以被證明) 不見得在每一個系統中都成立。 換言之, 恆真句就算是「不管在什麼情況下都會為真」, 也不保證你能在你的系統當中證出它來, 如果你的系統證不出某個恆真句, 你就無法合法地引入它作為你的前提。 如此例中, 如果你的系統證不出 R v ~R, 那麼你無法引入 R v ~R 作為前提。 而的確在直覺主義的自然演譯法中, (briefly, 不能使用RAA的自然演譯法), 你是證不出 R v ~R的。 ※ 引述《maylaw (討厭傲嬌)》之銘言： : ※ 引述《aletheia (cOnJeCTuRe)》之銘言： : : 你這樣說不太對 : : 直覺主義認為排中律並不成立 : : 對於他們來說 (φvψ)指的是 : : "φ可以建構出一個證明或者ψ可以建構出一個證明" : : 對於(pv~p)來說 : : 除非能說明所有的句子與其negation不能皆同時找到證明 : : 那不能說明排中律成立 : : 另外我也覺得自然演繹法在過程中直接放入恆真句怪怪的 : : 有書可以參考一下嘛 我只知道Gentzen版本的 : 「直覺主義認為」是「直覺主義者認為」，只有理性生物會思考，才會認為； : 主義本身不會「認為」。 : 所以目前問題區分成兩個部份，是不是有恆真句的問題， : 跟恆真句能否直接引進推論的問題： : 1.恆真句是存在的嗎？ : 你這段話： : "φ可以建構出一個證明或者ψ可以建構出一個證明" : 對於(pv~p)來說 : 除非能說明所有的句子與其negation不能皆同時找到證明 : 我看不懂在說什麼，可否舉例輔助？ : φ可以建構出一個證明，究竟是以φ為前提來做出論證證明其他陳述？ : 還是以φ為結論，可用論證來證明φ為真？ 一命題是否為一個恆「真」句, 有時要看你給的 semantics是什麼, aletheia的這句話, 是直覺主義對logical connectives (not and if), 所給出的一種可能的semantics, 我們通常稱為 Kripke semantics。 用「可證性」來理解一句子的「真」, 是一種對Kripke semantics的理解方式, 也就是說, ~φ 為「可證」, 若且惟若, 在以後時間中都不會找到φ為「可證」, 而因此, (pv~p)有可能在 p不為「可證」, 同時~p也不為「可證」的情形下, (pv~p)也不為「可證」。 舉例而言, 我們把哥德巴赫猜想寫成命題p, 在這詮釋下, p不是可證的, ~p也不是可證的, (雖然未來某刻可能其中一個會被證出來) 而因此 p or not p 不是可證的。 : 話說恆真句對我們而言沒有成立或不成立的問題，恆真句不管在什麼情況下都會為真， : 因此它並不從任何有別於它的陳述句導出來，也就是它的真並不依賴於其他敘述、現象、 : 事物等。因此恆真句的真假也不需要被檢證。它也無法提供我們任何資訊，例如「白色 : 的牆壁是白色的」，一般我們都會說：「啊這不是廢話嗎？」不過這是不是為真？是！ : 至於所謂的排中律，若舉個例子來講：「螞蟻是紅色的或螞蟻不是紅色的」，也是恆真句 : ，除了紅色跟不是紅色以外，還有第三種可能嗎？有可能既是紅色的又不是紅色的嗎？ : 尤其這段話： : 「除非能說明所有的句子與其negation不能皆同時找到證明，那不能說明排中律成立」 : 以上述的螞蟻作為例子，我想問問直覺主義：「你能找到一隻同時既是紅色的又不是紅 : 色的螞蟻嗎？」，沒有任何事物存有這樣的矛盾，你不能把陳述分開來看，不能找一隻 : 不是紅色的螞蟻，跟一隻是紅色的螞蟻，然後告訴我：「我同時證明這螞蟻是紅色的跟 : 另一隻螞蟻不是紅色的」，問題是那是兩隻，但是當我說「螞蟻不可能既是紅色的又不 : 是紅色的」，這時候我是講同一隻螞蟻。你要拿兩個不同的個例，然後做出兩句陳述， : 以選言符號擺在一起當然不會有矛盾，但是當我們陳述同一個例的時候，我們是不可能 : 找到既是肯定它如何如何，又否定它如何如何，的矛盾例子，這是不可能的。 : 至於能否引入恆真句證明容我下次再說，上班去～～ (p & ~p)的不成立, 與 (p v ~p)的成立, 在直覺主義當中是兩回事, 大部份的直覺主義不接受 (p & ~p) (除非你是paraconsistent logic) 但卻也不接受 (p v ~p)。 [矛盾律與排中律是不一樣的, 要從矛盾律導排中律, 你可能要預設某些東西] 而如果你想要從, 假設排中律不成立, 我們可以找到矛盾, 因此排中律成立, 這剛好就是直覺主義者不接受的 RAA 證明方式。 --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 81.101.138.175 ※ 編輯: MathTurtle 來自: 81.101.138.175 (01/11 12:22)