How quantifier elimination works

Question

Wondering if you could take something like the transitive relation and rewrite it quantifier free.

$$\forall a,b,c\in X:(aRb\wedge bRc)\Rightarrow aRc$$

The key questions are:

1. If the transitive relation can be written quantifier free, and what that would look like. If not, why not.
2. If all expressions can be written quantifier free. This paper says "all structures with $P = NP$ allow quantifier-elimination", but not sure what $P = NP$ means in this context.
3. When you can use quantifier elimination if not all cases.

Answer 1

Basically, quantor elimination works if you can find for any formula $\varphi(x_1,...,x_n)$ (where $x_1,...,x_n$ are the free variables) an equivalent formula $\psi(x_1,...,x_n)$ that has no quantors.

So what we would need to find in the example would be a single test that returns true if $R$ is transitive, and returns false if not.

How would you proceed to find such an example? First, we need to line out the axioms of our theory. Since we're talking about a 2-ary relation, our universe is $U$, and it has a 2-ary relation symbol $R$. There are no constants or function symbols in our theory.

Next we show whether our theory has quantor elimination for a formula $\exists x: \bigwedge_{i=1}^n L_i$ where $L_i$ is a literal. If so, we can show that we can reduce any formula within the theory to a form without quantifiers.
The only way to build atomic formulas in our theory is as $R(x,y)$ where $x,y$ are variables.

Let's ask the even more simplified version: Is there a quantor free formula $\psi$ with $\psi \equiv \exists x: R(x,y)$?

The answere depends on the cardinality of $U$. If $|U|$ were finite, we could replace $ \exists x: R(x,y)$ by all possible substitutions: $\exists x: R(x,y) \equiv \bigvee_{u\in U} R(u,y)$.
Analogue we could solve the harder case $\exists x: \bigwedge_{i=1}^n L_i$

If $|U|$ is infinite however, the disjunction $\bigvee_{u\in U} R(u,y)$ would be infinite and therefore not a formula. We'd somehow need to reduce the problem of finding finding any point $x$ so that $R(x,y)$ to a finite set of points we have to check. This is obviously not possible, so there's no quantor elimination for our theory if $|U|$ is infinite.

Just as side note: Every theory over a finite universe admits quantifier elimination, so the result for the other case wouldn't be very stunning.

2. No. If that were possible, FOL would be decidable. You could take any formula, reform it to another one without quantifiers, and as it still would be a formula it would be of finite length. So now all you'd have to do would be to solve it part by part, and after some (finite) time, you'd be done and would have your result.

In your paper, it most likely means, that if your theory has quantifier elimination, for every Non-Polynomial algorithm, there can be found a polynomial algorithm that does the same.