※ 引述《maylaw (討厭傲嬌)》之銘言： : ※ 引述《MathTurtle (恩典)》之銘言： : : 一命題是否為一個恆「真」句, : : 有時要看你給的 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 不是可證的。 : 如果一個語句具有可證性，則是因為它有真假可言。不具有真假可言的語句還談 : 什麼恆真恆假？形式邏輯的系統只適用於有真假可言的語句，你拿沒有真假可言 : 的語句作為例子不是很奇怪嗎？形式邏輯的效力有限，它並不能百分之百吻合我 : 們的思維，這我想所有的邏輯學家都會承認。 為何我拿了沒有真假可言的語句作例子呢? 假設p表示「任何大於2的偶數皆為兩個質數的和。」, 這個命題是有真假可言的: p為真, 若且惟若, 任何大於2的偶數皆為兩個質數的和。 但是p目前沒有被證出來, 它的反命題~p, 也就是「存在一大於2的偶數不是兩個質數和」 也沒有被證出來, 因此如果我們用有沒有被證出來, 來詮釋Kripke semantics中以「可證」給出logical connectives的semantics, 那麼, pv~p在這裡是不成立的。 這裡我們還是要區分, 「可證」作為Kripke semantics的一種詮釋方式, 以及「可證」作為實際上的證明。 前者只是一種我們在meta-theory中所給予某一特定proof theory (如: natural deduction of intuistic logic)的semantics。 這有點confusing我知道, 因為「可證」拿來當成了semantics的概念, 這也是為何我其實不太喜歡用可證來詮釋Kripke semantics, 還是比較偏好用possible world semantics來詮釋。 : 另外就是恆真句是否可引入推論之中的問題，很抱歉我看的書比較少，目前看到 : 有人這樣用的就是Stephen F. Barker，他寫的邏輯書"The Elements of Logic" : ，有這樣的用法。 他這麼用, 我猜, 是建立在兩個假設上: 1. 這裡的系統是古典邏輯(classical logic), 而古典邏輯我們知道是完備的。 2. 這系統含有某種類似於cut theorem的meta-theorem (或structure theorem)。 把它符號化後, 這兩個假設分別是: 1. 若p是tautology, 則 |- p; 2. 若 Γ |- p 且 Γ, p |- q, 則 Γ |- q。 作為基本邏輯的教科書, 或許作者不會把這兩個 "meta-theorem"加以證明, 不過他的確是應該交待一下, 引入恆真句作為前提, 我們會需要這兩個定理成立, 而1.在很多系統中不成立是大家都知道的(如: 代數系統, 某些二階邏輯等等), 而2.雖然作為structure theorem在大部份的proof theory都會成立, 但在很多proof theory之中是需要假設它來characterise一個proof的概念是什麼。 而雖然intuistic logic在Kripke semantics下是完備的(我應該沒記錯), 但提到intuistic logic是一個直接可以指出在證明中引入 R v ~R 可能會有的問題。 : 雖然我沒辦法舉出有哪些邏輯學家這樣用，但是我們其實也是這樣在做推論的。 : 當我們知道一個斷言會導出矛盾的時候，我們就會說那斷言不成立。例如懷疑論 : 者主張：「我什麼都不知道」，則有人馬上會回應：「那對於『你什麼都不知道』 : 的這件事情你知不知道呢？如果不知道的話，那你說出的話則無意義，如果你知 : 道的話，則你就不是什麼都不知道，你至少知道了一件事情。」 : 我舉的例子可能形式上不太吻合，也請大家不要去深究那個例子，否則便是 : 離題。我想說的是，我們的確會這樣在思考，下列以"P"&"Q"表有真假可言 : 的陳述，箭頭表若則符號。 : 主張P會導出矛盾，我們便會說主張P不成立，符號化的話就是： : P→(Q&～Q) : ∵～P : 上述我們省略了的步驟便是否定那個矛盾句，矛盾句的否定就是恆真句， : 然後再用否定後件則否定前件的規則，我們平常就是這樣在思考的，而形 : 式邏輯便是在明示出我們如何思考，若我們平日就是這樣在推論的，怎麼 : 可能符號化後就不能這樣做推論呢？當我們平常在說：「這樣矛盾」的時 : 候，我們的意思也蘊含了怎麼樣做才不矛盾，但我們有先證明這不矛盾怎 : 麼來的才開始推論嗎？ 上面所講的「主張P會導出矛盾，我們便會說主張P不成立」 或許爭議比較不大, 但它並無法用來證明 (R v ~R) 會成立, 因為它只能用來證明某個東西「不成立」, 而無法證明某個東西「會成立」。 而要能夠證明 (R v ~R)的, 通常是另外一個看起來類似, 但不太一樣的思考過程, 即: 「主張P的否定會導出矛盾, 我們便會說P是成立的」 也就是 ~P |- (Q&～Q) 則 |- P. 這個思考過程正好就是直覺主義所不接受的 RAA證明。 因為在某種詮釋下, 主張~P會導出矛盾, 是主張~P無法在這系統中被接受, 或許這表示~~P是成立的, 但這和直接宣稱P是成立的, 即 P 為定理, 是不一樣的。 這差別的關鍵也許是和negation的意義有關(在natural deduction中可以這樣理解), 但在某些直覺主義者的看法中, 更是較為原初的認為RAA的理解是有問題的, 因為你只能宣稱你不接受~P, 但你無法因此強迫任何人去接受P, 中間所需要的, 正是古典邏輯認為理所當然的歸謬, 而直覺邏輯認為是屬非建構式的理解, 而因此不能被接受。 : 另外，回應前文推文的問題。其實我們實在不需要去談什麼定義不定義一 : 隻紅螞蟻，這邊請拿剃刀把它剃掉；對於S大的問題，我只說那隻螞蟻紅 : 色的部份就不會是黑色的，那隻螞蟻黑色的部份就不會是紅色的。你也許 : 會說這是廢話，但對於這個問題的回答也就只能這樣。 --

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