To be or not to be, that is the question !

To be (true) or not to be (false), that is really the question! 有一天要弄懂 set theory, type theory, mathematical logc 這些東西 _A_

現在 ZFC, ZF, CZF, IZF, CTT, ITT, ETT, OTT, UTT, IL 這些把我弄得昏頭轉向的了,更別提那些 predicativity, extensionality, definable, deriviable, K axiom, proof irrelevance …

初步認知是 proof irrelevance 等於 law of excluded middle,既然 proof 只有分「有」跟「沒有」也就是 true, or false, 而既然只有這兩種 case,LEM 自然就會有,難怪可以在 proof-irrelevance type theory 下詮釋完整的 ZFC …

Advertisements

2 thoughts on “To be or not to be, that is the question !

  1. > 既然 proof 只有分「有」跟「沒有」也就是 true, or false, 而既然只有這兩種 case,LEM 自然就會有

    我的直覺上原因好像沒這麼單純呢?否則同樣的論證也適用於 intuitionistic logic:一個 type 要嘛是 inhabited 要嘛不是。

    可以多說一點嗎?:)

  2. 或許我應該這樣說 …
    將 Prop 看作只有兩種一個是 true, 一個是 false, 分別對應 top 跟 bottom

    [_] : Bool → Set
    [ true ] = ⊤
    [ false ] = ⊥

    接下來 …

    EM : (p : Bool) → [ p ] ⊎ ¬ [ p ]
    EM true = inj₁ tt
    EM false = inj₂ λ ()

    跟 intuitionistic logic 的情況不大一樣吧?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s