Are there any sources for good examples of anti-classical theories in intuitionstic first-order logic? There are many examples of topoi with anti-classical properties (such as "all functions $\mathbb{N} \to \mathbb{N}$ are computable"), but I'm unable to find many simple first-order theories.

One which we can devise is the theory of the non-trivial tiny object: (with no extra symbols besides equality) $$ \forall xy, \neg\neg(x = y)\\ \neg \forall xy, (x=y) $$ This is inspired by the set of infinitesimals in SDG, but I believe we can easily produce models in sheaf topoi: For a $T^1$ topological space take $X(U) = U\, \cup\, \{\star\}$ with the restriction $X(U) \to X(V)$ sending elements not in $V$ to $\star$. I have not double-checked the gluing rigorously. For any $x \neq y$ we have that at stage $U$ we always have $U \backslash \{x, y\}$ as a dense open subset in which $x = y$.

Are all anti-classical theories of a sort like this? I suppose equality could be replaced with any relational symbol.