firstorder 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. Firstorder logic can only quantify over sets of atomic
propositions. (E.g. For all p . p => p). Secondorder logic can quantify over
functions on propositions, and higherorder logic can quantify over any type of
entity. The sets over which quantifiers operate are usually implicit but can be
deduced from wellformedness constraints.
In firstorder logic quantifiers always range over ALL the elements of the
domain of discourse. By contrast, secondorder logic allows one to quantify over
subsets.
["The Realm of FirstOrder Logic", Jon Barwise, Handbook of Mathematical Logic
(Barwise, ed., North Holland, NYC, 1977)].
(20051227)
Nearby terms:
firstin firstout « first normal form « firstorder
«
firstorder logic » First Party DMA » fish »
FISH queue
