I just came across the term quantifier-free first-order formula, I first thought that might be similar to a propositional formula, but then after a closer evaluation I realized there are more concepts in first-order logic then just the quantifiers. I believe the difference is the following. A quantifier-free first-order formula can still contain:
- Function symbols
- Predicates
where as a propositional formula does not have these concepts. Is that correct? Did I miss something?
If the formula is open, it can also contain free variables. Technically, $x=y$ doesn't contain a quantifier. Whether or not you want to allow that case or not depends on why you're interested in quantifier-free formulas in the first place.
If you disallow free variables, then you can, in a way, interpret a quantifier-free formula as a propositional formula. You can simply treat its atomic parts, i.e. a predicate applied to some expression containing functions and constants, as propositions. If propositional logic proves such a translation to be unsatisfiable, then first-order logic will agree.
If propositional logic proves it to be satisfiable, then first-order logic only necessarily agrees if you look at the formula alone. But if you look at it in the context of some theory, then axioms of the theory can of course constraint the truth assignment to the atoms of the formula, and so the formula may be disproved by the theory, even if it's propositional translation is satisfiable.