# 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?

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.