Quantifier Elimination for a Class of Intuitionistic Theories
Ben Ellison, Jonathan Fleischmann, Dan McGinn, Wim Ruitenburg · Notre Dame Journal of Formal Logic · 2008
From classical, Fraïissé-homogeneous, ( ≤ ω )-categorical theories over finite relational languages, we construct intuitionistic theories that are complete, prove negations of classical tautologies, and admit quantifier elimination. We also determine the intuitionistic universal fragments of these theories.