first-order logic

First-order logic (FOL) is a formal deductive system used by mathematicians, philosophers, linguists, and computer scientists. It goes by many names, including: first-order predicate calculus (FOPC), the lower predicate calculus, the language of first-order logic or predicate logic. Unlike natural languages such as English, FOL uses a wholly unambiguous formal language interpreted by mathematical structures. FOL is a system of deduction extending propositional logic by allowing quantification over individuals of a given domain (universe) of discourse. For example, it can be stated in FOL "Every individual has the property P".
See more at Wikipedia.org...

<language, logic> The language describing the truth of mathematical formulas. 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 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 quantifiers 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 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)