| A Failure of Quantifier Elimination (2007) | |||||||||||||||
Abstract | |||||||||||||||
| uld actually eliminate quantifiers in the language L an [ flogg [ fx q : q 2 Qg. Here we show that although exp and log are interdefinable, log is essential for quantifer elimination. Theorem. Let OE(x; y) be the formula 9z (exp(exp z) = x y = z exp z): Then OE(x; y) is not equivalent to a quantifier free L R an;exp -formula. Of course OE(x; y) is equivalent to the quantifier free L an [ flogg-formula x ? 1 y = (log x)(log log x): There are several previous "failur | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||