[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Relatedly, both MLTT and Nuprl's meaning explanations refute Church's > Thesis if formulated internally (not only does it fail to hold, it is > false). Really? How does (pure!) MLTT refute Church's Thesis? Oh, you're interpreting it like this: ∏ (f : N → N) ∑ (e : N) ∏ (n m : N) (Id(f n, m) ↔ ∑ (k : N) T(e, n, k) × Id (U k, m) ? This says: "For every function f there is a machine e, such that f(n) = m is equivalent to there existing a run k of e on input n which results in output m." Cruicially, because we're using pies and sigmas, e depends on f in an extensional way, i.e., we can extract a map godel : (N → N) → N which calculates such an e, given f. But that's not a contradiction yet. How do you get a contradiction? With kind regards, Andrej
