Hrbacek, following Ballard, has recently put a certain partial ordering called $\sqsubseteq$ on absolutely everything in order to do nonstandard analysis a la Nelson (i.e. internal set theory):

Let $\mathscr{L}$ be the language of ZFC (and Tarski-Grothendieck if you insist). We say a well-formed formula of $\mathscr{L}$ is an $\in$-formula. We assert that ZFC holds for all well-formed $\in$-formulae.

Now we throw in $\sqsubseteq$ to $\mathscr{L}$ to get a bigger language $\mathscr{HB}.$ First, we assume that ZFC holds for all $\in$-formulae. Let us write $x \sqsubseteq_\alpha y$ as an abbreviation of $x \sqsubseteq \alpha \vee x \sqsubseteq y.$ Suppose we have a well-formed formula $P$ of $\mathscr{HB}.$ We write $P^\alpha$ for the replacement of every instance of $\sqsubseteq$ with $\sqsubseteq_\alpha.$ Let us also write $x \sqsubset y$ for $x \sqsubseteq y \wedge y \not\sqsubseteq x.$ We also write $2^A_{\mathrm{fin}}$ for the set of all finite subsets of $A.$ We also write $(\forall u \sqsubseteq v) P(u,v)$ for $(\forall u)(u \sqsubseteq v \implies P(u,v)),$ and so on for $\exists,$ and for $\in$ as well.

Then Hrbacek's GRIST is the following condition on $\sqsubseteq,$ with four axiom schemata:

R elativization condition on $\sqsubseteq$: $\sqsubseteq$ is a total dense preordering with minimal element $\emptyset$ and no maximal element; i.e. the conjunction of

1. Partial ordering: $(\forall u,v,w)((v\sqsubseteq u \wedge w \sqsubseteq v) \implies w \sqsubseteq u) \wedge u \sqsubseteq u;$

2. Preordering: $(\forall u,v)(u \sqsubseteq v \wedge v \sqsubseteq u);$

3. Minimality of $\emptyset$: $(\forall u)(\emptyset \sqsubseteq u);$

4. Illimitability: $(\forall u) (\exists v) (u \sqsubset v);$

5. Density: $(\forall u,v) (u \sqsubset v \implies (\exists w)(u \sqsubset w \sqsubset v)).$

Axiom schemata, in which we use words so as not to have our eyes completely glaze over:

For any well-formed formula $P$ of $\mathscr{HB}$ depending on finitely many variables,

1. T ransfer: for all $u \sqsubseteq v$ and $x_1,\ldots, x_n \sqsubseteq u,$

$P^u(x_1,\ldots,x_n) \iff P^v(x_1,\ldots,x_n)$

2. S tandardization: for all $u \sqsupset \emptyset$ and for all $A, x_1, \ldots, x_n,$ there are $v \sqsubset u$ and $B \sqsubset v$ such that, for every $w$ with $v \sqsupseteq w \sqsupset u,$

$(\forall y \sqsubseteq w)(y \in B \iff y \in A \wedge P^w(y,x_1,\ldots,x_n)).$

3. I dealization: For all $A \sqsubset v$ and all $x_1,\ldots,x_n,$

$(\forall a \in 2^A_{\mathrm{fin}})\big([a\sqsubset v \implies (\exists y)(\forall x \in a) P^v(x,y,x_1,\ldots,x_n)] \iff[(\exists y)(\forall x \in A)[x \sqsubset u \implies P^v(x,y,x_1,\ldots,x_n)]\big).$

4. G ranularity: For all $x_1,\ldots,x_k,$ if $(\exists u) P^u(x_1,\ldots,x_k),$ then

$(\exists u)[P^u(x_1,\ldots,x_k) \wedge (\forall v)(v \sqsubset u \implies \neg P^v(x_1,\ldots,x_n))]$