On elimination of quantifiers in some non-classical mathematical theories

TL;DR

This paper investigates the failure of quantifier elimination in certain non-classical mathematical theories and suggests that more extensional logics might restore this property.

Contribution

It demonstrates the failure of quantifier elimination in well-known theories under various logical frameworks and proposes moving to more extensional logics as a solution.

Findings

Quantifier elimination fails dramatically in several theories.

Moving to more extensional logics may restore quantifier elimination.

The failure is consistent across different logical backgrounds.

Abstract

Elimination of quantifiers is shown to fail dramatically for a group of well-known mathematical theories (classically enjoying the property) against a wide range of relevant logical backgrounds. Furthermore, it is suggested that only by moving to more extensional underlying logics can we get the property back.