>>12941877Subsets are richer constructively, because predicates are.
If is a set and and unary predicate, then .
E.g. if then the four decidable predicates "always always true", "is even", "is odd", "is always false" give rise to the found subsets , , , A={}, . Generally, on a set of cardinality n, there are 2^n characteristic functions and thus at least 2^n subsets.
But since predicates don't collapse to mere characteristic functions if you adopt excluded middle ("let's make everything decidable"), the constructive power class, i.e. the class of all subsets of A, is generally far greater than the function space of characteristic functions.
You might think of subsets of sets as corresponding to described but not necessarily terminating processes, whereas "function" means the nice terminating case.
Constructively, to prove a disjunction requires you to be able to prove one of the disjuncts. If you got an undecidable predicate, let's say the continuum hypothesis is one in our context, then classically is true (per axiom LEM), while without LEM it's just as undecidable as itself.
As a consequence, if you got a singleton, say , then is classically just , but constructively we can neither judge it to be nor . Subsets are richer constructively, because predicates are.
To be finite means to be in bijection with an n in N. If we don't know about any of the elements of a subset, we can't put it into bijection with any set. So the subset of A may fail to be finite, even if A is.
LEM trivializes predicates and thus subsets.
