Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)?

On the first sight, they aren't, since elements of types are terms and we have only countable number of terms.

Does it mean that sets with cardinality of a continuum really doesn't exist and just a nice abstraction which simplifies mathematics a lot?

  • 2
    $\begingroup$ You should probably take a look at Skolem's paradox: the class of all sets only has countably many elements, when viewed from the "outside" (at least for certain models). $\endgroup$
    – cody
    May 8 '14 at 21:46

You must be careful here. You are using set-theoretic concepts (cardinal, continuum) outside set theory. There is potential for confusion.

Your question can be understood in several ways.

Maybe you are asking whether there can be uncountably many terms of a given type. The answer is: obviously not since there are only countably many finite strings, and eact term is a string (or a finite tree if we think of abstract syntax). You might be asking this question because you claim that "the elements of types are terms". This, in my opinion, is a very damaging view of types. It is like saying that the elements of $\mathbb{R}$ are only certain expressions which denote real numbers.

Another possibility is that you are asking whether there is a model of type theory in which some of the types are interpreted as uncountable sets. The answer is yes, for example the set-theoretic type model in which types are sets. In this case $\mathtt{nat} \to \mathtt{bool}$ has the power of continuum because it is the sets of all infinite boolean sequences.

You could be asking whether inside type theory we can prove that there are types of the cardinality of continuum. In this case the question does not make sense because the notion "cardinality of continuum" is something that only make sense in set theory. You need to rephrase it so that it makes sense in type theory, but there are complications. Cardinality just does not behave the same way in type theory as it does in set theory. For example, you cannot show that cardinals (whatever you think they are) are linearly ordered. But we can still define special cases. Thus we can define the notion of an uncountable type:

Definition uncountable (A : Type) :=
   forall f : nat -> A, exists x : A, forall n : nat, ~ (f n = x).

In words, $A$ is uncountable if for every sequence $f : \mathbb{N} \to A$ there exists $x : A$ such that $x$ is not in the image of $f$. The Baire space $\mathbb{N}^\mathbb{N}$ is uncountable:

Theorem baire_uncountable : uncountable (nat -> nat).
  intro f.
  exists (fun n => S (f n n)).
  intro n.
  intro E.
  absurd (f n n = S (f n n)).
  - auto.
  - pattern (f n) at 1.
    rewrite E.

So, classically this would mean that the cardinality of the Baire space is larger than $\aleph_0$, but as I said, cardinalities inside type theory, and in constructive mathematics in general, behave a lot less nicely than in set theory.

  • $\begingroup$ Shouldn't the definition for uncountable be exists x : A, forall f : nat -> A, forall n : nat, ~ (f n = x)? There is some x which is not in the image of any sequence f? As it reads now, for each sequence f there is an x not in its image (which is not the definition of an uncountable set A). If so, the theorem doesn't appear to hold... $\endgroup$ Jun 15 '17 at 16:36
  • $\begingroup$ No. According to your definition there are no uncountable sets. You have your order of quantifiers backwards. Consider the reals: is there a real $x$ which is not in the image of any sequence? (How about the constant sequence $x, x, x, \ldots$?) $\endgroup$ Jun 15 '17 at 18:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.