1. first-order logic 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 pt1,. . tnwhere 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 ^ F2conjunction - true if both F1 and F2 are true, F1 V F2disjunction - true if either or both are true, F1 => F2implication - true if F1 is false or F2 is true, F1 is the antecedent, F2 is the consequent sometimes written with a thin arrow, F1 <= F2true if F1 is true or F2 is false, F1 == F2true if F1 and F2 are both true or both false normally written with a three line equivalence symbol ~F1negation - true if f1 is false normally written as a dash - with a shorter vertical line hanging from its right hand end. For all v . Funiversal quantification - true if F is true for all values of v normally written with an inverted A. Exists v . Fexistential 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. 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].
first-order logic |
