Quantifier-free formula
= Quantifier-free formula
A quantifier-free <first-order formula> is built from <atomic formulas> using logical connectives, with no quantifiers. An embedding of <first-order structures> preserves and reflects its truth, by <mathematical induction> on the <first-order formula>. Both positive and negated atomic information are needed for this conclusion in a relational language.