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.