First-order logic

• 1. Introduction

  ›

  First-order logic, also known as predicate logic, predicate calculus, and quantificational logic, starts from a plain claim: all humans are mortal. It rewrites that claim as: for all x, if x is a human, then x is mortal. The rewrite looks pedantic, yet mathematicians, philosophers, linguists, and computer scientists all rely on it. Gottlob Frege and Charles Sanders Peirce laid its foundations independently of one another. Three questions drive what follows. How does a sentence become a string of symbols that a machine can check? What does it mean for such a string to be true? And what can this carefully built language never say, however many axioms are piled onto it?

  519

• 2. Sentences About Things

  ›

  Take two short sentences: Socrates is a philosopher, and Plato is a philosopher. Propositional logic treats each one as an indivisible unit, labelled by a letter such as p or q. First-order logic looks inside them instead. Both share one predicate, is a philosopher, applied in the first case to Socrates and in the second to Plato.

  The fragment x is a philosopher has no definite truth value on its own. Whether it is true depends on which object x denotes and on how the predicate is read. Link two predicates with a conditional, as in if x is a philosopher then x is a scholar, and the result still waits for a value of x.

  The sentence for every x, if x is a philosopher then x is a scholar, adds a universal quantifier to that conditional. The claim now covers every possible choice of x. Its negation is equivalent to a different statement: there exists an x that is a philosopher and is not a scholar. The existential quantifier, there exists, only asks that a single choice works.

  The sentence Socrates is the teacher of Plato uses a predicate with two slots. Predicates may take as many arguments as a situation needs. Now read the sentence there exists an x that is a philosopher against a world of all human beings, with philosopher meaning author of the Republic. It comes out true, because of Plato. Since the system adds individuals while keeping every logical connective, it contains propositional logic inside it. What counts as a legitimate sentence in the first place is decided by a strict grammar, and that grammar comes next.

  9104247

• 3. Alphabet and Grammar

  ›

  The conjunction symbol always means and. No interpretation can turn it into or, which has a separate symbol. These are the logical symbols. Non-logical symbols behave differently. A predicate symbol written Phil of x might mean x is a philosopher, or x is a man named Philip, depending on the interpretation at hand.

  Where one author writes an arrow for implication, another writes Cpq, and a third writes a horseshoe. Some prefer a tilde, an ampersand, or a middle dot for negation and conjunction. Few of these symbols are strictly required. One quantifier, negation, conjunction, variables, brackets, and equality are enough to build everything else.

  In the traditional approach, every n-ary predicate symbol came with an endless supply of siblings, written P with subscripts 0, 1, 2, 3, and so on. That meant a single language of first-order logic, a habit that survives in philosophically oriented books. The modern practice chooses symbols per application through a signature. A signature for groups can be just multiplication, or multiplication together with the number 1. One for ordered fields is 0, 1, plus, times, and less-than. Signatures can be empty, finite, infinite, or even uncountable.

  A grammar in Backus-Naur form captures all of this for symbols with up to three arguments. One formula it admits describes multiplicative inverses, once its symbols are read as multiplication, zero, and one. Terms grow from variables and function symbols. Formulas grow from predicates, equality, negation, connectives, and quantifiers. The string for all x, implies, is made of valid symbols but is not a formula. Parentheses guarantee that any formula can be built in only one way, a property called unique readability.

  In the formula P of x implies for all x Q of x, the letter x appears twice with different standing. The first occurrence is free, while the second is bound by the quantifier. Quine supplied one formalization of this distinction. A formula with no free variable occurrences is called a sentence, and only sentences have definite truth values under an interpretation.

  The language of ordered abelian groups has one constant symbol 0, a unary minus, a binary plus, and a binary less-than-or-equal relation. The axiom that the group is commutative reads: for all x, for all y, x plus y equals y plus x. A grammar like this dictates shape and nothing more. Meaning arrives only when an interpretation assigns each symbol an actual object, function, or relation.

  1815171312

• 4. Worlds for Symbols

  ›

  Suppose the domain of discourse is the set of integers. Under that choice, a binary function symbol can be interpreted as addition, and a constant symbol c can be assigned the value 10. A binary predicate symbol P could stand for the set of pairs of integers whose first member is smaller than the second. The domain and the interpretation function together form a structure, also called a model.

  The formula y equals x shows why a variable assignment is needed. Its truth changes with whichever values x and y denote. In the standard, or Tarskian, semantics, truth is defined step by step in what is called the T-schema, and the connectives follow their propositional truth tables. An existential claim is true when some adjusted assignment, differing only at x, makes the inner formula true. A universal claim demands success for every such adjustment. A second route adds a fresh constant symbol for each element of the domain and substitutes it directly. It assigns exactly the same truth values to all sentences. Game semantics also exists, and it requires the axiom of choice.

  A sentence is satisfiable if some interpretation makes it true. A sentence true under every interpretation is logically valid, and such formulas play a role similar to tautologies in propositional logic. For a formula with free variables, the usual convention counts it as satisfied when its universal closure is. One formula is a logical consequence of another when every interpretation that makes the second true also makes the first true.

  Peano arithmetic has an intended interpretation: the usual natural numbers with their usual operations. It is one example of a first-order theory, which is a set of axioms written in a given signature. A structure satisfying every sentence of the theory is a model of it, and the set of all such structures is an elementary class, a main subject of model theory. A theory is effective when its axioms form a finite or recursively enumerable set. Peano arithmetic and Zermelo-Fraenkel set theory axiomatize number theory and set theory, respectively. Most first-order theories also admit other, nonstandard models.

  A theory is consistent if no contradiction can be proved from its axioms. It is complete if, for every formula in its signature, either the formula or its negation follows from the axioms. Gödel's incompleteness theorem says that an effective first-order theory containing enough natural-number arithmetic can never be both.

  Three algebraic routes remove quantified variables altogether: cylindric algebra from Alfred Tarski and colleagues, polyadic algebra from Paul Halmos, and predicate functor logic mainly from Willard Quine. In 1987, Tarski and Givant showed something striking. The fragment of first-order logic in which no atomic sentence lies within the scope of more than three quantifiers matches relation algebra in expressive power. That fragment is still large enough for Peano arithmetic and most axiomatic set theory, including ZFC.

  34365250

• 5. Machines for Proof

  ›

  A deduction in a Hilbert-style system is a list of formulas. Each line is a logical axiom, an assumed hypothesis, or the product of a rule of inference applied to earlier lines. Typical systems keep the rules few, often just modus ponens and universal generalization, and rely on infinite schemas of axioms. Natural deduction also produces lists of formulas, but it drops the logical axioms and adds more rules for handling the connectives.

  The sequent calculus was built to study natural deduction. It works with sequents, which place formulas A1 through An on the left of a turnstile and B1 through Bk on the right. Intuitively, a sequent says that the conjunction of the left side implies the disjunction of the right side.

  The tableaux method abandons lists for trees. To prove a formula A, it puts the negation of A at the root and tries to show that the negation is unsatisfiable. To refute C or D, the tree branches into C and D, and each branch must fail.

  Resolution is a single rule of inference that, paired with unification, is sound and complete for first-order logic. From a clause containing C and a clause containing the negation of C, it yields the combination of what remains. The rule works only on disjunctions of atomic formulas, so arbitrary formulas must first be converted through Skolemization. It is commonly used in automated theorem proving.

  Every one of these systems produces a finite syntactic object that can be checked without any interpretation. Such derivations are completely formalized, unlike mathematical proofs written in natural language. A sound argument therefore holds in every possible interpretation, whether the subject is mathematics, economics, or something else. All the systems described here are both sound and complete.

  The substitution rule shows how delicate the syntax can be. Take the valid formula that there exists an x equal to y, written in the signature of arithmetic. Replace y with the term x plus 1, and the result says some x equals x plus 1, which is false in many interpretations. The free variable x of the term became bound. Renaming the bound variable to z gives a formula that is valid again.

  Provable identities let quantifiers move. The negation of for all x P of x is equivalent to there exists x not P of x, and the negation of an existential claim becomes a universal one. These rearrangements help put formulas into prenex normal form. Not every move is free: P and there exists x Q of x equals there exists x of P and Q of x only when x does not occur free in P.

  2537384042

• 6. Equality and Emptiness

  ›

  Leibniz's law, also called the indiscernibility of identicals, is the third of three equality axioms in the most common convention. That convention, first-order logic with equality, treats the equality symbol as primitive and always reads it as true identity between members of the domain. The first axiom says each variable equals itself. The second lets equal arguments be swapped inside a function. The third lets equal terms be swapped inside any formula. Each is a schema standing for infinitely many axioms, and symmetry and transitivity follow from them.

  In first-order logic without equality, the symbol is non-logical, and an interpretation may treat two distinct individuals as equal. The equality relation can then be any equivalence relation that is congruent with the functions and relations. A model in which no two distinct individuals are equal is called a normal model. This second convention is often used for second-order arithmetic, where equality between sets of natural numbers is usually omitted.

  Some theories can define equality for themselves. In the theory of partial orders, with only the relation less-than-or-equal, s equals t can abbreviate s is below t and t is below s. In set theory, with only the membership relation, two sets are equal when they belong to exactly the same sets, or when they have exactly the same members. With that definition in place, the usual axiom of extensionality must be restated: sets with the same elements also belong to the same sets.

  The requirement that a domain of discourse be nonempty seems harmless until it is questioned. Inclusive logic permits empty domains, and an empty poset is a natural example of an empty structure. The rule that P or there exists x Q implies there exists x of P or Q, where x is not free in P, is sound in nonempty domains but unsound if the domain may be empty. Truth defined through variable assignment functions breaks down, because no assignment function can have an empty range. Most authors simply exclude the empty domain by definition.

  3431125146

• 7. What Logic Can Decide

  ›

  In 1929, Kurt Gödel proved that sound, complete, effective deductive systems exist for first-order logic. Logical consequence therefore matches finite provability. The naive reading looks hopeless, because the models of a formula can have arbitrarily large cardinality and cannot be inspected one by one. The workaround is to list every finite derivation and search through them. If one sentence implies another, a derivation will eventually turn up.

  This search explains the word semidecidable. A positive answer always arrives, but a negative one may never come. If a sentence A does not imply a sentence B, that does not mean A implies the negation of B.

  David Hilbert and Wilhelm Ackermann posed the Entscheidungsproblem in 1928, asking for a procedure that decides whether a formula is valid. Alonzo Church answered in 1936 and Alan Turing in 1937, independently, and both answered no. Their proofs tie the problem to the unsolvability of the halting problem. The verdict holds whenever the language has at least one predicate, other than equality, with two or more arguments. Propositional logic, by contrast, is decidable.

  Monadic predicate logic, restricted to unary predicate symbols and no function symbols, is decidable. So are the guarded fragment, two-variable logic, and the Bernays-Schönfinkel class. The fragment called C2 combines two variables with counting quantifiers. The Rabin fragment keeps equality and allows exactly one unary function symbol. Description logics study such subsets, and a monograph by Pratt-Hartmann from 2023 surveys them. Another decidable case is the Löb-Gurevich fragment, which has no equality, only unary function symbols, and only unary predicate symbols.

  52830293

• 8. Limits of Expression

  ›

  A theory of cardinality lambda that has an infinite model, the Löwenheim-Skolem theorem says, has models of every infinite cardinality at least lambda. It is one of the earliest results in model theory. No first-order formula can single out the countable structures, or the uncountable ones. No first-order theory has the real line as its only model, since any theory with an infinite model also has a model larger than the continuum. Applied to set theories, the theorem produces what is known as Skolem's paradox.

  The compactness theorem, first proved by Gödel as a consequence of his completeness theorem, says that a set of sentences has a model if and only if every finite subset does. It rules out a surprising number of ideas. The class of all finite graphs is not an elementary class. Neither are the connected graphs, so no first-order formula can say there is a path from x to y. That matters in computer science, where checking a system may mean showing that no bad state is reachable from a good one. Second-order logic can express connectedness.

  Per Lindström showed that these properties characterize first-order logic. Any logical system of his kind that contains first-order logic and satisfies both the Löwenheim-Skolem and compactness theorems is equivalent to it. So is any such system with a semidecidable consequence relation that satisfies Löwenheim-Skolem. Stronger logics can pin down the natural numbers or the real numbers, but they pay by losing compactness or the downward Löwenheim-Skolem theorem.

  The sentence every person who lives in Perth lives in Australia translates cleanly into first-order logic, which is why the logic underlies knowledge representation languages such as FO(.). Natural language is harder. One assessment runs: "Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than first-order predicate logic". The sentence If John is self-satisfied, then there is at least one thing he has in common with Peter needs quantifiers over properties. Santa Claus has all the attributes of a sadist does too. John is walking quickly, Jumbo is a small elephant, and Mary is sitting next to John resist analysis as well, since adverbs, relative adjectives, and prepositions are not ordinary second-order predicates.

  Infinitary logics stretch the language by permitting infinitely long sentences, such as conjunctions of infinitely many formulas. A formula that long cannot be a finite string, so it is represented as a tree. The most studied systems are written with the Greek letters alpha and beta as subscripts, and ordinary first-order logic is the case written L omega omega.

  4947334334