# First-order logic

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

(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)].

 < Previous Terms Terms Containing first-order logic Next Terms > first generation computer first generation language first-in first-out first normal form first-order BABEL deductive database equational logic first-order logic Isabelle First Party DMA fish FISH queue FITNR FITS