first-order logic


first-order logic

(language, logic)The language describing the truth ofmathematical formulas. Formulas describe properties ofterms and have a truth value. The following are atomicformulas:

TrueFalsep(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 thefollowing 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 istrue, F1 is the antecedent, F2 is theconsequent (sometimes written with a thinarrow),

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 lineequivalence symbol)

~F1 negation - true if f1 is false (normallywritten as a dash '-' with a shorter verticalline hanging from its right hand end).

For all v . F universal quantification - true if F is truefor all values of v (normally written with aninverted A).

Exists v . F existential quantification - true if thereexists some value of v for which F is true.(Normally written with a reversed E).

The operators ^ V => <= == ~ are called connectives. "Forall" and "Exists" are quantifiers whose scope is F. Aterm 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 onlyquantify over sets of atomic propositions. (E.g. For all p. p => p). Second-order logic can quantify over functions onpropositions, and higher-order logic can quantify over anytype of entity. The sets over which quantifiers operate areusually implicit but can be deduced from well-formednessconstraints.

In first-order logic quantifiers always range over ALL theelements of the domain of discourse. By contrast,second-order logic allows one to quantify over subsets.

["The Realm of First-Order Logic", Jon Barwise, Handbook ofMathematical Logic (Barwise, ed., North Holland, NYC, 1977)].