First-order logic (FOL) refers to logic in which the predicate of a sentence or statement can only refer to a single subject. It is also known as first-order predicate calculus or first-order functional calculus.
FOL differs from propositional logic (PL), which isn't very expressive because information can only be represented as either true or false. FOL is an extension of PL and its predicates assert a relationship among certain elements. It provides a richer language to mathematically represent linguistic (English) statements. It also requires more complex mechanisms to check for logical consequences.
FOL is a system of formal logic that provides a way to formalize natural languages into a computable/mathematical format. With FOL, problems expressed in English sentences can be represented in a formal manner, which makes it possible to formulate ideas, draw conclusions and prove theorems. Such formulations support inferential reasoning, which is crucial for many academic and real-world disciplines, including:
In these fields, FOL is preferred over PL. This is because PL has a limited capacity for abstraction since it doesn't allow for reasoning over variables and functions having general and mutable content. FOL provides a more formal logical system that includes variables and therefore allows for abstraction, symbolic reasoning and inferences.
PL is declarative and assumes the world contains facts. It allows the representation of information in a logical form and draw conclusions from it. However, it's not sufficient or expressive enough to represent complex sentences or natural language statements mathematically and logically.
FOL provides a more expressive and concise way to represent natural language statements. Its logical language is suitable to express the relationship between objects. Like PL, FOL assumes the world contains facts. But unlike PL, it also assumes objects, relations and functions. Objects could be people, theories, numbers, letters, etc. Relations could be specifics like tall, round, father of, etc. And functions refer to other terms such as variables.
Since FOL is an extension of PL, it includes PL. As a result, problems expressed in PL can be treated under FOL. However, the reverse isn't true, meaning not all problems expressed in FOL can be treated under PL.
Another difference between the two types of logic is that PL uses propositions and logical operators to express formulas. FOL also uses variables, quantifiers and relationships. In addition, PL can't handle problems involving changing or undetermined parts. As a result, it's quite easy to check for logical consequences. FOL can handle problems with changing or undetermined parts since formulas can be created with a greater capacity for generalization.
Since PL isn't very expressive, it's difficult -- and often impossible -- to write axioms and draw conclusions from them. It also doesn't provide variables that can be quantified. For example, it's not possible to represent "all fish" in "All fish can swim" by a variable or have the variable take on a range of multiple possible values of specific fish.
It's also not possible to claim that something with a particular property exists by representing that something with a variable. For example, in the statement "There exists an odd number less than 99," it's not possible to represent a number that's odd and less than 99.
A third weakness of PL is that it doesn't provide a syntax to represent specific objects in the domain of interest. Rather, it only permits statements about the domain. For example, it's not possible to have a symbol for India, it's only possible to make statements about India. Finally, PL doesn't support functional abstraction. For example, it's not possible to refer to the neighbor of India.
FOL overcomes these weaknesses by providing a richer language than PL. This is because it not only assumes facts, but includes variables, quantifiers and relationships to better express the logic between elements and to draw conclusions.
That said, the increased expressivity of FOL results in some loss of decidability for logical consequence. FOL is only semi-decidable, which means that if a formula is not a logical consequence of a set of axioms, it may not be possible to show that it's not. Although if a formula is a logical consequence of a set of axioms, then it's possible to show that it is. This means statements exist in FOL that, under certain conditions, cannot be proven true or false.
The syntax of FOL decides which symbols or collection of symbols constitute a logical expression. This syntax is defined relative to a signature consisting of a set of symbols. The symbols are the basic syntactic elements of FOL and are used to write statements in shorthand notation.
FOL consists of three sets of symbols:
Variables usually start with uppercase letters, while functions and predicate symbols start with lowercase letters.
Example:
V = { V : V starts with uppercase }
F = { ronald/0, harry/0, friend_of/1 }
P = { funny/1, chosen/2 }
When referring to a function or predicate symbol, its arity ( See section below on "Arity in FOL functions and predicates") is given after a /. For example, in thick/2, thick is the functor or predicate symbol and the arity is 2.
From FOL language, the following two types of expressions can be built:
FOL syntax can have both logical and non-logical symbols. Logical symbols correspond to logical operators or connectives, such as ∧, ∨, ¬, ⇒, ⇔. They're always interpreted in the sense of the logical operation they represent. Also, their meaning is never conditioned by the domain of discussion in which FOL is used. In other words, the meaning of a logical symbol in FOL is always unambiguous.
Non-logical symbols in FOL consist of predicates, relationships, constants and functions. The meaning associated with them is always domain-specific, which is why their conversion to natural language requires the use of conversion rules and a fair amount of interpretation.
Example:
In the formula P(x), x could have different meanings depending on the domain:
Arity is the number of arguments, parameters or variables in FOL functions and predicates. In FOL, each function and predicate symbol has an arity k > 0. An arity of 0 is known as nullary arity. Arities of 1, 2 and 3 are known as unary, binary and ternary, respectively.
Functions of arity 0 are known as constants. Predicate symbols of arity 0 are propositions. If a function has arity greater than 0, it could have an infinite number of terms.
FOL with equality is an important variant of FOL because it admits equality as a built-in binary relation symbol, so it's a part of FOL, just like →, ¬ and others. This differentiates the equality symbol from the function and predicate symbols in a signature that can be interpreted as arbitrary functions and predicates in a structure.
A special predicate, =, says whether two objects are equal. Equality can only be applied to objects. To state that two propositions are equal, the ↔ symbol should be used.
Examples:
Moony = RemusLupin
Padfoot = SiriusBlack
Wormtail = PeterPettigrew
In FOL, quantifiers allow the definition of formulae where numbers or quantities are considered in relation to some predicates. They correspond to indefinite adjectives in the English language, such as any, some, all or none.
Two types of quantifiers are provided in FOL:
FOL quantifiers are defined through the symbols: ∀ and ∃, which mean all (universal) and there exists (existential), respectively. Quantifiers always precede variables in the expressions that contain them and are written as ∀x and ∃x. Also, if the variable refers to a predicate P(x), the quantifier precedes the predicate and is written as ∀xP(x) and ∃xP(x).
First-order logic can be useful in the creation of computer programs. It's also of interest to researchers and practitioners in the field of artificial intelligence (AI). There are more powerful forms of logic, but FOL is adequate for most everyday reasoning.
Explore key differences between AI vs. machine learning vs. deep learning.
19 Jan 2023