[TYPES] Meaning explanations and the invalidity of the law of excluded middle

[Ahmad Salim Al-Sibahi]

Dear Bruno,

As far as I understand, MLTT is not anti-classical so it leaves it open whether the law of excluded middle or its converse can be added to the theory without losing consistency. That is, you can add ` Π(A : U) A + ¬A true` and get a consistent classical system; so traditionally “¬Π(A : U) A + ¬A true” should not be derivable in MLTT.

Kind Regards/Med Venlig Hilsen,
Ahmad Salim


D. 12/10/2017 11.19 skrev "Types-list på vegne af Bruno Bentzen" <types-list-bounces at LISTS.SEAS.UPENN.EDU på vegne af b.bentzen at hotmail.com>:

    [ 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/