An anti-classical axiom $\phi$ is one which is inconsistent with LEM 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.