first-order logic
first-order logic
(language, logic)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)].