 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.