VERY INTUITIONISTIC THEORIES AND QUANTIFIER ELIMINATION
Wim Ruitenburg · Project Euclid (Cornell University) · 2005
We show methods to construct, and give examples of, consistent intuitionistic theories that admit quantifier elimination. The examples are very intuitionistic in the sense that they prove the negation of the schema of linearity.