[TYPES] decidability vs completeness

[Thomas Streicher]

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