I need some clarification on understanding the "undecidability of" First-Order Logic (onwards, FOL). I understand that it means that the set of FOL theorems is undecidable (i.e. there is no effective method to decide, for any FOL wff, wether it's a theorem or not). By Completeness of FOL that is equivalent to not being an effective method to determine, for any FOL wff, wether it's a validity or not. Now, by the semantics, any proposition P is valid iff ¬P is unsatisfiable. This way, it seems that the undecidability of FOL in the former sense is equivalent to the undecidability of the satisfiability problem (i.e., the inexistence of an effective method to determine wether a given sentence is or not satisfiable).
Now, for my questions:
1) is my previous paragraph correct?
2) (Sorry for not knowing how to properly write logical symbols. Going forwards I'll use ¬ for negation, & for conjunction, v for disjunction, A for the universal quantifier and E for the existential quantifier, asuming the other constants are definable in term of these). I'm trying to figure out which problems would arise in creating a procedure for checking the satisfiability of arbitrary formulas. So far, I've got the following:
1a. Put the formula in prennex normal form (it is known that for each sentence there is a formula in prennex form equivalent to it) 1b. replace existential quantification with Skolem functions (it is known that a formula in prennex form is satisfiable iff its skolemisation i.
Now, supose the sentence resulting from 1a-1b is not of the form Ax(B)
2.Check the satisfiability of this formula:
-It can be transformed into an equivalent disjunctions of conjunctions of literals (we abuse the language to a allow conjunctions and disjunctions to take arbitrary finite sets of propositions as arguments). It will be satisfiable iff at least one of the disjoined conjunctions does not include among its arguments two contradictory literals.
Now consider the case where there is only one universal quantifer in the (skolemised prennex) formula whose satisfiability we're trying to ckeck.
Basically this amounts to as much as checking wether the union of the properties defined by each disjunct equates with the domain of some model. By henkin's theorem, if the sentence is satisfiable, then it's satisfiable in an at most denumerable model. I don't know how do define a procedure to do it, but since it is known that this would be in a decidable fragment of FOL, I asume there is one.
Now, if we have two universal quantifiers in our Skolemised formula, checking the satisfiability of the formula would, analogously, amount to as much as checking wether the union of the binary relations defined in each disjunct equates with the cartesian product of the domain of some (at most denumerable, by Henkin theorem) model. This again, must be possible since it is known that the fragment of FOL with two variables is decidable.
But, why does this not generalise to formulas with n quantifiers?
3) Also, is there an exhaustive list of fragments of FOL within which the satisfiability problem is decidable? In general, is it decidable wether, for an arbitrary fragment of FOL, the satisfiability of its formulas is decidable or not?