Criteria for "constructive" in this question: Given a formal system and all the models that satisfy the axiomatic systems of interest (e.g. all models of ZF without choice), any object being constructed can be proved to exist/not exist and the proof is written only in terms of the sequence of axioms (and theorems derived from them) being used, and rejecting the law of excluded middle.

In ZF set theory where axiom of choice is absent, it is consistent that there exists amorphous and infinite dedekind finite sets, although we cannot prove them because we can construct models where they exist and models where they don't.

$S$ is infinite dedekind finite, or strictly dedekind finite if it does not biject with any initial section of the naturals (not of finite cardinality) and there exists no map that can inject $S$ into any of its subsets.

In particular, it is consistent that there can exist infinite dedekind finite subsets $S$ of the reals.

After discussing in the chat, it was found that $S \subsetneq \Bbb{R\setminus Q}$ and that $S$ consists of both a countable subset and another infinite dedekind finite set.

But that raised a question: It is known that any irrational $r$ is a rational distance away from some other irrationals $s$, therefore this will mean for any subset of irrationals, there always exists a nonzero rational $q$, not necessary unique, such that $s=r+q$ for any pairs of $r,s \in S$. Since $\Bbb{Q}$ is countable regardless of choice, it seems $\{s : s=r+q\}$ will always form a countable subset for any candidate $S$, thus leading to the conclusion that there cannot be any such $S$.

  1. What is an explicit example of an infinite dedekind finite subset of the reals in models of ZF where they can be proved to exist. More generally, what well known models of ZF will allow the existence of such sets be provable and also constructible explcitly via an algorithm or procedure?

  2. How to show that objects defined using both axiom of choice or its negation can never be constructive, is there a well known reference for such proof?

  • 2
    $\begingroup$ "In ZF set theory where axiom of choice is absent, there exists amorphous and infinite dedekind finite sets.", no, ZF is syntax and existence is semantics. Moreover, this seems to hint that the existence of DF sets is provable without choice, which it most certainly isn't. Even rejecting countable choice doesn't necessarily mean that you can prove there are DF sets. $\endgroup$ – Asaf Karagila Oct 15 '17 at 7:30
  • 1
    $\begingroup$ Also, you keep writing $\Bbb{R/Q}$, but I think you mean $\Bbb{R\setminus Q}$. $\endgroup$ – Asaf Karagila Oct 15 '17 at 7:31
  • 1
    $\begingroup$ The three questions, overall, seem to be quite confused upon first reading, specifically about what the nature of sets of reals in a universe of set theory, and what does mean to have an explicit construction. The third question starts with a blatantly false statement, and also seems to be very confused. Using the negation of AC is the same as using AC. And the set {x : x=0 and CH holds or x=1 and CH fails} does not use the axiom of choice, is provably a singleton, but requires the LEM in order to be determined in full. Since you cannot constructively tell me its element. $\endgroup$ – Asaf Karagila Oct 15 '17 at 7:34
  • $\begingroup$ "$S$ consists of both a countable subset and another infinite dedekind finite set." What? Any set with a countably infinite subset is not Dedekind finite ... $\endgroup$ – Noah Schweber Oct 16 '17 at 15:48
  • $\begingroup$ It was brought to my attention that instead of interacting with my comments, you posted them on the chat and had a small interaction there with someone. Did that help to dispel some of the problems? Do you feel that your questions have been answered (or alternatively, that some significant edits should be made in order for the question to be less "confused by foundations and related terminology")? It is just common courtesy to reply to someone that tried to give some critique to your question (and definitely not in a bad way)... $\endgroup$ – Asaf Karagila Oct 16 '17 at 21:42

As far as constructivity, Arnie Miller has a proof that it is consistent to have a Borel set which is [infinite] Dedekind-finite.

Miller, Arnold W., A Dedekind finite Borel set, Arch. Math. Logic 50, No. 1-2, 1-17 (2011). ZBL1225.03061.

In fact this Borel set is relatively low in the hierarchy, it is an $F_{\sigma\delta}$ set.

As far as "constructive", I guess this is more or less the best you can get. In the same paper he shows that it's impossible to get it from a lower stage of the Borel hierarchy.

If this answer does not satisfy you, then I'm afraid that there isn't much more we can say. Let me explain why by answering the second answer.

Suppose that $\varphi(x)$ is some formula which defines a set. And now you want to ask if the set it defines is provably such and such. For example, is it provably a finite set of ordinals, or provably a set of reals (for some canonical coding of the reals into sets).

Some formulas define things like that. Like the set of rational numbers, or the set of reals which are constructible in Gödel's sense.

But now we run into independence. In some models, we can show that no formula defines a Dedekind-finite set (or some other set whose existence defies the axiom of choice). Simply because in those models the axiom of choice holds, or sufficient fragment of it holds. And in some models we can prove that a certain set with a certain property does in fact exist.

This means that it is impossible, without the axiom of choice, to prove or disprove that $\varphi(x)$ defines a set with a certain property.

And it can get worse. Just assuming the failure of the axiom of choice, we can prove that Zorn's lemma fails. But we cannot point at a specific example, since the axiom of choice consistently holds up to some rank in the universe, and only fails very high. So anything you might want to define and prove that it "has to be a counterexample to Zorn's lemma" is going to fail.

In other words, the definitions "$\alpha$ is the least such that $V_\alpha$ is not well-orderable" and "$\alpha$ is the least ordinal such that $\mathcal P(\alpha)$ is not well-orderable" might be such that just assuming choice fails ensures that this $\alpha$ exists; but there is no algorithm for finding it, because we can always find models where choice fails above this $\alpha$. And the same is true for many other definitions of this sort.

| cite | improve this answer | |
  • $\begingroup$ Thanks for the detailed answer and guidance. This will surely help me to be aware on how to check whether an object is constructive, predicative or nonconstructive, which will be useful when working in constructive and/or predicative mathematics and in determining whether it is possible to find (counter)examples to some given formula algorithmically $\endgroup$ – Secret Oct 17 '17 at 13:08

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.