[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Are there interesting or commonly used logical axioms that we know for sure > cannot have computational interpretations? PEM (Principle of Excluded Middle) already for equality of functions from N to N. From this you immediately get a decider for the halting problem. Thomas
