[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear all, It is relatively well-known that the meaning explanations of Martin-Löf dependent type theory (MLTT) justifies many inference rules that may not be included in the formalism (the reflection rule, for instance). However, do the meaning explanations also justify (via the proposition-as-types correspondence) the invalidation of that law of excluded middle for all types? In other words, is the judgment ¬Π(A : U) A + ¬A true validated by the meaning explanations? I am strongly inclined to believe that the answer is 'yes'. Please correct me if I am wrong: because MLTT proves that H : Σ (P : A -> U) ¬Π(x : A) P(x) + ¬P(x) ⊢¬Π(A : U) A + ¬A true it is sufficient to demonstrate the validation of the categorical judgment Σ (P : A -> U) ¬Π(x : A) P(x) + ¬P(x) true For this task we are required to exhibit a pair with a closed predicate P : A -> U such that we have a closed proof of ¬Π(x : A) P(x) + ¬P(x). Now let A := nat and P := Σ (i, x : nat) T(e,i,x), where 'T' stands for Kleene's predicate. Given the meaning of the negation sign, the matter amounts to the question H : Π(e : nat) (Σ (i, x : nat) T(e,i,x)) + ¬(Σ (i, x : nat) T(e,i,x)) ⊢ empty true ? but there can be no such closed term H, otherwise we would have a decision procedure for the halting problem. Could anyone kindly confirm if this is correct? Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/
