[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Paul, what you observe is a variation of the fact that type theory cannot prove all true \Pi^0_1 sentences. The only variation is that you reformulate it as a type checking problem. As we know from Goedel's 1931 Incompleteness Theorem any reasonably strong system fails to prove true \Pi^0_1 sentences. This applies in particular to realizability models of type theory which are complete in the sense that for every closed type expression A either A or A -> False is inhabited. One point of view of type theory is that it approximates realizability which is a semantic notion. But realizability is a notion whose logical complexity is beyond decidability. Thus, this approximation is bound to be just an approximation. In ordinary logic one is at least free to compensate for this incompleteness by adding axioms. That is not so with type theory where there is also the constraint that the realizers for these axioms have also computational meaning. I agree with you that there is a sort of "formalist" tradition in type theory which identifies validity with provability. Of course, that's not said explicitly but sort of insinuated. Thomas
