Chapter 8
First-order logic
First-order logic (FOL) (glossary, opens in a new tab) is the logic of relations and quantification (glossary, opens in a new tab) over objects. In natural language, quantifiers (opens in a new tab) such as “all”, “some”, and “most” tell us how many individuals satisfy a condition. FOL gives precise meanings to “all” and “some”. It is a standard framework for expressing the claims of science and mathematics in a formal language (glossary, opens in a new tab) . Its roots lie in the work of Gottlob Frege (opens in a new tab) and Charles Sanders Peirce (opens in a new tab) on logic and the foundations of mathematics. Today, it is also a language for KRR (glossary, opens in a new tab) in AI. Our question in this chapter is how FOL lets us represent knowledge about objects and their relationships.
Much of FOL’s usefulness comes from its expressive power. Consider our inference about Socrates:
In propositional logic, we could use HUMAN for ‘Socrates is human’ and MORTAL for ‘Socrates is mortal’. Then HUMAN → MORTAL says that if Socrates is human, he is mortal. But the first premise says something about all humans, including people we haven’t named. Giving the premise its own propositional variable would leave its connection to Socrates obscure.
If we wanted to add a premise like ‘Xanthippe is human’, we couldn’t reuse HUMAN, as it already stands for a claim about Socrates. We’d need a new variable, say HUMAN₂, to say that Xanthippe is human, another one, MORTAL₂, for ‘Xanthippe is mortal’, and another conditional, HUMAN₂ → MORTAL₂, to say that if Xanthippe is human, she’s mortal. The similar names don’t tell propositional logic that these claims concern the same properties. Of course, we could list a conditional for each person in a fixed finite domain, but we’d have to extend the list whenever we added another person to our model.
FOL solves this problem by making the underlying structure explicit: Human(Socrates) and Human(Xanthippe) apply the same < gloss > predicate – Human – to different objects – Socrates and Xanthippe . In this way, we can represent the general claim once, as:
Here the so-called universal quantifier ∀x says that the condition that follows applies to every object. So, ∀x (Human(x) → Mortal(x)) means that every object – everything – is such that if it is human, then it is mortal. In other words, all humans are mortal.
By combining the universal quantifier with the existential quantifier \exists, we can express complex mathematical claims in FOL, such as the fact that for every number there exists a larger one. As a formula, this becomes
Mathematical concepts such as the continuity of functions (opens in a new tab) use this kind of nested quantification, and representing mathematical claims and concepts like this is precisely the work required to check mathematical reasoning with(in) AI.
Additionally, FOL has a deep connection to knowledge representation and the way of storing knowledge in a computer: relational databases (glossary, opens in a new tab) . We will develop the language first, then models that represent objects and their properties and relations. Sets, tables, and knowledge graphs display this information; formulas express conditions we can check against it. Database queries bring the two together: Codd’s theorem (opens in a new tab) connects conditions written as formulas to operations on stored tables. This chapter develops these ways of representing and querying knowledge. Chapter 9 · FOL Inference takes up reasoning: what follows from a knowledge base, and how we can prove it.
Syntax
To represent claims about objects, we need expressions for the objects and for their properties and relations. Recall from Chapter 2 · Formal Languages that we define a formal language by giving an alphabet and a grammar. In FOL, the grammar distinguishes two kinds of expression: terms name objects, while formulas make claims about them. We keep the propositional connectives and add quantifiers to express claims about every object or at least one object.
Alphabet
In Human(Socrates), the constant (glossary, opens in a new tab) Socrates names an object and the predicate (glossary, opens in a new tab) Human expresses a property. In BiggerThan(MrSir, LittleJimmy), the predicate expresses a relation between two objects. The order of the arguments is important here: the formula says that Mr Sir is bigger than Little Jimmy, not that Little Jimmy is bigger than Mr Sir.
A function symbol (glossary, opens in a new tab) builds another expression for an object. For example, fatherOf(Socrates) names Socrates’ father. The term distanceBetween(x, y), instead, names the distance between two objects x and y. The arity (glossary, opens in a new tab) of a function or predicate symbol is the number of its argument places. The function symbols fatherOf and Human are unary, while distanceBetween and BiggerThan are binary. We sometimes indicate arity with a superscript, as in Human¹ or BiggerThan².
A variable such as x stands for some object without specifying which one it is. The universal quantifier (glossary, opens in a new tab) ∀ says that a condition holds for every object. The existential quantifier (glossary, opens in a new tab) ∃ says that a condition holds for at least one object. So, for example,
says that for every object there is (at least) a bigger one. Nested quantifiers let us express dependencies of this kind: the choice of y can depend on x.
Here are the kinds of symbols in our alphabet. The dots indicate that a language can have more symbols of the indicated kind:
The superscripts record arities; they needn’t be typed in formulas. Names such as Human and fatherOf make a language easier to read, but their spelling will not force a particular interpretation.
Our language also has variables, the logical symbols listed above, and identity. Different knowledge representation tasks can use different signatures. A language for family relationships might include ParentOf; one for geography might include CapitalOf. We fix the signature before interpreting its symbols.
Terms and formulas
To define the grammar, we first need expressions for objects.
In BNF, with a ranging over constants and x over variables:
The last rule is recursive: function arguments can themselves contain function applications. For example,
is a term. It names the distance between Socrates’ birthplace and the capital of whatever object x stands for. We can omit the application brackets and commas if the arities are fixed and the symbol boundaries remain clear:
As in the propositional parser from Chapter 2 · Formal Languages, the grammar determines the children of each node. At the root, distanceBetween requires two term children. The left child begins with the unary function birthplaceOf and ends at the constant Socrates. The right child begins with capitalOf and ends at the variable x. Each application of a grammar rule fixes the next children.
Enable JavaScript to step through the tree. The grammar and worked example remain available in the chapter.
Replacing x by Greece removes the last variable from our term. The model can then determine its denotation without any further values supplied. We give such terms a name:
Terms fill the argument places in formulas. With t₁, …, tₙ ranging over terms, our formula grammar is:
Human(Socrates) and motherOf(x) = y are atomic formulas. We abbreviate ¬(t₁ = t₂) by t₁ ≠ t₂. fatherOf(Socrates) is a term, so it cannot occupy a formula’s place after a connective. Likewise, Human(Socrates) cannot be an argument of fatherOf: we need an object-denoting term there, not a claim.
Consider our example of a human mother:
The root is ∀x, with one formula child, its scope. That child’s main connective is →. Predicates and identity lead from the formula part of the tree into its term parts. This is why the parser must keep track of whether it expects a formula or a term.
Enable JavaScript to step through the tree. The grammar and worked example remain available in the chapter.
Try removing an argument of motherOf or adding a second one. The parser rejects both strings because the signature fixes its arity at one. As in Formal Languages, the fully bracketed grammar gives each binary connective its own brackets. Parentheses around function and predicate arguments serve a different purpose: they delimit a list of terms.
The language already gives us a way to represent knowledge: collect formulas into a knowledge base, as we did with propositional logic. For example, {Human(Socrates), ∀x (Human(x) → Mortal(x))} records a fact and a general condition. The language can also express contradictory information, such as Human(Socrates) together with ¬Human(Socrates).
Before we can say when these formulas are true, we need to distinguish claims about particular objects from conditions whose variables still need values.
Scope and open formulas
Human(x) expresses a condition on an object, but it does not say which object x stands for. In ∃x Human(x), the quantifier binds that occurrence of x. We need to identify such bindings before we can evaluate a formula.
In our formula about human mothers, the two scopes are:
Enable JavaScript to explore variable binding.
The arrows connect each quantifier with its bound occurrences. The scope of ∀x is the whole conditional; the scope of ∃y is its right-hand conjunction.
The x inside motherOf(x) belongs to ∀x, even though it also lies inside the scope of ∃y. Binding requires the same variable.
Reusing a variable can hide a different binding. In
Enable JavaScript to explore variable binding.
the first occurrence in Human(x) belongs to ∃x. The occurrences in the inner conditional belong to ∀x. Renaming the inner bound variable makes the structure easier to see without changing what the formula says:
An open formula acts as a complex predicate. Human(x) expresses a property of one object; (Human(x) ∧ ¬Mortal(x)) expresses the more specific property of being human and immortal. (BiggerThan(x, y) ∧ Human(x)) expresses a relation between two objects. The free variables mark the places whose values are still needed. Quantifying a variable closes that place.
A variable can have free and bound occurrences in the same formula. For example, (Human(x) ∧ ∀x Mortal(x)) is open because its first occurrence of x is free.
Enable JavaScript to explore variable binding.
A quantifier cannot bind occurrences outside its scope. In the following formula, the two quantifiers use the same variable name, but each binds only the occurrence in its own conjunct:
Enable JavaScript to explore variable binding.
A quantifier can also be vacuous (glossary, opens in a new tab) : its scope contains no free occurrence of the variable it quantifies. In ∀x Human(y), there is no x to bind, and y remains free. With our nonempty-domain convention, adding this quantifier does not change the condition on y.
Enable JavaScript to explore variable binding.
Substitution
We can fill a free variable’s place with a term. This lets us turn a condition such as Human(x) into the claim Human(Socrates), or into another open formula such as Human(fatherOf(y)).
For instance,
The bound occurrences stay unchanged. There is a second precaution, needed for Chapter 9 · FOL Inference: replacing x by y in ∃y BiggerThan(x, y) must not produce ∃y BiggerThan(y, y). That would capture the newly inserted y. Rename the bound variable to a fresh z first:
The resulting formula still has a free y. Binding and substitution are facts about the syntax tree; they do not depend on a model.
Iterated quantifiers
Some claims relate a choice for one variable to a choice for another. We express these dependencies with iterated quantifiers (glossary, opens in a new tab) , where one quantifier occurs within another’s scope. Suppose we’re talking about the natural numbers ℕ = {0, 1, 2, …}. We use a binary predicate LessThan for the usual strict ordering and write x < y as shorthand for LessThan(x, y). Then
says that every number has a larger number. To check what it requires, take any value n for x. The inner existential asks for a value of y larger than n. We can always use n + 1: for x assigned 0, use 1; for x assigned 1, use 2; and so on. The witness for y can depend on the value of x.
Reversing the quantifiers changes that dependency:
This says that there is a number larger than every number. Now we must choose one value for y that works for every value of x. No natural number does: if we choose n for y, assigning n to x already makes x < y false. For the natural numbers, the first sentence is true and the second is false.
Two universal quantifiers, as in ∀x ∀y A(x, y), require every pair of values to work. Two existential quantifiers require at least one pair. Exchanging quantifiers of the same kind preserves these conditions. With mixed quantifiers, the order determines which choices may depend on which others.
No finite, nonempty set of numbers with its usual ordering makes ∀x ∃y (x < y) true: its largest member has no larger member in the domain. The choice of objects therefore affects which claims are true. We will return to this example when we compare finite and infinite models.
Open formulas express properties and relations; sentences make claims with no free places left to fill. Either way, writing a formula does not guarantee that it describes a possible scenario. A knowledge base can describe one scenario, many of them, or none. Models will give us a precise representation of these scenarios.
Models
In Chapter 3 · Valid inference, we treated models as possible worlds without analyzing their contents. Chapter 4 · Boolean algebra then represented a world’s basic facts by truth-values. FOL lets us look further inside: we distinguish objects and record their properties and relations.
A model is a possible reasoning scenario. In propositional logic, a scenario specifies which basic claims are true. A first-order scenario also tells us which objects there are, what our names denote, and which properties and relations those objects have.
Suppose Socrates is human. We can represent this information by placing him inside a set labeled Human, listing him in a table of humans, or attaching Human to his node in a knowledge graph. For relational information, such as Mr Sir being bigger than Jimmy, we can list an ordered pair or draw a labeled arrow. These presentations record the same information. The mathematical notion of a model collects what they have in common.
Here Dⁿ contains the ordered n-tuples from D. The semantic brackets ⟦…⟧ᴹ indicate interpretation in M; we omit the superscript when only one model is under discussion.
For a finite model, we can record these interpretations in tables. This gives us a relational database: a way of storing the scenario’s information in a computer. Constants and functions require tables too, with constraints that ensure they pick out the right number of values. Later we will use formulas to query that information.
Domains
We first choose which objects our scenario contains. A model of a family might contain people; a model of arithmetic might contain numbers. This set of objects is the domain, and it fixes what our quantifiers range over. We can also mix kinds of objects. Our example contains Little Jimmy, Mr Sir, Granny Smith, Socrates, and a box:
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
The pictures represent the objects themselves. The domain is a set, so its order does not matter, and each object occurs only once. Which objects we include is a modeling choice: leaving someone out means our claims about every object will not range over that person.
Domains need not be finite. The natural numbers, integers, or real numbers can be a domain. Arithmetic uses such infinite scenarios, and some first-order theories can only be represented by infinite models. Our finite examples let us display every object; they do not limit the definition of a model.
Constants
Having chosen the objects, we can give them names. We might let Socrates name the pictured Socrates. That object is the constant’s denotation (glossary, opens in a new tab) in this scenario:
The labeled objects below show the denotations of our three constants. A table can record the same assignments, one constant and its denotation per row.
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
Functions
We can also refer to an object through its relation to another: Jimmy’s father, for example. The term fatherOf(LittleJimmy) does this by applying a function to Jimmy. To interpret it, we need the denotation of LittleJimmy and a function on the domain.
For a unary function, a table has one row for every domain object. An arrow diagram gives each object exactly one outgoing arrow with the function’s label. Both represent the same function. In the example, the row beginning with Jimmy ends with Mr Sir:
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
Our example assigns the box to itself and Socrates to himself. These choices complete the function, but they do not fit the intended family story. Following a unary function repeatedly in any finite domain eventually revisits an object. An acyclic ancestry chain would require a different representation. A binary predicate ParentOf can record parent pairs without assigning every object a parent. We will discuss what an absent pair means in the next section.
For a binary function, we need a value for every ordered pair in D²; for an n-ary function, for every tuple in Dⁿ. Every value must also belong to D. The name alone imposes no further constraint. In a domain containing Jimmy and a soda, even this is allowed:
We need additional conditions to rule out interpretations that disagree with what we intend to represent.
Predicates
We also need to record which objects are human. We collect Jimmy, Mr Sir, Granny Smith, and Socrates in a set, leaving the box outside it. This is ⟦Human⟧, the extension (glossary, opens in a new tab) of Human: the set of objects to which the predicate applies. A set diagram shows these memberships spatially; a one-column table lists the members.
Relational information needs more than a set of individual objects. To record that Mr Sir is bigger than Jimmy, we must keep the two objects together and remember their order. We use the fixed-length lists called tuples.
The extension of a binary predicate is a set of ordered pairs. A table puts each pair in a row, with its first object in the first column and its second object in the second column. A graph draws an arrow from the first to the second. Here ⟦BiggerThan⟧ contains the pairs from Mr Sir to Jimmy, from Jimmy to the box, and from Mr Sir to the box:
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
Reversing a pair changes its meaning. Including [Jimmy, MrSir] in ⟦Sibling⟧ does not automatically include [MrSir, Jimmy]. Symmetry is an additional condition we might impose. The starting Sibling extension is empty.
An n-ary predicate has a set of n-tuples as its extension, represented by a table with n columns. A ternary LiesBetween needs three columns. We identify unary extensions with sets of one-tuples when writing them as tables. Every tuple is either in the extension or outside it. If we only have incomplete information about a relation, a single complete model commits to more than we know; a set of possible models can leave those choices open.
Models as knowledge bases
A complete model specifies the basic information about a scenario. That information can serve as a knowledge base. We have several ways to present it:
- Semantic equations specify the domain, denotations, function values, and predicate extensions using sets and functions.
- Set diagrams (glossary, opens in a new tab) place objects or tuples inside their extensions. Overlap shows shared membership, as in Euler diagrams (opens in a new tab) . A diagram of one extension shows one part of the model.
- Tables store extensions as rows. Together with tables for the domain, constants, and functions, they encode a finite model as a relational database (glossary, opens in a new tab) (Wikipedia (opens in a new tab) ).
- Knowledge graphs (glossary, opens in a new tab) represent objects as nodes, with property labels and relation arrows (Wikipedia (opens in a new tab) ). For relations with more than two places, we must also record the argument positions.
- Formulas record the model’s basic facts in an expanded language with a name for every object. We will describe this collection below.
These presentations must record the same domain and interpretations to represent the same model. Changing a membership or denotation changes the scenario itself.
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
For the database presentation, predicate extensions become relation tables. A function becomes a table of argument tuples followed by their values, with exactly one value for each argument tuple. Constants require denotation entries, and a domain table records all objects, including those absent from every predicate extension. These tables encode the whole finite structure. We will use the same representation for database queries below.
We can also describe a model syntactically. Give every object a name, adding names if necessary, and record its basic facts as atomic formulas and negated atomic formulas. For example, Human(Socrates) records a membership and ¬Sibling(Socrates, LittleJimmy) records a non-membership. Equations such as fatherOf(LittleJimmy) = MrSir record function values. Model theory calls the full collection of true atomic and negated atomic sentences in this expanded language the atomic diagram (glossary, opens in a new tab) of the model.
The diagram includes identities and inequalities between names. To specify a finite model exactly, we also say that every object is one of the named objects; the atomic diagram alone does not exclude additional unnamed objects. This is another way to represent the scenario’s information with formulas. A general knowledge base can leave some facts open, allowing several models. A complete model settles them all. Satisfaction will tell us precisely how to check a formula against such a scenario.
Truth and satisfaction
A knowledge base should help us answer questions. Once we have recorded who is human, who is mortal, and who is bigger than whom, we can ask which humans are mortal or which humans are bigger than the box. We need not store a separate predicate for every question: open formulas express these complex conditions using the information already in the model.
Before checking a formula, we need to know what its terms denote. A model fixes ⟦LittleJimmy⟧ and the function ⟦fatherOf⟧, but it cannot tell us what fatherOf(x) denotes until we give x a value.
We use v, as for Chapter 4 · Boolean valuations. Here, its values are objects.
With these values supplied, denotation follows the term’s construction:
For a ground term, no variable lookup is needed. Its denotation depends only on M, so we omit v.
Start at the leaves: look up variables in v and constants in M. Then apply each function to the values of its arguments. If v(x) is Jimmy, fatherOf(fatherOf(x)) first gives Mr Sir, then Socrates in our example model. Change the value of x and follow the calculation:
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
Atomic and compound formulas
Once we know what the terms denote, we can check a claim about those objects. For Human(Socrates), we look for Socrates in ⟦Human⟧. For BiggerThan(MrSir, LittleJimmy), we look for the ordered pair in ⟦BiggerThan⟧. We then combine the answers using the same truth-functions as in Chapter 4 · Boolean algebra. Satisfaction records the result of these checks.
Identity (glossary, opens in a new tab) compares the objects denoted by two terms. In our starting model,
is true because both terms denote Mr Sir. The names do not have to look alike. Conversely, a predicate atom is true only when its whole ordered tuple belongs to the predicate’s extension.
A ground formula (glossary, opens in a new tab) contains no variables. Take, for example:
This is an example of a non-atomic ground formula. Every ground formula is a sentence, since it has no free variables. The converse fails: ∀x Human(x) is a sentence containing a variable.
Recall that a sentence is a closed formula: it has no free variable occurrences. An assignment affects satisfaction only through the values of free variables. So for a closed A, any two assignments v and w agree on whether it is satisfied:
A closed formula is therefore satisfied under one assignment iff it is satisfied under every assignment. Take ∀x Human(x): whatever v(x) was, the quantifier checks every object. The box makes this sentence false in our model regardless of the starting assignment. For the open formula Human(x), by contrast, the choice of v(x) matters.
This is why we can omit the assignment for a sentence. For open formulas we keep it explicit. The same convention will apply in Chapter 9 · FOL Inference, where we compare truth across models to study valid inference.
Extensions of open formulas
An open formula defines a complex property or relation in a model. To find its extension, we go through the possible values of its free variables and keep the objects or tuples for which the formula is true.
Write A(x₁, …, xₙ) to list all the free variables of A in a chosen order. An assignment prescription (glossary, opens in a new tab) [x₁ ↦ d₁, …, xₙ ↦ dₙ] gives each of them a value. These are the only values satisfaction depends on.1
Here A(d₁, …, dₙ) is semantic shorthand: the objects need not have names in our language.
For one free variable, we identify a one-tuple [d] with its object d. For example, ⟦(Human(x) ∧ Mortal(x))⟧ contains all four humans in the starting model. If Jimmy becomes immortal, it contains only Mr Sir, Granny Smith, and Socrates. For two free variables, we try the ordered pairs [d, e] ∈ D², assigning d to x and e to y for each check.
The extension of (BiggerThan(x, y) ∧ Human(x)) keeps the BiggerThan rows whose first object is human. There are three such pairs in our starting model:
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
These sets of satisfying tuples will become our database query answers. A required positive atom lets us skip tuples absent from its relation; negation and unrestricted formulas can still require the whole domain.
Quantifiers and truth in a model
The extension makes the quantifiers easy to read. An existential claim says that the extension has a member; a universal claim says it fills the domain.
For a formula with x as its only free variable:
In ∃y Sibling(x, y), we still need a value for x: whose siblings are we asking about? The quantifier changes the value of y while keeping x fixed. We implement this by updating an assignment with a prescription:
An existential quantifier tries possible values for its variable. One witness is enough. A universal quantifier requires every value to work; one counterexample is enough to refute it. In either case, the other variables keep their current assignments.
In the model below, each human belongs to ⟦Mortal⟧. For each object we check the whole conditional Human(x) → Mortal(x). A false antecedent makes the conditional true; a human outside ⟦Mortal⟧ would make it false. Once all five objects pass this check, the universal sentence is true.
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
Finite and infinite models
Our examples use finite lists of objects, but FOL can also describe the whole set of natural numbers. A finite model (glossary, opens in a new tab) has finitely many domain objects; an infinite model (glossary, opens in a new tab) has infinitely many. Infinite models are indispensable in logic and mathematics. Some axioms even require an infinite model: a strict, transitive ordering in which every object has a larger one cannot be finite.
Concrete databases, by contrast, contain finitely many records. Many AI tasks also concern a finite collection of objects: people in a register, parts in a warehouse, or countries on a map. The study of finite models is therefore central to database theory (opens in a new tab) .
For a finite model, the satisfaction clauses give us an algorithm for model checking (glossary, opens in a new tab) : evaluate atoms, combine their truth-values using the connectives, and check domain objects for the quantifiers. Every search finishes, though nested quantifiers can require many checks. On an infinite domain, we cannot generally settle a quantified claim by running through all the objects. We may need a proof instead.
Databases and FOL
A finite model’s predicate extensions can be stored as database tables. We can then use formulas to ask questions about the stored information. Let’s build a database and see how this works.
From a model to a database
Suppose we want to record countries, their capitals, their continents, and languages spoken there. We can describe this information as a model, then store its relations as tables in a relational database (glossary, opens in a new tab) . Our example uses a small dataset; it does not attempt to list every language spoken in each country. Choosing which objects and relations to represent is part of knowledge engineering (glossary, opens in a new tab) .
We use the binary predicates CapitalOf, CityIn, LocatedIn, and LanguageOf. CapitalOf(country, capital) puts the country first. The domain consists of 18 objects, each identified by a distinct text value. Constants such as Europe and Japan denote the corresponding objects. New York appears in CityIn; Washington D.C. appears as the United States’ capital.
Each predicate extension becomes a table with one column per argument place
and one row per tuple. For example, [France, Paris] ∈ ⟦CapitalOf⟧ gives a
row with France in the country column and Paris in the capital column.
SQL has no built-in table of all domain objects. When exporting a model, we
explicitly create Domain(value), including objects absent from every relation.
Without this table, we read a database’s domain as the union of the values in
its relation columns, its active domain. An empty union needs a nonempty
Domain table to give a model in our sense. Constants must denote objects in
the chosen domain; there are no function symbols here.
The database needs both a table structure and its contents. In SQL,
CREATE TABLE declares the columns of an initially empty table; INSERT INTO
adds its rows. TEXT makes the entries text identifiers, and NOT NULL
requires a value in each column. A PRIMARY KEY covering all columns prevents
duplicate rows, so the table represents a set of tuples.
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
With Domain included, the round trip preserves otherwise unused objects. Without it, the app uses the active domain. Constant denotations stay fixed. Each SQL example starts from its own database.
From formulas to queries
With the model stored, we can ask for the countries in Europe or their capitals. An open formula specifies the condition, and its extension gives the answer. This is the connection between the syntactic and semantic approaches to knowledge representation: a formula picks out information in a stored model.
For instance, LocatedIn(x, Europe) asks for the countries in Europe. Its answer in our database is France, the United Kingdom, and Greece. The formula
asks for their capitals. A candidate value of x is kept when some y relates to it through CapitalOf and also relates to Europe through LocatedIn. The answer is Paris, London, and Athens.
For LocatedIn(x, Europe), consider France as a value of x. The pair [France, Europe] occurs in ⟦LocatedIn⟧, so we keep France. Japan fails the same test: its recorded continent is Asia. Each candidate is checked against the stored relation, and the successful candidates form the answer table.
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
The negated query ¬LocatedIn(Japan, x) returns every domain object except Asia, including objects that are not continents. Negation takes its complement relative to the whole domain. If we want continents only, we must express that further restriction.
In SQL, we can retrieve the extension of LocatedIn(x, Europe) as follows:
Enable JavaScript to edit and run this SQL.
Atomic queries
We now go through the syntactic operations one by one. Each rule translates a formula using the translations of its immediate parts. The reverse problem, finding a formula for a query built from table operations, leads to Codd’s theorem.
The short query above reads LocatedIn directly. For a recursive translation, we use a uniform outer query: range over the possible values of each free variable and test the formula as an SQL condition. For one free variable x, the outer query has this form:
This is a template: the comment must be replaced by a condition. d is an
alias, a local name for a row of Domain. Its value column supplies the
current value of x. With two free variables x, y, we use two aliases:
FROM Domain AS d CROSS JOIN Domain AS e. The product visits every ordered
pair of domain values. SELECT DISTINCT d.value AS x, e.value AS y returns
the pairs that pass the condition, without repetitions.
A predicate atom asks whether a particular row exists. For LocatedIn(x, Europe), we search LocatedIn for the current value of x paired with Europe:
Enable JavaScript to edit and run this SQL.
EXISTS is true when its inner query returns at least one row. SELECT 1
puts a placeholder value in that row: here we only need to know whether a
matching row exists. A constant becomes its text identifier, such as
'Europe'; a variable becomes its current domain value, such as d.value.
Thus x = Japan translates to d.value = 'Japan'. If a variable occurs twice,
both occurrences use the same value: LocatedIn(x, x) requires both columns
of a relation row to equal d.value.
Propositional connectives
Suppose we have already translated A and B to SQL conditions. We combine
those conditions according to the main connective, just as in recursive
formula evaluation. Write query(A) for the SQL condition translating A, including any inner
queries:
| FOL | SQL condition |
|---|---|
| ¬A | NOT (query(A))
|
| A ∧ B | (query(A)) AND (query(B))
|
| A ∨ B | (query(A)) OR (query(B))
|
| A → B | (NOT (query(A))) OR (query(B))
|
For example, LocatedIn(x, Europe) ∧ ¬LanguageOf(x, English) has conjunction
as its main connective. Translate the two atoms first, negate the second
condition, and join them with AND:
Enable JavaScript to edit and run this SQL.
The answer is France and Greece. Replacing AND with OR changes the
formula’s main connective and therefore its answer. Notice that NOT rejects
a candidate exactly when the condition inside it succeeds. Because candidates
come from Domain, negation can also retain cities, languages, and continents.
Restricting a variable to countries takes another condition; its name alone
doesn’t restrict its range.
Quantifiers
An existential quantifier introduces another search over Domain. For each
current value of x, ∃y A(x, y) asks whether some value of y makes A
true. Give y a fresh domain alias, translate A using that alias, and put
the condition inside EXISTS.
For ∃y (CapitalOf(y, x) ∧ LocatedIn(y, Europe)), the recursion has three
steps: translate the two atoms, combine them with AND, then search for a
value of y satisfying that conjunction. The outer alias d supplies x;
the inner alias e supplies y:
Enable JavaScript to edit and run this SQL.
Only x appears in the result. The inner value of y supplies a witness; it isn’t a free variable of the whole formula.
A universal quantifier asks whether every value passes. SQL can express this by looking for a failure: ∀y A is true exactly when ∃y ¬A is false. Translate A, negate its condition, search for such a value of y, and negate the search result:
| FOL | SQL condition template |
|---|---|
| ∃y A | EXISTS (SELECT 1 FROM Domain AS e WHERE query(A))
|
| ∀y A | NOT EXISTS (SELECT 1 FROM Domain AS e WHERE NOT (query(A)))
|
Here query(A) uses e.value for y; the notation is a placeholder, not an SQL function.
For example, ∀y (LocatedIn(x, y) → y = Europe) asks for objects whose
recorded locations, if any, are all Europe. A counterexample would be a
location other than Europe:
Enable JavaScript to edit and run this SQL.
France, the United Kingdom, and Greece pass. Objects with no recorded location also pass: they supply no counterexample to the conditional. The United States and Japan fail. To ask specifically for European countries, the earlier positive atomic query is a better choice.
With iterated quantifiers, repeat the construction. Each quantifier gets a fresh alias, and the scope is translated using that alias for its bound variable. An inner quantifier for the same variable temporarily replaces its outer alias; outside that scope, the outer alias still applies. The parse tree determines where each translation step belongs. This gives us a procedure for translating formulas of any depth in our relational language.
Codd’s theorem
We can now translate a formula by translating its parts. Can we go back as well, from a computation on tables to a formula? Codd’s theorem gives us this connection between logic and databases.
We need one qualification. A query is domain-independent if adding unused objects to the domain, while leaving the stored relations and constant denotations unchanged, leaves its answer unchanged. Asking for European capitals has this property: adding an object to no relation cannot make it a European capital.
Selecting rows tests their values; projecting columns keeps only the requested columns. Products combine rows from two tables, and subtraction removes rows found in the second table. These operations form relational algebra (glossary, opens in a new tab) ; describing queries with FOL formulas is called relational calculus (glossary, opens in a new tab) . We use SQL to write the table operations. Codd’s theorem says that we can translate between these computations and formulas without changing the answer on any database.
Our negated query, ¬LocatedIn(Japan, x), explains the domain-independence qualification: adding an unused object changes its answer. Our recursive translation handles such formulas too because it explicitly queries Domain. Codd’s theorem concerns queries that need no such dependence on unused objects.
This recalls the Curry–Howard correspondence (glossary, opens in a new tab) from Chapter 7 · Logical proofs. There, a formula becomes a type, and a proof becomes a program of that type. Here, a model becomes a database, and an open formula becomes a query on that database:
| Logical representation | Computational representation | |
|---|---|---|
| Curry–Howard | Formula | Type |
| Proof of the formula | Program of that type | |
| Databases and FOL | Model | Database |
| Open formula evaluated in the model | Query evaluated on the database |
Both connections let us move between logical and computational representations. A type specifies what a proof program must establish; an open formula specifies which tuples a query must return. Codd’s theorem tells us that the table operations can compute exactly the relations specified by the appropriate formulas. Unlike a proof, a query does not establish its formula in general: its answer depends on the database we give it.
Enable JavaScript to use the model canvas. The definitions and worked examples remain available.
Going back from SQL can introduce or rename bound variables. The resulting formula needn’t be spelled like the original; it must return the same relation. SQL also has features outside this correspondence, such as duplicates, NULLs, and aggregates. The translation here covers the FOL fragment.
A database query concerns one specified model. A knowledge base can describe many possible models. Chapter 9 · FOL Inference asks which conclusions hold in every model of its premises and develops inference rules for reasoning about them.
Further readings
- Richard Zach, Sets, Logic, Computation (PDF) (opens in a new tab) , chapters 6–7, for first-order syntax, structures, and variable assignments.
- Russell and Norvig, Artificial Intelligence: A Modern Approach, 4th edition (opens in a new tab) , chapter 8, for first-order knowledge representation.
-
Formally, complete the prescription to any assignment on all variables. Every completion gives the same result, since all free variables already have their values. ↩︎