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.

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