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$.
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?
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?