Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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?

share|improve this question
2  
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). –  cody May 8 at 21:46

1 Answer 1

up vote 13 down vote accepted

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).
Proof.
  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.
    reflexivity.
Qed.

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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