I can answer this question positively modulo an assumption whose consistency strength I do not know. Roughly speaking, I need a $\beta$-model of $\mathsf{KP}(\mathcal{P})+$"there exists a Reinhardt cardinal". All I know is that the existence of a rank-into-rank cardinal (or an actual Reinhardt, since this construction can be done on the level of definable classes) is good enough. It's likely that somebody who knows more would be able to sharpen this result.
What I need precisely is that there exists a transitive set $M$ such that
- $M$ satisfies adjunction (i.e., for any sets $x,y \in M$, the set $x \cup \{y\}$ is in $M$),
- $M$ satisfies $\Delta_0$-comprehension,
- $M$ is a $\beta$-model (i.e., any internally well-founded set relation is externally well-founded),
- the ordinal rank functions on well-founded relations and on sets are definable in $M$,
- for every ordinal $\alpha \in M$, the set $V_\alpha^M$ of all sets in $M$ of rank less than $\alpha$ is an element of $M$, and
- there is a proper elementary self-embedding $f : M \prec M$ with critical point $\alpha$ (i.e., $f$ moves some rank up, and $\alpha$ is the smallest ordinal in $M$ such that $f(\alpha) > \alpha$).
Note that for any set $x \in M$, the Cartesian product $x \times x$ is an element of $M$. This is the standard argument that powerset and comprehension are enough to get the existence of Cartesian products. We need adjunction to make sure that Kuratowski ordered pairs exist and to ensure that the height of $M$ is a limit ordinal.
Given $f$, construct a sequence of structures $(N_i)_{i<\omega}$ by setting $N_0 = M$ and choosing each $N_{i+1}$ so that $(N_{i+1},N_i)\cong (M,f(M))$. Let $N = \bigcup_{i<\omega}N_i$. Clearly we have that $N \equiv M$.
$f$ induces an automorphism $j$ on $N$ defined by sending each element $a$ of $N_i\cong M$ to the element corresponding to $f^{-1}(a)$ in $N_{i+1}$. Now we have that $\alpha \in N$ is an ordinal rank with $j(\alpha) < \alpha$, so we can apply the Boffa construction of a model of $\mathsf{NFU}$, i.e., we build a structure $A$ whose underlying set is $V_\alpha^N$ with an element-of relation $x\in^\ast y$ which holds if and only if $j(x) \in y\wedge y \in V_{j(\alpha)+1}^{N}$.
$\Delta_0$-comprehension is all that we need to ensure that this structure is a model of $\mathsf{NFU}$. By a result of Holmes, $\in$ and the restriction of $j$ to $V_\alpha$ are definable in $A$. (All that this argument needs is that the set $E=\{(\{x\},x): x \in j(V_\alpha^N)\}$ is in $N$, which ensures that $j^3(E)$ is in $V_{j(\alpha)+1}^N$. This follows from the earlier remark regarding Cartesian products.)
Now we need to relate binary relation that $A$ thinks are well-founded to binary relations that $N$ thinks are well-founded. Let $r \in V_\alpha^N$ be a binary relation on some set $x\in V_\alpha^N$. Since $\in^\ast$ and $\in$ agree on the subset relation and on what Kuratowski ordered pairs are, we have that $A\models$"$r$ is well-founded" if and only if $N \models$"$r$ is well-founded". (Note though that $\in^\ast$ and $\in$ disagree about what the elements of $x$ are, but this doesn't actually matter.)
We will also need the following claims.
Claim 1. If $\gamma \in N$ is an (internal) ordinal such that for all $\delta \leq \gamma$, $j(\delta)=\delta$, then $(\gamma, <)$ is (externally) well-founded.
Proof. This follows immediately from the fact that any element of $N$ fixed by $j$ must be an element of $N_0\cong M$, which is well-founded. $\square_{\text{claim}}$
Claim 2. If $r \in N$ is a binary relation on some set $x \in N$, then $(x,r)$ is externally ill-founded if and only if either $N \models$"$r$ is ill-founded" or there is some $b \in x$ such that $N \models j(\mathrm{rk}(b)) < \mathrm{rk}(b)$.
Proof. If $N \models r\text{ is ill-founded}$, then clearly $(x,r)$ is externally ill-founded. If there is some $b \in x$ such that $N \models j(\mathrm{rk}(b)) < \mathrm{rk}(b)$, then $r$ has a rank function with values in an ill-founded ordinal. Since the theory of $M$ (and therefore also the theory of $N$) knows that the set of ranks occuring in $(x,r)$ is an initial segment of the ordinals, we have that $(x,r)$ is externally ill-founded.
Now suppose that $N \models r\text{ is well-founded}$ and for every $b \in x$, $j(\mathrm{rk}(b))=\mathrm{rk}(b)$. By Claim 1, we have that $(x,r)$ has a rank function with values in a well-founded ordinal, wherefore $(x,r)$ itself is well-founded. $\square_{\text{claim}}$
So for any $x,r \in A$ (i.e., in $V_\alpha^N$) with $r$ an externally ill-founded binary relation on $x$, either $A \models$"$r$ is ill-founded", in which case this is witnessed by some set in $A$, or we can consider the sub-class
$$\{y \in x : (\exists \gamma \leq \mathrm{rk}(y))j(\gamma) < \gamma\}$$
which contains no $r$-minimal element and so witnesses that $r$ is externally ill-founded. So we have that $A$ is a $\beta$ish-model of $\mathsf{NFU}$.
I don't know whether $A$ satisfies the stronger version of the $\beta$ish-model condition that you mentioned. At its face, it seems like it might at best have it for "$\in$-$\Delta_0$-definable" classes.
By strengthening the theory of $M$ you can strengthen the resulting theory of $A$. Since the automorphism $j$ can't touch $\omega$, the requirements I've written imply that $M$ satisfies the (von Neumann ordinal) axiom of infinity, so $A$ will also satisfy the (Frege cardinal) axiom of infinity. ($\mathsf{NFU}+\neg\mathrm{Inf}$ implies that every set is Dedekind finite. Whatever $\omega$ turns into will not be Dedekind finite. Amusingly, I can't actually see a way to construct a $\beta$ish-model of $\mathsf{NFU}+\neg\mathrm{Inf}$.) $A$ should also satisfy the axiom of counting (i.e., that the set of finite cardinals is strongly Cantorian).
As for $\mathsf{NF}$ itself, Holmes's (tentative) proof that $\mathsf{NF}$ is consistent is a compactness argument, and to me there's no clear way to modify it to control well-foundedness of parts of the resulting model. EDIT: See the discussion in the comments.
A common strategy in constructive mathematics is to define how to things can be different rather than just defining how things are the same.
Consider a local ring. One definition of a local ring is a ring where $0 \neq 1$ and where for all $x, y$, if $x + y = 1$ then either $x$ or $y$ is a unit. Equivalently, one can define a local ring to be one where $0$ is not a unit and where if $x + y$ is a unit, then either $x$ or $y$ is a unit.
In classical mathematics, one can equivalently characterize a local ring as a ring in which $\{(x, y) \mid x - y$ is not a unit$\}$ is an equivalence relation. This is a rather nice result because it provides a rather pithy description of a local ring.
In constructive logic, we actually want to flip this on its head.
An apartness relation $R \subseteq A^2$ is a relation satisfying three properties:
- Irreflexivity: $\forall x \in A$, $\neg (xRx)$
- Symmetry: $\forall (x, y) \in R, y R x$.
- Not sure what to call this one: $\forall (x, y) \in R \forall z \in A (xRz \lor yRz)$
An equivalence relation on $A$ describes a sense in which two elements of $A$ can be said to be "the same". Conversely, an apartness relation on $A$ describes how two elements on $A$ can said to be "distinguishable".
Note that the complement $A^2 \setminus R$ of an apartness relation is an equivalence relation. In classical logic, an apartness relation is exactly the complement of an equivalence relation.
This suggests another definition of a local ring. A local ring is a ring where the relation $\{(x - y) \mid x - y$ is a unit$\}$ is an apartness relation.
This is the version that is constructively valid.
Clasically, one can further define a field to be a ring in which the relation $\{(x, y) \mid x - y$ is not a unit$\}$ is exactly the equality relation.
Constructively, the correct definition of a field is a local ring where the complement of the apartness relation $\# = \{(x, y) \mid x - y$ is a unit$\}$ is exactly the equality relation. An apartness relation whose negation is equality is known as a "tight apartness relation". We use $\#$ as a stronger version of $\neq$ - $\#$ is typographically similar to $\neq$.
The statement that an apartness relation is tight is the statement that if two elements cannot be distinguished using the given apartness relation, then they are identical.
We see that $x \# 0$ if and only if $x$ is a unit. Now suppose that $x \cdot y \# 0$. Then we see that $xy$ is a unit. Then both $x$ and $y$ are units. Then $x \# 0$ and $y \# 0$. In other words, if $xy$ is apart from $0$, then both $x$ and $y$ are apart from $0$.
Conversely, if $x \# 0$ and $y \# 0$, then both $x$ and $y$ are units; thus, $xy$ is a unit; and therefore, $xy \# 0$. So if $x$ and $y$ are both apart from $0$, then $xy$ is also apart from $0$.
Finally, let's suppose that $x$ and $y$ are distinguishable - that is, suppose that $x \# y$. Then either $x \# 0$ or $y \# 0$. If $x \# 0$ and $xy = 0$, then $\neg (xy \# 0)$; thus $\neg (y \# 0)$; thus, $y = 0$. And similarly, if $y \# 0$ then $x = 0$. So if $x \# y$ and $xy = 0$, then one of $x$ and $y$ is apart from $0$ and the other equals $0$.
We can still take advantage of most of the familiar theorems involving fields. In cases like $\mathbb{Q}$ where apartness is decidable, we have most of the power of classical linear algebra at our disposal.
It turns out that for the real numbers $\mathbb{R}$, we have $x \# y$ if and only if $x < y$ or $y < x$.
Apartness relations are also critical in topology. For example, the typical constructive definition of a Hausdorff space states that a space $X$ is Hausdorff if and only if $\{(x, y) \in X^2 \mid $ there are open sets $x \in U$, $y \in V$ such that $U \cap V = \emptyset\}$ is a tight apartness relation.
Best Answer
It is a theorem of ECST + BRA (a subsystem of CZF set theory) that there is an Archimedean Dedekind-complete (R3) pseudo-ordered (R2) field (R1). See e.g. Section 7.3 in the Aczel-Rathjen constructive set theory notes.
If you extend CZF with countable choice, you get that the "Cauchy" and "Dedekind" reals coincide, and there is a Cauchy-complete Archimedean pseudo-ordered field (in fact uniquely up to isomorphism). For more on the relationship between "Cauchy" and "Dedekind" reals, see the Lubarsky-Rathjen article On the Constructive Dedekind Reals.