Does "Church's Law" really fail in Extensional Type Theory?

Question

Last year Bob Harper wrote a blog post about the failure of "Church's Law" in Extensional Type Theory[1]. However his statement of the law looks to me more like an internal version of the statement "all functions are computable" and I am not surprised that this turns out to be false.

To falsify the law I would have imagined that it would be necessary to set up two general internal models of computation, both of which we believe cannot be extended further whilst retaining their "algorithmic" character, and then proceed to show, internally, that these models of computation are distinct.

Is the issue here just two different interpretations of what "Church's Law" should mean internally, or is there really something deeper going on that I don't understand?

[1] http://existentialtype.wordpress.com/2012/08/09/churchs-law/

Answer 1

I think there's a terminological distinction at work here. "Church's Thesis" (also called the Church-Turing Thesis) says that the intuitive notion of computability agrees with (or "is adequately captured by") its various proposed formal versions (Turing computability, lambda definability, representability in various formal theories, etc., all of which a provably equivalent to each other). The "Church's Law" mentioned in your question, on the other hand, says that all functions from natural numbers to natural numbers are computable (in one of the formal senses mentioned above). This is inconsistent with classical arithmetic (i.e., one can prove the existence of non-computable functions) but consistent with constructive systems and is sometimes assumed as an addition to the basic axioms of constructive arithmetic (and type theory).