R i c e ' s T h e o r e m f o r t h e M a r t i n - L o f u n i v e r s e Martin Escardo, University of Birmingham, UK. February 2012. This is a proof in intensional Martin-Lof type theory, extended with the propositional axiom of extensionality as a postulate, written in Agda notation. The K-rule or UIP axiom are not used, except in instances where they can be proved. The proof type-checks in Agda 2.3.0. A b s t r a c t. We show that a Martin-Lof universe `a la Russell satisfies the conclusion of Rice's Theorem: it has no non-trivial, decidable, extensional properties. We derive this as a corollary of more general topological facts in type theory, which don't rely on Brouwerian continuity axioms. I n t r o d u c t i o n We don't manipulate syntax or Turing machines to prove this claim. We show, within type theory, that the hypothetical existence of a non-trivial, decidable extensional property of the universe leads to a construction that is known to be impossible, namely WLPO, defined and discussed below. Hence this version of Rice's Theorem for the universe remains true when type theory is extended with any kind of postulated axiom (e.g. univalence, Church's thesis, Brouwerian continuity axioms, Markov principle, to name a few of the contentious axioms that one may wish to consider in constructive mathematics). One possible reaction to our result is that this is to be expected: after all, there are no elimination rules for the universe. But our arguments show that, even if there were, Rice's Theorem for the universe would still hold, which justifies the lack of elimination rules. Of course, if we postulate classical logic, for example in its extreme version given by the principle of excluded middle, then there are decidable properties of the universe. Our theorem is compatible with that. In fact, what our construction does is to produce a classical conclusion from the hypothetical premise. Our assumption of the axiom of extensionality may seem dubious. In any case, we do get a meta-theorem that does not rely on extensionality: For all closed terms p: Set → ₂ with p extensional and X,Y: Set, there is no closed term of type p(X) ≡ ₀ ∧ P(Y) ≡ ₁, where Set is the universe of types and where ₂ is a type with two distinct elements ₀ and ₁, and with decidable equality. We derive this claim as a corollary or more general topological constructions developed in the module TheTopologyOfTheUniverse, which is the interesting and non-trivial technical aspect of this work. We emphasize that we don't postulate any continuity axiom in that module (or in fact any axiom other than extensionality). \begin{code} module RicesTheoremForTheUniverse where open import TheTopologyOfTheUniverse open import Cantor open import CurryHoward open import Equality open import Extensionality open import GenericConvergentSequence open import Isomorphism open import Naturals open import SetsAndFunctions open import Two WLPO : Prp WLPO = ∀(u : ℕ∞) → u ≡ ∞ ∨ u ≠ ∞ \end{code} Navigate to the module GenericConvergentSequence for the definition of the type ℕ∞ and its role. More discussion is included in the module TheTopologyOfTheUniverse. The weak principle of omniscience WLPO is independent of type theory: it holds in the model of classical sets, and it fails in recursive models, because it amounts to a solution of the Halting Problem. But we want to keep it undecided, for the sake of being compatible with classical mathematics, following the wishes of Bishop, and perhaps upsetting those of Brouwer who was happy to accept continuity principles that falsify WLPO. In the words of Aczel, WLPO is a taboo. More generally, anything that implies a taboo is a taboo, and any taboo is undecided. Taboos are boundary propositions: they are classically true, recursively false, and constructively, well, taboos! The following says that a particular kind of discontinuity for functions p : ℕ∞ → ₂ is a taboo. Equivalently, it says that the convergence of the constant sequence ₀ to the number ₁ in the type of binary numbers is a taboo. A Brouwerian continuity axiom is that any convergent sequence in the type ₂ of binary numbers must be eventually constant (which we don't postulate). \begin{code} basic-discontinuity : (ℕ∞ → ₂) → Prp basic-discontinuity p = (∀ n → p(under n) ≡ ₀) ∧ p ∞ ≡ ₁ basic-discontinuity-taboo : ∀(p : ℕ∞ → ₂) → basic-discontinuity p → WLPO basic-discontinuity-taboo p (f , r) u = two-equality-cases lemma₀ lemma₁ where fact₀ : u ≡ ∞ → p u ≡ ₁ fact₀ t = trans (cong p t) r fact₁ : p u ≠ ₁ → u ≠ ∞ fact₁ = contra-positive fact₀ fact₂ : p u ≡ ₀ → u ≠ ∞ fact₂ = fact₁ ∘ Lemma[b≡₀→b≠₁] lemma₀ : p u ≡ ₀ → u ≡ ∞ ∨ u ≠ ∞ lemma₀ s = in₁(fact₂ s) fact₃ : p u ≡ ₁ → (∀ n → u ≠ under n) fact₃ t n s = zero-is-not-one(Lemma[x≡y→x≡z→y≡z](f n)(Lemma[x≡y→x≡z→y≡z](cong p s) t)) lemma₁ : p u ≡ ₁ → u ≡ ∞ ∨ u ≠ ∞ lemma₁ t = in₀(not-ℕ-is-∞ (fact₃ t)) \end{code} Our promised corollary of the universe indiscreteness theorem is that the hypothetical existence of an extensional P : Set → ₂ with two different values is a taboo. \begin{code} extensional : (Set → ₂) → Prp₁ extensional P = ∀(X Y : Set) → X ≅ Y → P X ≡ P Y Rice's-Theorem-for-Set : ∀(P : Set → ₂) → extensional P → ∀(X Y : Set) → P X ≡ ₀ → P Y ≡ ₁ → WLPO Rice's-Theorem-for-Set P e X Y r s = basic-discontinuity-taboo p (p-lemma , p-lemma∞) where Q : ℕ∞ → Set Q = attach (λ i → X) Y Q-lemma : ∀ i → Q [ i ] ≅ X Q-lemma i = attach-lemma (λ i → X) Y i Q-lemma∞ : Q ∞ ≅ Y Q-lemma∞ = attach-lemma∞ (λ i → X) Y p : ℕ∞ → ₂ p u = P(Q u) p-lemma : ∀ i → p(under i) ≡ ₀ p-lemma i = trans (e (Q(under i)) X (Q-lemma i)) r p-lemma∞ : p ∞ ≡ ₁ p-lemma∞ = trans (e (Q ∞) Y Q-lemma∞) s \end{code} Notice that although the proof uses topological techniques, the formulation of the theorem doesn't mention topology. One can get more milleage exploiting the fact that ℕ∞ satisfies the principle of omniscience, as proved in the module GenericConvergentSequence. As a simple example, one can conclude LPO rather than WLPO. The type-inhabitedness predicate is clearly extensional. By the above theorem, this means that there is no algorithm within type theory that decides whether any given type is inhabited, that is, whether a proposition has a proof. Of course we already know this since the time of Godel, Turing and Church, in stronger forms (such as adding general recursion to type theory). But we emphasize again that our development is syntax-free (or Godel-number free), and hence make senses in any model of type theory. We have the following meta-theorem as a corollary, *without* assuming the propositional axiom of extensionality: For all closed terms P: Set → ₂ and X,Y: Set with a given proof of extensionality of P, there is no closed term of type P(X) ≠ P(Y). Proof. Assuming the axiom of extensionality, there can't be such closed terms, as there is a realizability interpretation, e.g. Hyland's effective topos, where WLPO solves the Halting Problem. Without postulating the axiom, fewer terms are definable in the language, and hence the omission of extensionality gives the same result. Q.E.D.