Source : Free On-Line Dictionary of Computing

first-order logic
     
         The language describing the truth of
        mathematical {formula}s.  Formulas describe properties of
        terms and have a truth value.  The following are atomic
        formulas:
     
         True
         False
         p(t1,..tn)	where t1,..,tn are terms and p is a predicate.
     
        If F1, F2 and F3 are formulas and v is a variable then the
        following are compound formulas:
     
         F1 ^ F2	conjunction - true if both F1 and F2 are true,
     
         F1 V F2	disjunction - true if either or both are true,
     
         F1 => F2	implication - true if F1 is false or F2 is
        		true, F1 is the antecedent, F2 is the
        		consequent (sometimes written with a thin
        		arrow),
     
         F1 <= F2	true if F1 is true or F2 is false,
     
         F1 == F2	true if F1 and F2 are both true or both false
        		(normally written with a three line
        		equivalence symbol)
     
         ~F1		negation - true if f1 is false (normally
        		written as a dash '-' with a shorter vertical
        		line hanging from its right hand end).
     
         For all v . F	universal quantification - true if F is true
        		for all values of v (normally written with an
        		inverted A).
     
         Exists v . F	existential quantification - true if there
        		exists some value of v for which F is true.
        		(Normally written with a reversed E).
     
        The operators ^ V => <= == ~ are called connectives.  "For
        all" and "Exists" are {quantifier}s whose {scope} is F.  A
        term is a mathematical expression involving numbers,
        operators, functions and variables.
     
        The "order" of a logic specifies what entities "For all" and
        "Exists" may quantify over.  First-order logic can only
        quantify over sets of {atomic} {proposition}s.  (E.g. For all p
        . p => p).  Second-order logic can quantify over functions on
        propositions, and higher-order logic can quantify over any
        type of entity.  The sets over which quantifiers operate are
        usually implicit but can be deduced from well-formedness
        constraints.
     
        In first-order logic quantifiers always range over ALL the
        elements of the domain of discourse.  By contrast,
        second-order logic allows one to quantify over subsets of M.
     
        ["The Realm of First-Order Logic", Jon Barwise, Handbook of
        Mathematical Logic (Barwise, ed., North Holland, NYC, 1977)].
     
        (1995-05-02)