first-order logic


Also found in: Acronyms, Wikipedia.

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.

["The Realm of First-Order Logic", Jon Barwise, Handbook of Mathematical Logic (Barwise, ed., North Holland, NYC, 1977)].
References in periodicals archive ?
It uses formal logic to encode the deep lexical semantics of the full breadth of psychological words and phrases, providing fourteen hundred axioms of first-order logic organized into twenty-nine commonsense psychology theories and sixteen background theories.
Finally, the article First-Order Logic with Inductive Definitions for Model-Based Problem Solving, by Maurice Bruynooghe, Marc Denecker, and Mirek Truszczynski, complements this special issue by broadening the view on declarative problem solving.
Since program analysis requires reasoning in the combination of first-order logic and theories, we will design efficient algorithms for automated reasoning with both theories and quantifiers.
The first piece was Montague grammar (named after philosopher and mathematician Richard Montague), which uses a formal system of first-order logic, a systematic method of machine learning where a programmer assigns rigid meanings based on syntax and each word's definition.
Kharlampovich will update ICM attendees on the progress of their collaboration to develop a framework using first-order logic that allows mathematicians to approach previously unsolvable problems.
In this coverage it differs from the model-theory that is familiar from mainstream mathematical logic in the twentieth century, which focused almost entirely on classical first-order logic and its infinitary or higher-order extensions.
First-order logic is strong enough to eliminate ontological commitments that are eliminable.
present a first-order logic approach to automatically extract genre classification models using harmony: their system allows for any chord sequence length and enables the coexistence of harmony progressions of various lengths in the same model.
In the first half of the book, the author wrestles with broad issues of identity, individuals, and kinds, while in the second half of the book he addresses more specific related issues, such as those of the part-whole relation, the nature of persons, and even the problem of standard first-order logic as inadequate to capture all that needs to be said about individuals and kinds (suggesting what he calls a "formalized sortal language" complete with a new logical constant, "/" the instantiation sign).
Following an overview of paradoxes historically found in the field, chapters cover truth tables, first-order logic, model theory, formal number theory, axiomatic set theory, and compatibility.
Boticario); (23) Dimensions of Difficulty in Translating Natural Language into First-Order Logic (Dave Barker-Plummer, Richard Cox, and Robert Dale); (24) Predicting Correctness of Problem Solving from Low-level Log Data in Intelligent Tutoring Systems (Suleyman Cetintas, Luo Si, Yan Ping Xin, and Casey Hord); (25) Back to the future: a non-automated method of constructing transfer models (Ming Feng and Joseph Beck); (26) How do Students Organize Personal Information Spaces?
Such expressions describe domain knowledge formally using first-order logic.

Full browser ?