So, I realised that the validity and related notions of a quantifier-free first-order sentence is decidable.
I know that the validity of first-order sentences is not in general decidable. So, I am curious about "how many quantifiers it takes" for it to stop being decidable.
I am under the impression that the validity of a sentence with only one quantifier is decidable. For example, consider the sentence below, which we'll call $\sigma$,
$(\forall x (Px \leftrightarrow \neg Px) \to Qa) \lor Rb$
($a$ and $b$ are to denote closed terms)
We turn $\sigma$ into a zeroth-order sentence by substituting the prime formulas by atoms, and obtain $(A \to B) \lor C$. Now, the resulting sentence is not valid, but if it were, we'd know that $\sigma$ was valid. So next we do the same, but for the subsentence in the range of the quantifier, i.e. $Px \leftrightarrow \neg Px$. The resulting zeroth-order sentence is unsatisfiable, so now we know that under any interpretation, $\sigma$ will always have a false implicant, thus always making the implication true, and consequently the disjunction as well.
Now, this is a bit messy, but I hope you get the idea.
So, is it correct to assume that the validity of a sentence with only one quantifier is decidable? I couldn't come up with any counterexamples.
Next, this method at first sight looks like it can just be iterated multiple times for sentences with multiple quantifiers, though I know that at some point validity won't be decidable anymore. When does that happen?