# Quantifier-free first-order formula equal to propositional formula

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?

## 1 Answer

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.

• Could you clarify the term open? Do you mean open as it is defined here: en.wikipedia.org/wiki/… – lanoxx May 6 '14 at 17:10
• @lanoxx Open just means not closed here, i.e. a formula that contains free variables. – fgp May 7 '14 at 0:40
• I see. The link I posted gives a conflicting definition of what open means. That is why I asked. – lanoxx May 7 '14 at 15:10