atomic formula

Let Σ be a signaturePlanetmathPlanetmathPlanetmath and T(Σ) the set of terms over Σ. The set S of symbols for T(Σ) is the disjoint unionMathworldPlanetmath of Σ and V, a countably infiniteMathworldPlanetmath set whose elements are called variables. Now, adjoin S the set {=,(,)}, assumed to be disjoint from S. An atomic formula φ over Σ is any one of the following:

  1. 1.

    either (t1=t2), where t1 and t2 are terms in T(Σ),

  2. 2.

    or (R(t1,,tn)), where RΣ is an n-ary relation symbol, and tiT(Σ).


  1. 1.

    Using atomic formulas, one can inductively build formulasMathworldPlanetmathPlanetmath using the logical connectives , ¬, , etc… In this sense, atomic formulas are formulas that can not be broken down into simpler formulas; they are the building blocks of formulas.

  2. 2.

    A literal is a formula that is either atomic or of the form ¬φ where φ is atomic. If a literal is atomic, it is called a positive literal. Otherwise, it is a negative literal.

  3. 3.

    A finite disjunctionMathworldPlanetmath of literals is called a clause. In other words, a clause is a formula of the form φ1φ2φn, where each φi is a literal.

  4. 4.

    A qunatifier-free formula is a formula that does not contain the symbols or .

  5. 5.

    If we identify a formula φ with its double negation ¬(¬φ), then it can be shown that any quantifier-free formula can be identified with a formula that is in conjunctive normal formMathworldPlanetmath, that is, a finite conjunctionMathworldPlanetmath of clauses. For a proof, see this link (

Title atomic formula
Canonical name AtomicFormula
Date of creation 2013-03-22 12:42:54
Last modified on 2013-03-22 12:42:54
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 10
Author CWoo (3771)
Entry type Definition
Classification msc 03C99
Classification msc 03B10
Synonym quantifier free formula
Related topic TermsAndFormulas
Related topic CNF
Related topic DNF
Defines literal
Defines clause
Defines quantifier-free formula
Defines positive literal
Defines negative literal