first order logic assignment

Introduction to Logic

First Order Logic

In the preceding chapters, we have seen how Herbrand Logic can be used to define arithmetic over finite sets (e.g., modular arithmetic) and arithmetic over infinite sets (e.g., natural number arithmetic). In each case, we started by fixing a language for the arithmetic we wanted to define. For example, we used the object constants 0, 1, 2, 3 for modular arithmetic with modulus 4.

Unfortunately, Herbrand Logic does not allow us to state properties of arithmetic without knowing precisely how many objects are involved. This is problematic when we want to formalize properties of functions or relations that hold across universes of different sizes. For example, we might want to state the fact that addition is commutative whether we're considering finite arithmetic, arithmetic over the natural numbers, or arithmetic over the real numbers.

Unfortunately, without having a fixed universe defined by the language, the material we have seen so far does not give rigorous meaning to the sentences we write. In this chapter, we consider a different logic that avoids this apparent limitation by allowing the universe of objects to vary independently of the space of ground terms in our language. The resulting logic is called First-Order Logic.

In this chapter, we start by introducing the idea of a language-independent space of objects. Then we define a semantics that gives meaning to sentences without fixing in advance the space of objects. We also discuss how the limitation of a fixed universe can be circumvented without leaving the framework of Herbrand Logic.

As we shall see, the semantics of First-Order Logic is based on the notion of a of the world in terms of objects, functions, and relations.

The notion of an used here is quite broad. Objects can be concrete (e.g. this book, Confucius, the sun) or abstract (e.g. the number 2, the set of all integers, the concept of justice). Objects can be primitive or composite (e.g. a circuit that consists of many sub-circuits). Objects can even be fictional (e.g. a unicorn, Sherlock Holmes, Miss Right). In short, an object can be anything about which we want to say something.

Not all knowledge-representation tasks require that we consider all the objects in the world; in some cases, only those objects in a particular set are relevant. For example, number theorists usually are concerned with the properties of numbers and usually are not concerned with physical objects such as resistors and transistors. Electrical engineers usually are concerned with resistors and transistors and usually are not concerned with buildings and bridges. The set of objects about which knowledge is being expressed is often called a .

As an example, consider the Blocks World scene in Figure 1. Most people looking at this figure interpret it as a configuration of toy blocks. Some people conceptualize the table on which the blocks are resting as an object as well; but, for simplicity, we ignore it here. The universe of discourse corresponding to this conceptualization is the set consisting of the five blocks in the scene.

Although in this example there are finitely many elements in our universe of discourse, this need not always be the case. It is common in mathematics, for example, to consider the set of all integers or the set of all real numbers or the set of all n -tuples of real numbers, as universes with infinitely many elements.

An interrelationship among the objects in a universe of discourse is called a relation . Although we can invent many relations for a set of objects, in conceptualizing a portion of the world we usually emphasize some relations and ignore others. The set of relations emphasized in a conceptualization is called the relational basis set .

In a spatial conceptualization of the Blocks World, there are numerous meaningful relations. For example, it makes sense to think about the on relation that holds between two blocks if and only if one is immediately above the other. We might also think about the above relation that holds between two blocks if and only if one is anywhere above the other. The stack relation holds of three blocks that are stacked one on top of the other. The clear relation holds of a block if and only if there is no block on top of it. The bottom relation holds of a block if and only if that block is resting on the table.

One way of giving meaning to these intuitive notions in the context of a specific conceptualization of the world is to list the combinations of objects in the universe of discourse that satisfy each relation in the relational basis set.

For example, the on relation can be characterized as a set of all pairs of blocks that are on -related to each other. If we use the symbols a , b , c , d , and e to stand for the blocks in the scene shown above, then the table below encodes the on relation. There is a separate row in the table for each pair of blocks in which the first element is on the second.

The clear relation is a property of a block in and of itself, not with respect to other blocks. In this case, the table has just one column, and each row represents a block that is clear of other blocks.

The stack relation is a relationship among three blocks; and so the table requires three columns, as shown below. In this case, there is just one stack in the scene, and so there is just one row in the table.

The generality of relations can be determined by comparing their elements. Thus, the on relation is less general than the above relation, since, when viewed as a set of tuples, it is a subset of the above relation. Of course, some relations are empty (e.g. the unsupported relation), whereas others consist of all n -tuples over the universe of discourse (e.g. the block relation).

Logic allows us to capture the contents of such tables; and, more importantly, it allows us to assert relationships between these tables. For example, it allows us to say that, if one block is on a second block, then that block is above the second block. Also, the first block is not on the table. Also, the second block in not clear. Moreover, it allows us to say these things general , i.e. out of the context of any particular arrangement of blocks.

One thing that our tabular representation for relations makes clear is that, for a finite universe of discourse, there is an upper bound on the number of possible n -ary relations. In particular, for a universe of discourse of size b , there are b n distinct n -tuples. Every n -ary relation is a subset of these b n tuples. Therefore, an n -ary relation must be one of at most 2^( b n ) possible sets.

A function is a special kind of relation among the objects in a universe of discourse. For each combination of n objects in a universe of discourse (called the arguments , a function associates a single object (called the value ) of the function applied to the arguments. Note that there must be one and exactly one value for each combination of arguments. Functions that are not defined for all combinations of arguments are often called partial functions ; and functions for which there can be more than value for a given combination of arguments are often called multi-valued functions . By and large, we will ignore partial and multi-valued functions in what follows.

Mathematically, a function can be viewed as a set of tuples of objects, one for each combination of possible arguments paired with the corresponding value. In other words, an n -ary function is a special kind of ( n +1)-ary relation. For example, consider the unary function shown on the left below. We can view this function as a binary relation shown on the right.

	→
	→
	→
	→
	→

In an analogous way, a binary function can be treated as a ternary relation; a ternary function can be treated as a 4-ary relation; and so forth.

Although the tabular representation for functions and relations is intuitively satisfying, it consumes a lot of space. Therefore, in what follows, we use a different way of encoding relational tables, viz. as sets of tuples, each tuple representing a single row of the corresponding table.

As an example, consider the on relation shown earlier. In what follows, we will treat the relation as the set of three 2-tuples shown below.

Since functions are relations, we could use the same representation. However, to emphasize the special properties of functions, we use a slight variation, viz. the use of an arrow in each tuple to emphasize the fact that the last element is the value of the function applied to the element or elements before the arrow.

Using this notation, we can rewrite the functional table shown earlier as the set shown below.

Finally, before we get on with the details of First-Order Logic, it is worthwhile to make a few remarks about conceptualization. No matter how we choose to conceptualize the world, it is important to realize that there are other conceptualizations as well. Furthermore, there need not be any correspondence between the objects, functions, and relations in one conceptualization and the objects, functions, and relations in another.

In some cases, changing one's conceptualization of the world can make it impossible to express certain kinds of knowledge. A famous example of this is the controversy in the field of physics between the view of light as a wave phenomenon and the view of light in terms of particles. Each conceptualization allowed physicists to explain different aspects of the behavior of light, but neither alone sufficed. Not until the two views were merged in modern quantum physics were the discrepancies resolved.

In other cases, changing one's conceptualization can make it more difficult to express knowledge, without necessarily making it impossible. A good example of this, once again in the field of physics, is changing one's frame of reference. Given Aristotle's geocentric view of the universe, astronomers had great difficulty explaining the motions of the moon and other planets.

The data were explained (with epicycles, etc.) in the Aristotelian conceptualization, although the explanation was extremely cumbersome. The switch to a heliocentric view quickly led to a more perspicuous theory.

This raises the question of what makes one conceptualization more appropriate than another for knowledge formalization. Currently, there is no comprehensive answer to this question. However, there are a few issues that are especially noteworthy.

One such issue is the grain size of the objects associated with a conceptualization. Choosing too small a grain can make knowledge formalization prohibitively tedious. Choosing too large a grain can make it impossible. As an example of the former problem, consider a conceptualization of our Blocks World scene in which the objects in the universe of discourse are the atoms composing the blocks in the picture. Each block is composed of enormously many atoms, so the universe of discourse is extremely large. Although it is in principle possible to describe the scene at this level of detail, it is senseless if we are interested in only the vertical relationship of the blocks made up of those atoms. Of course, for a chemist interested in the composition of blocks, the atomic view of the scene might be more appropriate. For this purpose, our conceptualization in terms of blocks has too large a grain.

Finally, there is the issue of reification of functions and relations as objects in the universe of discourse. The advantage of this is that it allows us to consider properties of properties. As an example, consider a Blocks World conceptualization in which there are five blocks, no functions, and three unary relations, each corresponding to a different color. This conceptualization allows us to consider the colors of blocks but not the properties of those colors.

We can remedy this deficiency by reifying various color relations as objects in their own right and by adding a partial function - such as color - to relate blocks to colors. Because the colors are objects in the universe of discourse, we can then add relations that characterize them, e.g. pretty , garish , etc.

Note that, in this discussion, no attention has been paid to the question of whether the objects in one's conceptualization of the world really exist. We have adopted neither the standpoint of realism , which posits that the objects in one's conceptualization really exist, nor that of nominalism , which holds that one's concepts have no necessary external existence. Conceptualizations are our inventions, and their justification is based solely on their utility. This lack of commitment indicates the essential ontological promiscuity of logic: Any conceptualization of the world is accommodated, and we seek those that are useful for our purposes.

3. Semantics

An interpretation i is a mapping from the constants of the language into the elements of a conceptualization. We use the expression ∀ i to refer to the universe of discourse corresponding to the conceptualization. Each object constant in our language is mapped into an element of the universe of discourse. Each function constant with arity n is mapped into an n -ary function on the universe of discourse. Each relation constant with arity n is mapped into an n -ary relation on the universe of discourse.

As an example, consider a First-Order language with object constants a , b , c , unary function constant f , and binary relation constant r .

As our universe of discourse, we take the set consisting of the numbers 1, 2, and 3. Admittedly, this is a very abstract universe of discourse. It is also very small. This has the advantage that we can write out examples in their entirety. Of course, in practical situations, universes of discourse are likely to be more concrete and much larger.

The equations shown below define one interpretation of our language in terms of this universe of discourse. As we did with Propositional Logic, we are using metalevel statements here. Remember that these are not themselves sentences in First-Order Logic.

∀	=	{1, 2, 3}
	=	1
	=	2
	=	2
	=	{1→2, 2→1, 3→3}
	=	{[1, 1], [1, 2], [2, 2]}

Note that more than one object constant can refer to the same object. In this case, both b and c refer to the number 2. Also, not every object in the universe of discourse need have a constant that refers to it. For example, there is no object constant that denotes the number 3. Note that the function denoted by f assigns one and only one value to every number in the universe of discourse. By contrast, in the relation r , some objects are paired with several other objects, whereas some objects do not appear at all.

A variable assignment for a universe of discourse ∀ i is a mapping from the variables of the language into ∀ i .

	=	1
	=	1
	=	2

A value assignment based on interpretation i and variable assignment v is a mapping from the terms of the language into ∀ i . The mapping must agree with i on constants, and it must agree with v on variables. The value of a functional term is the result of applying the function corresponding to the function constant to the objects designated by the terms.

	=	1
	=	2
( )	=	2
( )	=	1
( ( ))	=	2

The truth assignment based on interpretation i and variable assignment v is a mapping from the sentences of the language to true or false defined as follows.

Given an interpretation i and a variable assignment v , a relational sentence is true if and only if the tuple of objects denoted by the arguments is contained in the relation denoted by the relation constant.

For example, given the interpretation and the variable assignment presented above, we have the truth assignments shown below. The relational sentence r ( a , b ) is true since [1, 2] is a row in r i . The sentence r ( z , a ) is false since [2, 1] is not in r i .

( , )	=
( , )	=

The conditions for truth of logical sentences in First-Order Logic are analogous to those for the truth of logical sentences in Propositional Logic. A negation ¬φ is true if and only if φ is false. A conjunction (φ ∧ ψ) is true if and only if both φ and ψ are true. A disjunction (φ ∨ ψ) is true if and only if φ is true or ψ is true (or both). An implication is true unless the antecedent is true and the consequent is false. A reduction is true unless the antecedent is true and the consequent is false. An equivalence is true if and only if the truth values of the two embedded sentences are the same.

Intuitively, a universally quantified sentence is satisfied if and only if the embedded sentence is satisfied for all values of the quantified variable. Intuitively, an existentially quantified sentence is satisfied if and only if the embedded sentence is satisfied for some values of the quantified variable.

Sadly, expressing this intuition rigorously is a little tricky. First, we need the notion of a version of a variable assignment. Then, we can give a rigorous definition to our intuition by talking about some variations or all variations of a given variable assignment.

A version v :ν/ x of a variable assignment v is a variable assignment that assigns object x as value of the variable ν and agrees with v on all other variables.

Suppose, for example, we had the variable assignment v shown below.

The version v : y /3 is shown below.

/3	=	1
/3	=	3
/3	=	2

With this notation, we can formalize the semantics of quantified sentences as follows. An interpretation i and a variable assignment v satisfy a universally quantified sentence ∀ν.φ if and only if i and v satisfy φ for all versions of v that can be defined over the same universe of discourse of i . An interpretation i and a variable assignment v satisfy an existentially quantified sentence ∃ν.φ if and only if i and v satisfy φ for at least one version of v that can be defined over the same universe of discourse of i .

An interpretation i and a variable assignment v are said to satisfy a sentence φ (written |= i φ[ v ]) if and only if the sentence φ is assigned the value true .

A sentence is satisfiable if and only if there is an interpretation and a variable assignment that satisfy it. A sentence is valid if and only if it is satisfied by every interpretation and variable assignment. A sentence is unsatisfiable if and only if it is satisfied by no interpretation and variable assignment.

An interpretation i is a model of a sentence φ (written |= i φ) if and only if the interpretation satisfies the sentence for every variable assignment (in other words, if |= i φ[ v ] for every variable assignment v ). Note that, if an interpretation satisfies a closed sentence for one variable assignment, then it satisfies the sentence for every variable assignment (i.e. it is a model). Note also that, if an interpretation i satisfies an open sentence φ with free variable ν for every variable assignment, then it is a model of ∀ν.φ.

4. Blocks World

Let's revisit the Blocks World example from section 6.5. The typical Blocks World scene from chapter 6 is shown again in Figure 1.

As in section 6.4, we adopt a vocabulary with five object constants.

Also as in chapter 6, let's consider the following literals that states whether the on relation holds for each pair of names. We will refer to the following set of sentences as Σ. (We have written the positive literals in black and the negative literals in grey in order to distinguish the two more easily.)

( , )

Here we illustrate one of the main differences between First-Order Logic and Herbrand Logic. Under Herbrand Logic, the set of five object constants fixes the universe of five objects. As a result, the above set of sentences completely defines the arrangement of blocks. That is, there is exactly one Herbrand Logic truth assignment over the language {a,b,c,d,e, on} that satisfies the above set of sentences. In contrast, under First-Order Logic, the set of five object constants are simply five names that refer to objects in a universe but do not constrain the universe in any way. As a result, under First-Order Logic, the set of sentences is satisfied by more than one interpretation. That is, the set of sentences accurately describes more than one arrangement of blocks and does not specify which one.

Here we look at several examples of interpretations that satisfy the sentences Σ.

An interpretation corresponding to arrangement shown in figure 1. ∀ i = {o 1 , o 2 , o 3 , o 4 , o 5 } a i = o 1 b i = o 2 c i = o 3 d i = o 4 e i = o 5 on i = {[o 1 ,o 2 ], [o 2 ,o 3 ], [o 4 ,o 5 ]}

Same five objects. Some objects have more than one name. (o 1 and o 2 ). Some objects have no names (o 4 and o 5 ). ∀ i = {o 1 , o 2 , o 3 , o 4 , o 5 } a i = o 1 b i = o 2 c i = o 3 d i = o 1 e i = o 2 on i = {[o 1 ,o 2 ], [o 2 ,o 3 ]}

Three objects. ∀ i = {o 1 , o 2 , o 3 } a i = o 1 b i = o 2 c i = o 3 d i = o 1 e i = o 2 on i = {[o 1 ,o 2 ], [o 2 ,o 3 ]}

Eight objects. ∀ i = {o 1 , o 2 , o 3 , o 4 , o 5 , o 6 , o 7 , o 8 } a i = o 1 b i = o 2 c i = o 3 d i = o 1 e i = o 2 on i = {[o 1 ,o 2 ], [o 2 ,o 3 ]}

Each of the three interpretations corresponds to a different world of blocks. But they all share a common feature; all three worlds have at least three blocks arranged in a stack. In fact, all the interpretations that satisfy Σ share this common feature.

Below are several example interpretations which do not satisfy set of sentences Σ.

This interpretation does not satisfy Σ because on(a,b) evaluates to false.

This interpretation does not satisfy Σ because ¬ on(a,a) evaluates to false.

5. Arithmetic

In the introduction to this chapter, we mentioned as motivation the desire to write down properties satisfied by a class of arithmetic structures without first fixing the space of objects. Here we consider several properties of addition. We then examine some interpretations that satisfy the properties and some interpretations that do not.

Consider the language with the object constant 0, the function constant s , and the relation constant plus . Below are the the properties of addition we saw in section 6.7 (except that the same relation is replaced with equality). We call this set of sentences Γ

∀ . (0, , )

∀ .∀ .∀ .( ( , , ) ⇒ ( ( ), , ( )))

∀ .∀ .∀ .∀ .( ( , , ) ∧ ¬( = ) ⇒ ¬ ( , , ))

Below are some examples of interpretations that satisfy Γ.

Modular arithmetic with modulus 2 ∀ i = {0,1} 0 i = 0 s i = {0→1,1→0} plus i = {[0,0,0],[1,0,1],[0,1,1],[1,1,0]}

Modular arithmetic with modulus 4 ∀ i = {0,1,2,3} 0 i = 0 s i = {0→1,1→2,2→3,3→0} plus i = {[0,0,0],[1,0,1],[2,0,2],[3,0,3],[0,1,1],[1,1,2],[2,1,3],[3,1,0],[0,2,2],[1,2,3],[2,2,0],[3,2,1],[0,3,3],[1,3,0],[2,3,1],[3,3,2]}

Addition over the natural numbers ∀ i = {0,1,2,3,4,...} (the natural numbers N ) 0 i = 0 s i = {0→1,1→2,2→3,3→4,...} ({m→m+1 : m ∈ N ) plus i = {[m,n,k] : m,n,k ∈ N and k is the sum of m and n}

Nonstandard arithmetic over two objects, where 1+1=1 ∀ i = {0,1} 0 i = 0 s i = {0→1,1→1} plus i = {[0,0,0],[1,0,1],[0,1,1],[1,1,1]}

Below are some examples of interpretations that do not satisfy Γ.

∀ i = {0,1} 0 i = 0 s i = {0→1,1→0} plus i = {[1,0,1],[0,1,1],[1,1,0]} (normal addition modulus 2, except that [0,0,0] is missing) This interpretation does not satisfy Γ because ∀ y . plus (0, y , y ) evaluates to false.

∀ i = {0,1} 0 i = 0 s i = {0→1,1→0} plus i = {[0,0,0],[0,0,1],[1,0,1],[0,1,1],[1,1,0]} (normal addition modulus 2, except that [0,0,1] is added) This interpretation does not satisfy Γ because (among other things), ∀ x .∀ y .∀ z .∀ w .( plus ( x , y , z ) ∧ ¬( z = w ) ⇒ ¬ plus ( x , y , w )) evaluates to false.

6. Properties

Although the semantics of Herbrand Logic and First-Order Logic are different, many of the key concepts of the two logics are the analogous. Notably, the concepts of validity, contingency, unsatisfiability, and so forth have essentially the same definitions in First-Order Logic as in Herbrand Logic.

A sentence is satisfiable if and only if it is satisfied by at least one interpretation. A sentence is falsifiable if and only if there is at least one interpretation that makes it false. A sentence is unsatisfiable if and only if it is not satisfied by any interpretation, i.e. no matter what interpretation we take, the sentence is always false. A sentence is contingent if and only if it is both satisfiable and falsifiable, i.e. it is neither valid nor unsatisfiable.

Not only are the definitions of these concepts the same; some of the results are the same as well. If we think of ground relational sentences and ground equations as propositions, we get similar results for the two logics - a ground sentence in Relational Logic is valid / contingent / unsatisfiable if and only if the corresponding sentence in Propositional Logic is valid / contingent / unsatisfiable.

7. Logical Entailment

A set of First-Order Logic sentences Δ logically entails a sentence φ (written Δ |= φ) if and only if every interpretation that satisfies Δ also satisfies φ.

As with validity and contingency and satisfiability, this definition is essentially the same for First-Order Logic as for Propositional Logic and Herbrand Logic.

In Herbrand Logic, we assume that there is a one-to-one relationship between ground terms in our language and objects in the application area we are trying to describe. For example, in talking about people, we assume a unique name for each person. In arithmetic, we assume a unique term for each number. This makes things conceptually simple, and it is a reasonable way to go in many circumstances. But not always.

In natural language, we often find it convenient to use more than one term to refer to the same real world object. For example, we sometimes have multiple names for the same person - Michael , Mike , and so forth. And, in Arithmetic, we frequently use different terms to refer to the same number - 2+2, 2*2, and 4.

The reverse is also true, We sometimes find that there are objects in an application area for which we have no names. For example, in Mathematics, we occasionally want to say things about uncountably many objects, such as the real numbers. Unfortunately, we have only countably many symbols in our logical language, so in such cases we cannot have names for everything.

Stack Exchange Network

Stack Exchange network consists of 183 Q&A communities including Stack Overflow , the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Q&A for work

Connect and share knowledge within a single location that is structured and easy to search.

What is the signficance and intended purpose of variable assignments in first order logic?

I have what might be a strange question. In so many words: what use is the notion of a variable assignment in first-order logic? Why care about variable assignments at all?

I'm not asking "what is a variable assignment?" I know what a variable assignment is: it's a function that maps from every variable in a (fragment of) a language to an element of the domain in the model for that language.

My question is: why should I care? When will this be useful? I'm not asking to be flippant. I feel like I can't fully understand what variable assignments are util I know what they could be used for and why (if at all) they are signficant. Here's why I'm struggling to see why they are.

First, from what I understand, a variable assignment assigns a referent to a free variable. But overwhelmingly, I'll only ever be working with with sentences -- i.e. WFFs that contain no free variables.
Second, it seems that I'm meant to think that a model $\mathfrak{M} = <D, I> $ or structure $\mathfrak{S} = <D, R_1 ... R_n, F_1 ... F_n>$ [this gets taught in different ways] is somehow incomplete or bad if it fails to provide a variable assignment for each variable in the (fragment of the) language we're working with. But why should I think this? After all, I'll almost never encounter a free variable, so I won't be concerned with the referent of the variable at all, and the whole point of variables is to substitute them, anyways. Why would I ever want a fixed assignment for a variable, given the high likelihood I'll be doing some substitution into it anyways?

Is the idea just that on the extremely low chance I encounter a free variable on its own or in an atomic WFF I'll need to know how to interpret it? That makes some sense, but it still conflcits with my intution that we shouldn't want any interpretation of variables at all. Why should I want it to be the case that, say, x = [____] at all? I'm inclined to think it's preferable to say that variables don't have referents, and consequently free variables and formulas containing free variables just fail to refer or don't have meaning. What am I missing?

OK. Sorry for the weird question. I'm just trying to figure out exactly what the significance of variable assignments is. I must be missing something.

first-order-logic
predicate-logic

1 $\begingroup$ Re: "What is a 'variable assignment?" In computer programming languages, the statement x=y is usually a command to move a copy of the data at the location assigned to the variable y to the location assigned to the variable x. It is not a symmetric relation. It is not logically equivalent to y=x. In a formal proof, however, the statement x=y means only that the symbols x and y are interchangeable in any statement including x=y itself. I think is would be misleading to call it an "assignment" of any kind. In a formal proof, after all, x=y is logically equivalent to y=x. $\endgroup$ – Dan Christensen Commented Jan 25, 2023 at 5:53
2 $\begingroup$ You need variable assignments for recursively evaluating formulas by decomposing them into subformulas, where the variable will eventually be detached from its binding quantifier. $\forall x \phi(x)$ is true iff $\phi(x)$ is true for all possible values of $x$. But when we check the truth value of $\phi(x)$, what is $x$? This is what we need variable assignments for. $\endgroup$ – Natalie Clarius Commented Jan 25, 2023 at 5:56
1 $\begingroup$ Variable assignments are relevant not only for free variables. We need variable assignments for bound variables too, because a quantifier is nothing but a loop over variable assignments. $\endgroup$ – Natalie Clarius Commented Jan 25, 2023 at 6:02
1 $\begingroup$ How do you undertsand "It is red"? By pointing woth a finger to an object on your desk; this is "assigning" a reference to the pronoun "it". The same for the formula "x is red": we need a way to assign a reference (an object of the domain of the interpretation) to the variable "x". $\endgroup$ – Mauro ALLEGRANZA Commented Jan 25, 2023 at 7:08
3 $\begingroup$ Ah, wow. Thank you so much. I see that I was badly misunderstanding the issue. This clarifies it majorly. Thank you all for the help! To put it into words I'm more familiar with, I take it that ff we didn't have variable assignments, then the meaning of WFFs formulas with variables in first order logic wouldn't be compositional (and might not be determinable at all?). That indeed seems like a problem! Thanks for correcting me! $\endgroup$ – dfi6ju Commented Jan 25, 2023 at 14:20

2 Answers 2

Even though a sentence like $\forall x. P(x)$ is a closed formula, you need 'variable assignment' to express what validity in a model $M$ means. By definition, $M \models \forall x. P(x)$ means that for all assignments $\eta$ of $x$ , $M \models_\eta P(x)$ .

(Note that this is essentially the point the lemontree is making in a comment.)

Of course, if you really wanted, you could temporarily look at a new language structure, one in which there is an additional constant symbol that you're going to use to hold the semantics of $x$ , and say that $M \models \forall x P(x)$ means that $M,a \models P(x)$ for all $a$ . But that's just a way of writing down the variable assignment in a different way.

Variable assignments are useful for talking about parameters and for talking about definable sets .

You can talk about parameters by using additional constant symbols , but definable sets are basically collections of variable assignments and I can't think of a reasonable way to talk about them without using a variable assignment or something similar.

Here's an example of a question that uses definable sets. This question is a little contrived.

Suppose we are interested in whether the function $\sin$ is definable in $(\mathbb{R}, 0, 1, +, -, *)$ in structures that satisfy $\text{Th}(\mathbb{R})$ , i.e. the real closed fields .

What does it mean for a function to be definable?

It means that the graph of the function is a definable set.

So, we want to know whether the set $\{ (x, y) : y = \sin(x) \}$ is equivalent to any sets of the form $\{ (x, y) : \varphi(x, y, \vec{p}) \}$ where $\varphi$ is a formula with vocabulary $(0, 1, +, -, *)$ and $\vec{p}$ is a collection of parameters in $\mathbb{R}$ .

I don't have a full proof of this fact, but we can prove that $\sin$ is not 0-definable by noting that, if it were 0-definable, then $\pi$ would be 0-definable as the solution to $\sin(x) = 0$ between $3$ and $4$ and $\pi$ is not 0-definable in real-closed fields .

You must log in to answer this question.

Not the answer you're looking for browse other questions tagged logic first-order-logic predicate-logic ..

Featured on Meta
Upcoming sign-up experiments related to tags

Hot Network Questions

Why don't they put more spare gyroscopes in expensive space telescopes?
Convention of parameter naming - undocumented options
Cannot install gnome-control-center upon upgrading Ubuntu (unmet dependencies with libpython3.10)
Looking for a story that possibly started "MYOB"
How to Find Efficient Algorithms for Mathematical Functions?
Am I using "for your peace of mind" correctly: "You should back up your file for your peace of mind"? Is the phrase equal to "to feel secure"?
Alternatives to raising a mains-fed shower?
Is it correct to call a room with a bath a "toilet"?
How to avoid getting scammed?
Does anyone know what Psatlees is more than it has something to do with silk?
Could Jordan have saved his company and avoided arrest if he hadn’t made that mistake?
Rule of Thumb meaning in statistics
A short story about an ancient anaerobic civilisation on Earth
How much time is needed to judge an Earth-like planet to be safe?
Does the NJ Sewerage Authorities Act say that failure to receive bills does not exempt late charges?
How should I end a campaign only the passive players are enjoying?
View doesn't recognise a change to an underlying table when an existing column is dropped and replaced with one with the same name but as computed
Is there a name for books in which the narrator isn't the protagonist but someone who know them well?
Recommendations Modifying/increasing a bicycles Max Weight limits
Why is the Newcomb problem confusing?
Show sixel images inside Vim terminal
Project Euler 127 - abc-hits
Generalized Sylow's theorem
How do languages where multiple files make up a module handle combining them into one translation/compilation unit?

$first order logic assignment$

school Campus Bookshelves
menu_book Bookshelves
perm_media Learning Objects
login Login
how_to_reg Request Instructor Account
hub Instructor Commons

Margin Size

Download Page (PDF)
Download Full Book (PDF)
Periodic Table
Physics Constants
Scientific Calculator
Reference & Cite
Tools expand_more
Readability

selected template will load here

This action is not available.

3.1: First Order Logic Syntax and Semantics

Last updated
Save as PDF
Page ID 6408

University of Cape Town

$ \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} $

$ \newcommand{\id}{\mathrm{id}}$ $ \newcommand{\Span}{\mathrm{span}}$

( \newcommand{\kernel}{\mathrm{null}\,}\) $ \newcommand{\range}{\mathrm{range}\,}$

$ \newcommand{\RealPart}{\mathrm{Re}}$ $ \newcommand{\ImaginaryPart}{\mathrm{Im}}$

$ \newcommand{\Argument}{\mathrm{Arg}}$ $ \newcommand{\norm}[1]{\| #1 \|}$

$ \newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$ \newcommand{\Span}{\mathrm{span}}$

$ \newcommand{\id}{\mathrm{id}}$

$ \newcommand{\kernel}{\mathrm{null}\,}$

$ \newcommand{\range}{\mathrm{range}\,}$

$ \newcommand{\RealPart}{\mathrm{Re}}$

$ \newcommand{\ImaginaryPart}{\mathrm{Im}}$

$ \newcommand{\Argument}{\mathrm{Arg}}$

$ \newcommand{\norm}[1]{\| #1 \|}$

$ \newcommand{\Span}{\mathrm{span}}$ $ \newcommand{\AA}{\unicode[.8,0]{x212B}}$

$ \newcommand{\vectorA}[1]{\vec{#1}} % arrow$

$ \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$

$ \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } $

$ \newcommand{\vectorC}[1]{\textbf{#1}} $

$ \newcommand{\vectorD}[1]{\overrightarrow{#1}} $

$ \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} $

$ \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} $

Observe first that logic is not the study of truth, but of the relationship between the truth of one statement and that of another . That is, in logic, we do not care whether a statement like “If angels exist then necessarily all of them fit on the head of a needle” (suitably formalized) is indeed true in reality 1 , but if the if-part were true (resp., false), then what does that say about the truth value of the then-part of the statement? And likewise for a whole bunch of such sentences. Others do care what is represented formally with such a logic language, but we will defer that to Block II.

To be able to study those aspects of logic, we need a language that is unambiguous; natural language is not. You may have encountered propositional logic already, and first order predicate logic (FOL) is an extension of that, which enables us to represent more knowledge in more detail. Here, I will give only a brief glimpse of it. Eventually, you will need to be able to recognize, understand, and be able to formalize at least a little bit in FOL. Of all the definitions that will follow shortly, there are four important ideas to grasp: the syntax of a language, the model-theoretic semantics of a language, what a theory means in the context of logic, and the notion of deduction where we apply some rules to what has been represented explicitly so as to derive knowledge that was represented only implicitly. We will address each in turn.

First, there are two principal components to consider for the language:

Definition $\PageIndex{1}$: Syntax

Syntax has to do with what ‘things’ (symbols, notations) one is allowed to use in the language and in what way; there is/are a(n):

Language constructs
Sentences to assert knowledge

Definition $\PageIndex{2}$: Semantics

Semantics: Formal meaning, which has to do what those sentences with the alphabet and constructs are supposed to mean.

Their details are presented in the remainder of this section.

The lexicon of a first order language contains the following:

Connectives and Parentheses: $\neg$, $\to$, $\leftrightarrow$, $\wedge$, $\vee$, ( and );
Quantifiers: $\forall$ (universal) and $\exists$ (existential);
Variables: $x, y, z, ...$ ranging over particulars (individual objects);
Constants: $a, b, c, ...$ representing a specific element;
Functions: $f, g, h, ...$, with arguments listed as $f(x_{1}, ...x _{n})$;
Relations: $R, S, ...$ with an associated arity.

There is an (countably infinite) supply of symbols (signature): variables, functions, constants, and relations.

In other words: we can use these things to create ‘sentences’, like we have in natural language, but then controlled and with a few extra figurines. Let us look first at how we can formalise a natural language sentence into first order logic.

Example $\PageIndex{1}$:

From Natural Language to First order logic (or vv.). Consider the following three sentences:

– “ Each animal is an organism”

– “ All animals are organisms”

– “ If it is an animal then it is an organism”

This can be formalised as:

\[∀x(Animal(x) → Organism(x))\]

Observe the colour coding in the natural language sentences: ‘each’ and ‘all’ are different ways to say “$\forall$” and the ‘is a’ and ‘are’ in the first two sentences match the “$\to$”, and the combination of the “$\forall$” and “$\to$” in this particular construction can be put into natural language as ‘if ... then’.

Instead of talking about all objects of a particular type, one also can assert there are at least some of them; e.g.,

– “Aliens exist ”

could be formalised as

\[∃x Alien(x)\]

with the ‘exist’ matching the ∃, and

– “ There are books that are heavy”

(well, at least one of them is) as:

\[∃x(Book(x) ∧ heavy(x))\]

where the ‘there are’ is another way to talk about “$\exists$” and the ‘that’ hides (linguistically) the “$\wedge$”. A formulation like “There is at least one book, and it is heavy” is a natural language rendering that is closer to the structure of the axiom.

A sentence—or, more precisely, its precise meaning—such as “Each student must be registered for a degree programme” requires a bit more consideration. There are at least two ways to say the same thing in the way the sentence is formulated (we leave the arguments for and against each option for another time):

$∀x, y(registered for(x, y) → Student(x) ∧ DegreeProgramme(y))$

“if there is a registered for relation, then the first object is a student and the second one a degree programme”

$∀x(Student(x) → ∃y registered for(x, y))$

“Each student is registered for at least one y”, where the y is a degree programme (taken from the first axiom)

2. $∀x(Student(x) → ∃y (registered for(x, y) ∧ DegreeProgramme(y)))$

“’Each student is registered for at least one degree programme’

But all this is still just syntax (it does not say what it really means), and it looks like a ‘free for all’ on how we can use these symbols. This is, in fact, not the case, and the remainder of the definitions will make this more precise, which will be illustrated in Example 2.1.2 afterward.

There is a systematic to the axioms in the examples, with the brackets, arrows, etc. Let us put this more precisely now. We start from the basic elements and gradually build it up to more complex things.

Definition $\PageIndex{3}$

(Term) A term is inductively defined by two rules, being:

Every variable and constant is a term.
if $f$ is a m-ary function and $t1, . . . tm$ are terms, then $f(t_{1}, . . . , t_{m})$ is also a term.

Definition $\PageIndex{4}$

(Atomic formula) An atomic formula is a formula that has the form $t1 = t2$ or $R(t_{1}, ..., t_{n})$ where R is an n-ary relation and $t_{1}, ..., t_{n}$ are terms.

Definition $\PageIndex{5}$

(Formula) A string of symbols is a formula of FOL if and only if it is constructed from atomic formulas by repeated applications of rules R1, R2, and R3.

R1. If $\phi$ is a formula then so is $\neg\phi$.

R2. If $\phi$ and $\psi$ are formulas then so is $\phi\wedge\psi$.

R3. If $\phi$ is a formula then so is $\exists x \phi$ for any variable $x$.

A free variable of a formula $\phi$ is that variable occurring in $\phi$ that is not quantified. For instance, if $\phi = \forall x (Loves(x,y))$, then $y$ is the free variable, as it is not bound to a quantifier. We now can introduce the definition of sentence .

Definition $\PageIndex{6}$

(Sentence) A sentence of FOL is a formula having no free variables.

Check that there are no free variables in the axioms in Example 2.1.1, i.e., they are all sentences.

Up to this point, we have seen only a few examples with going back-and-forth between sentences in natural language and in FOL. This is by no means to only option. One can also formalise diagrams and provide logic-based reconstructions of, say, UML class diagrams in order to be precise. We can already do this with syntax introduced so far. Let’s consider again the lion eating impalas and herbivores, as was shown in Figure 1.1.1-B in Chapter 1. First, we ‘bump up’ the eats association end to the name of the binary relation, eats . Second, noting that UML uses lookacross notation for its associations, the 1..* ‘at least one’ amounts to an existential quantification for the impalas, and the * ‘zero or more’ to a universal quantification for the herbivores. This brings us back to Eq. 1.1.1 from Chapter 1:

\[∀x(Lion(x) → ∀y(eats(x, y) ∧ Herbivore(y)) ∧ ∃z(eats(x, z) ∧ Impala))\]

Another example with different constraints is shown in Figure 2.1.1, which could be the start of a UML class diagram (but incomplete; notably because it has no attributes and no methods) or an abuse of notation, in that an ontology is shown diagrammatically in UML class diagram notation, as there is no official graphical language to depict ontologies.

Figure 2.1.1: A UML model that can be formally represented in FOL; see text for details.

Either way, syntactically, also here the UML classes can be converted into unary predicates in FOL, the association is translated into a binary relation, and the multiplicity constraint turns into an existential quantification that is restricted to exactly 4 limbs 2 . In the interest of succinctness and convention, the latter is permitted to be abbreviated as $\exists^{=4}$. The corresponding sentence in FOL is listed in Eq. 2.1.5. One can dwell on the composite aggregation (the black diamond), and we will do so in a later chapter. Here, it is left as an association with an ‘at most one’ constraint on the whole side (Eq. 2.1.6), or: “if there’s a limb related to two animal instances through whole , then those two instances must be the same object”.

\[∀x(Animal(x) → ∃^{=4}y(part(x, y) ∧ Limb(y)))\]

\[∀x, y, z(Limb(x) ∧ whole(x, y) ∧ whole(x, z) ∧ Animal(y) ∧ Animal(z) → y = z)\]

That is, indeed, literally talking of two references to one object.

The ‘new’ constraints that we have not translated before yet, are the subclassing, the disjointness, and the completeness. Subclassing is the same as in Eq. 2.1.1, hence, we obtain Eqs. 2.1.7-2.1.9.

\[∀x(Omnivore(x) → Animal(x))\]

\[∀x(Herbivore(x) → Animal(x))\]

\[∀x(Carnivore(x) → Animal(x))\]

Disjoint means that the intersection is empty, so it has the pattern $∀x(A(x) ∧ B(x) → ⊥)$, where “$⊥$” is the bottom concept/unary predicate that is always false; hence, Eq. 2.1.10 for the sample classes of Figure 2.1.1.

Completeness over the specialisation means that all the instances of the superclass must be an instance of either of the subclasses; hence Eq. 2.1.11.

\[∀x(Omnivore(x) ∧ Herbivore(x) ∧ Carnivore(x) → ⊥)\]

\[∀x(Animal(x) → Omnivore(x) ∨ Herbivore(x) ∨ Carnivore(x))\]

These are all syntactic transformations, both by example and that informally some translation rules and a general pattern (like for disjointness) have been noted. From a software engineering viewpoint, this can be seen as a step toward a logicbased reconstruction of UML class diagrams. From a logic viewpoint, the diagram can be seen as ‘syntactic sugar’ for the axioms, which is more accessible to domain experts (non-logicians) than logic.

This playing with syntax, however, does not say what it all means . How do these sentences in FOL map to the objects in, say, the Java application (if it were a UML diagram intended as such) or to some domain of objects wherever that is represented somehow (if it were a UML diagram depicting an ontology)? And can the latter be specified a bit more precise? We shall see the theoretical answers to such question in the next section.

Whether a sentence is true or not depends on the underlying set and the interpretation of the function, constant, and relation symbols. To this end, we have structures: a structure consists of an underlying set together with an interpretation of functions, constants, and relations. Given a sentence $\phi$ and a structure $M$, $M$ models $\phi$ means that the sentence $\phi$ is true with respect to $M$. More precisely, through the following set of definitions (which will be illustrated afterward):

Definition $\PageIndex{7}$

(Vocabulary) A vocabulary $\mathcal{V}$ is a set of function, relation, and constant symbols.

Definition $\PageIndex{8}$

($\mathcal{V}$-structure) A $\mathcal{V}$-structure consists of a non-empty underlying set $∆$ along with an interpretation of $\mathcal{V}$. An interpretation of $\mathcal{V}$ assigns an element of $∆$ to each constant in $\mathcal{V}$, a function from $∆n$ to $∆$ to each n-ary function in $\mathcal{V}$, and a subset of $∆n$ to each n-ary relation in $\mathcal{V}$. We say $M$ is a structure if it is a $\mathcal{V}$-structure of some vocabulary $\mathcal{V}$.

Definition $\PageIndex{9}$

($\mathcal{V}$-formula) Let $\mathcal{V}$ be a vocabulary. A $\mathcal{V}$-formula is a formula in which every function, relation, and constant is in $\mathcal{V}$. A $\mathcal{V}$-sentence is a $\mathcal{V}$-formula that is a sentence.

When we say that $M$ models $\phi$, denoted with $M \models \phi$, this is with respect to $M$ being a $\mathcal{V}$-structure and $\mathcal{V}$-sentence $\phi$ is true in $M$.

Model theory is about the interplay between $M$ and a set of first-order sentences $\mathcal{T}$ $(M)$, which is called the theory of $M$, and its ‘inverse’ from a set of sentences $\Gamma$ to a class of structures.

Definition $\PageIndex{10}$

(Theory of $M$) For any $\mathcal{V}$-structure $M$, the theory of $M$, denoted with $\mathcal{T}$ $(M)$, is the set of all $\mathcal{V}$-sentences $\phi$ such that $M \models \phi$.

Definition $\PageIndex{11}$

(Model) For any set of $\mathcal{V}$-sentences, a model of $\Gamma$ is a $\mathcal{V}$-structure that models each sentence in $\Gamma$. The class of all models of $\Gamma$ is denoted by $M(\Gamma)$.

Now we can go to the interesting notions: theory in the context of logic:

Definition $\PageIndex{12}$

(Complete $\mathcal{V}$-theory) Let $\Gamma$ be a set of $\mathcal{V}$-sentences. Then $\Gamma$ is a complete $\mathcal{V}$-theory if, for any $\mathcal{V}$-sentence $\phi$ either $\phi$ or $\neg\phi$ is in $\Gamma$ and it is not the case that both $\phi$ and $\neg\phi$ are in $\Gamma$.

It can then be shown that for any $\mathcal{V}$-structure $M$, $\mathcal{T}$ $(M)$ is a complete $\mathcal{V}$-theory (for proof, see, e.g., [Hed04], p90).

Definition $\PageIndex{13}$

A set of sentences $\Gamma$ is said to be consistent if no contradiction can be derived from $\Gamma$.

Definition $\PageIndex{14}$

(Theory) A theory is a consistent set of sentences.

The latter two definitions are particularly relevant later on when we look at the typical reasoning services for ontologies.

Example $\PageIndex{2}$:

How does all this work out in practice? Let us take something quasi-familiar: a conceptual data model in Object-Role Modeling notation, depicted in the middle part of Figure 2.1.2, with the top-half its ‘verbalisation’ in a controlled natural language, and in the bottom-part some sample objects and the relations between them.

Figure 2.1.2: A theory denoted in ORM notation, ORM verbalization, and some data in the database. See Example 2.1.2 for details.

First, we consider it as a theory, creating a logical reconstruction of the icons in the figure. There is one binary predicate, attends , and there are two unary predicates, Student and DegreeProgramme . The binary predicate is typed, i.e., its domain and range are defined to be those two entity types, hence:

\[∀x, y(attends(x, y) → Student(x) ∧ DegreeP rogramme(y))\]

Note that x and y quantify over the whole axiom (thanks to the brackets), hence, there are no free variables, hence, it is a sentence. There are two constraints in the figure: the blob and the line over part of the rectangle, and, textually, “ Each Student attends exactly one DegreeProgramme ” and “ It is possible that more than one Student attends the same DegreeProgramme ”. The first constraint can be formalised (in short-hand notation):

\[∀x(Student(x) → ∃^{=1}y attends(x, y))\]

The second one is already covered with Eq. 2.1.12 (it does not introduce a new constraint). So, our vocabulary is {$attends, Student, DegreeProgramme$}, and we have two sentences (Eq. 2.1.12 and Eq. 2.1.13). The sentences form the theory, as they are not contradicting and admit a model.

Let us now consider the structure. We have a non-empty underlying set of objects: $∆ =$ {$John, Mary, Fabio, Claudia, Markus, Inge, ComputerScience, Biology, Design$} . The interpretation then maps the instances in $∆$ with the elements in our vocabulary; that is, we end up with {$John, Mary, Fabio, Claudio, Markus, Inge$} as instances of $Student$, and similarly for $DegreeProgramme$ and the binary $attends$. Observe that this structure does not contradict the constraints of our sentences.

Equivalences

With the syntax and semantics, several equivalencies between formulae can be proven. We list them for easy reference, with a few ‘informal readings’ for illustration. $\phi$, $\psi$, and $\chi$ are formulas.

Commutativity:

$\phi\wedge\psi\equiv\psi\wedge\phi$

$\phi\vee\psi\equiv\psi\vee\phi$

$\phi\leftrightarrow\psi\equiv\psi\leftrightarrow\phi$

Associativity:

$(\phi\wedge\psi)\wedge\chi\equiv\phi\wedge(\psi\wedge\chi)$

$(\phi\vee\psi)\vee\chi\equiv\phi\vee(\psi\vee\chi)$

Idempotence:

$\phi\wedge\phi\equiv\phi$

$\phi\vee\phi\equiv\phi$ $//$ 'itself or itself is itself'

Absorption:

$\phi\wedge(\phi\vee\psi)\equiv\phi$

$\phi\vee(\phi\wedge\psi)\equiv\phi$

Distributivity:

$\phi\vee(\psi\wedge\chi)\equiv(\phi\vee\psi)\wedge(\phi\vee\chi)$

$\phi\wedge(\psi\vee\chi)\equiv(\phi\wedge\psi)\vee(\phi\wedge\chi)$

Double Negation:

$\neg\neg\phi\equiv\phi$

$\neg(\phi\wedge\psi)\equiv\neg\phi\vee\neg\psi$

$\neg(\phi\vee\psi)\equiv\neg\phi\wedge\neg\psi$ $//$ ‘negation of a disjunction implies the negation of each of the disjuncts’

Implication:

$\phi\to\psi\equiv\neg\phi\vee\psi$

$\phi\vee\top\equiv\top$

Unsatisfiability:

$\phi\wedge\bot\equiv\bot$

$\phi\wedge\neg\phi\equiv\bot$ $//$ something cannot be both true and false

$\phi\vee\neg\phi\equiv\top$

Neutrality:

$\phi\wedge\top\equiv\phi$

$\phi\vee\bot\equiv\phi$

Quantifiers:

$\neg\forall x.\phi\equiv\exists x.\neg\phi$

$\neg\exists x.\phi\equiv\forall x.\neg\phi$ $//$ 'if there does not exist some, then there's always none'

$\forall x.\phi\wedge\forall x.\psi\equiv\forall x.(\phi\wedge\psi)$

$\exists x.\phi\vee\exists x.\psi\equiv\exists x.(\phi\vee\psi)$

$(\forall x.\phi)\wedge\psi\equiv\forall x.(\phi\wedge\psi)$ if $x$ is not free in $\psi$

$(\forall x.\phi)\vee\psi\equiv\forall x.(\phi\vee\psi)$ if $x$ is not free in $\psi$

$(\exists x.\phi)\wedge\psi\equiv\exists x.(\phi\wedge\psi)$ if $x$ is not free in $\psi$

$(\exists x.\phi)\vee\psi\equiv\exists x.(\phi\vee\psi)$ if $x$ is not free in $\psi$

Note $\PageIndex{1}$:

The ones up to (but excluding) the quantifiers hold for both propositional logic and first order predicate logic.

1 or, for that matter, whether there is a reality and whether we have access to it

2 There are animals that indeed do not have 4 limbs (e.g., the sirens and the Mexican mole lizard have only two limbs and the millipede Illacme plenipes has 750 (the most), and there are animals with specific numbers of limbs in between, but that is beside the point as it would not change much the features used in the formalisation, just become more cluttered.

10. Semantics of First Order Logic ¶

In Chapter 6 , we emphasized a distinction between the syntax and the semantics of propositional logic. Syntactic questions have to do with the formal structure of formulas and the conditions under which different types of formulas can be derived. Semantic questions, on the other hand, concern the truth of a formula relative to some truth assignment.

As you might expect, we can make a similar distinction in the setting of first order logic. The previous two chapters have focused on syntax, but some semantic ideas have slipped in. Recall the running example with domain of interest ${\mathbb N}$ , constant symbols 0, 1, 2, 3, function symbols $\mathit{add}$ and $\mathit{mul}$ , and predicate symbols $\mathit{even}, \mathit{prime}, \mathit{equals}, \mathit{le}$ , etc. We know that the sentence $\forall y \; \mathit{le}(0, y)$ is true in this example, if $\mathit{le}$ is interpreted as the less-than-or-equal-to relation on the natural numbers. But if we consider the domain ${\mathbb Z}$ instead of ${\mathbb N}$ , that same formula becomes false. The sentence $\forall y \; \mathit{lt}(0,y)$ is also false if we consider the domain ${\mathbb N}$ , but (somewhat perversely) interpret the predicate $\mathit{lt}(x, y)$ as the relation “ $x$ is greater than $y$ ” on the natural numbers.

This indicates that the truth or falsity or a first order sentence can depend on how we interpret the quantifiers and basic relations of the language. But some formulas are true under any interpretation: for instance, $\forall y \; (\mathit{le}(0, y) \to \mathit{le}(0, y))$ is true under all the interpretations considered in the last paragraph, and, indeed, under any interpretation we choose. A sentence like this is said to be valid ; this is the analogue of a tautology in propositional logic, which is true under every possible truth assignment.

We can broaden the analogy: a “model” in first order logic is the analogue of a truth assignment in propositional logic. In the propositional case, choosing a truth assignment allowed us to assign truth values to all formulas of the language; now, choosing a model will allow us to assign truth values to all sentences of a first order language. The aim of the next section is to make this notion more precise.

10.1. Interpretations ¶

The symbols of the language in our running example—0, 1, $\mathit{add}$ , $\mathit{prime}$ , and so on—have very suggestive names. When we interpret sentences of this language over the domain ${\mathbb N}$ , for example, it is clear for which elements of the domain $\mathit{prime}$ “should” be true, and for which it “should” be false. But let us consider a first order language that has only two unary predicate symbols $\mathit{fancy}$ and $\mathit{tall}$ . If we take our domain to be ${\mathbb N}$ , is the sentence $\forall x \; (\mathit{fancy}(x) \to \mathit{tall}(x))$ true or false?

The answer, of course, is that we don’t have enough information to say. There’s no obvious meaning to the predicates $\mathit{fancy}$ or $\mathit{tall}$ , at least not when we apply them to natural numbers. To make sense of the sentence, we need to know which numbers are fancy and which ones are tall. Perhaps multiples of 10 are fancy, and even numbers are tall; in this case, the formula is true, since every multiple of 10 is even. Perhaps prime numbers are fancy and odd numbers are tall; then the formula is false, since 2 is fancy but not tall.

We call each of these descriptions an interpretation of the predicate symbols $\mathit{fancy}$ and $\mathit{tall}$ in the domain ${\mathbb N}$ . Formally, an interpretation of a unary predicate $P$ in a domain $D$ is the set of elements of $D$ for which $P$ is true. For an example, the standard interpretation of $\mathit{prime}$ in ${\mathbb N}$ that we used above was just the set of prime natural numbers.

We can interpret constant, function, and relation symbols in a similar way. An interpretation of constant symbol $c$ in domain $D$ is an element of $D$ . An interpretation of a function symbol $f$ with arity $n$ is a function that maps $n$ elements of $D$ to another element of $D$ . An interpretation of a relation symbol $R$ with arity $n$ is the set of $n$ tuples of elements of $D$ for which $R$ is true.

It is important to emphasize the difference between a syntactic predicate symbol (or function symbol, or constant symbol) and the semantic predicate (or function, or object) to which it is interpreted. The former is a symbol, relates to other symbols, and has no meaning on its own until we specify an interpretation. Strictly speaking, it makes no sense to write $\mathit{prime}(3)$ , where $\mathit{prime}$ is a predicate symbol and 3 is a natural number, since the argument to $\mathit{prime}$ is supposed to be a syntactic term. Sometimes we may obscure this distinction, as above when we specified a language with constant symbols 0, 1, and 2. But there is still a fundamental distinction between the objects of the domain and the symbols we use to represent them.

Sometimes, when we interpret a language in a particular domain, it is useful to implicitly introduce new constant symbols into the language to denote elements of this domain. Specifically, for each element $a$ of the domain, we introduce a constant symbol $\bar a$ , which is interpreted as $a$ . Then the expression $\mathit{prime}(\bar 3)$ does make sense. Interpreting the predicate symbol $\mathit{prime}$ in the natural way, this expression will evaluate to true. We think of $\bar 3$ as a linguistic “name” that represents the natural number 3, in the same way that the phrase “Aristotle” is a name that represents the ancient Greek philosopher.

10.2. Truth in a Model ¶

Fix a first-order language. Suppose we have chosen a domain $D$ in which to interpret the language, along with an interpretation in $D$ of each of the symbols of that language. We will call this structure—the domain $D$ , paired with the interpretation—a model for the language. A model for a first-order language is directly analogous to a truth assignment for propositional logic, because it provides all the information we need to determine the truth value of each sentence in the language.

The procedure for evaluating the truth of a sentence based on a model works the way you think it should, but the formal description is subtle. Recall the difference between terms and assertions that we made earlier in Chapter 4. Terms, like $a$ , $x + y$ , or $f(c)$ , are meant to represent objects. A term does not have a truth value, since (for example) it makes no sense to ask whether 3 is true or false. Assertions, like $P(a)$ , $R(x, f(y))$ , or $a + b > a \wedge \mathit{prime}(c)$ , apply predicate or relation symbols to terms to produce statements that could be true or false.

The interpretation of a term in a model is an element of the domain of that model. The model directly specifies how to interpret constant symbols. To interpret a term $f(t)$ created by applying a function symbol to another term, we interpret the term $t$ , and then apply the interpretation of $f$ to this term. (This process makes sense, since the interpretation of $f$ is a function on the domain.) This generalizes to functions of higher arity in the obvious way. We will not yet interpret terms that include free variables like $x$ and $y$ , since these terms do not pick out unique elements of the domain. (The variable $x$ could potentially refer to any object.)

For example, suppose we have a language with two constant symbols, $a$ and $b$ , a unary function symbol $f$ , and a binary function symbol $g$ . Let ${\mathcal M}$ be the model with domain ${\mathbb N}$ , where $a$ and $b$ are interpreted as $3$ and $5$ , respectively, $f(x)$ is interpreted as the function which maps any natural number $n$ to $n^2$ , and $g$ is the addition function. Then the term $g(f(a),b)$ denotes the natural number $3^2+5 = 14$ .

Similarly, the interpretation of an assertion is a value $\mathbf{T}$ or $\mathbf{F}$ . For the sake of brevity, we will introduce new notation here: if $A$ is an assertion and ${\mathcal M}$ is a model of the language of $A$ , we write ${\mathcal M} \models A$ to mean that $A$ evaluates to $\mathbf{T}$ in ${\mathcal M}$ , and ${\mathcal M} \not\models A$ to mean that $A$ evaluates to $\mathbf{F}$ . (You can read the symbol $\models$ as “models” or “satisfies” or “validates.”)

To interpret a predicate or relation applied to some terms, we first interpret the terms as objects in the domain, and then see if the interpretation of the relation symbol is true of those objects. To continue with the example, suppose our language also has a relation symbol $\mathit{R}$ , and we extend ${\mathcal M}$ to interpret $R$ as the greater-than-or-equal-to relation. Then we have ${\mathcal M} \not \models R(a, b)$ , since 3 is not greater than 5, but ${\mathcal M} \models R(g(f(a),b),b)$ , since 14 is greater than 5.

Interpreting expressions using the logical connectives $\wedge$ , $\vee$ , $\to$ , and $\neg$ works exactly as it did in the propositional setting. ${\mathcal M} \models A \wedge B$ exactly when ${\mathcal M} \models A$ and ${\mathcal M} \models B$ , and so on.

We still need to explain how to interpret existential and universal expressions. We saw that $\exists x \; A$ intuitively meant that there was some element of the domain that would make $A$ true, when we “replaced” the variable $x$ with that element. To make this a bit more precise, we say that ${\mathcal M} \models \exists x A$ exactly when there is an element $a$ in the domain of ${\mathcal M}$ such that, when we interpret $x$ as $a$ , then ${\mathcal M} \models A$ . To continue the example above, we have ${\mathcal M} \models \exists x \; (R(x, b))$ , since when we interpret $x$ as 6 we have ${\mathcal M} \models R(x, b)$ .

More concisely, we can say that ${\mathcal M} \models \exists x \; A$ when there is an $a$ in the domain of ${\mathcal M}$ such that ${\mathcal M} \models A[\bar a / x]$ . The notation $A[\bar a / x]$ indicates that every occurrence of $x$ in $A$ has been replaced by the symbol $\bar a$ .

Finally, remember, $\forall x \; A$ means that $A$ is true for all possible values of $x$ . We make this precise by saying that ${\mathcal M} \models \forall x \; A$ exactly when for every element $a$ in the domain of ${\mathcal M}$ , interpreting $x$ as $a$ gives that ${\mathcal M} \models A$ . Alternatively, we can say that ${\mathcal M} \models \forall x \; A$ when for every $a$ in the domain of ${\mathcal M}$ , we have ${\mathcal M} \models A[\bar a / x]$ . In our example above, ${\mathcal M} \not\models \forall x \; (R(x, b))$ , since when we interpret $x$ as 2 we do not have ${\mathcal M} \models R(x, b)$ .

These rules allow us to determine the truth value of any sentence in a model. (Remember, a sentence is a formula with no free variables.) There are some subtleties: for instance, we’ve implicitly assumed that our formula doesn’t quantify over the same variable twice, as in $\forall x \; \exists x \; A$ . But for the most part, the interpretation process tells us to “read” a formula as talking directly about objects in the domain.

10.3. Examples ¶

Take a simple language with no constant symbols, one relation symbol $\leq$ , and one binary function symbol $+$ . Our model ${\mathcal M}$ will have domain ${\mathbb N}$ , and the symbols will be interpreted as the standard less-than-or-equal-to relation and addition function.

Think about the following questions before you read the answers below. Remember, our domain is ${\mathbb N}$ , not ${\mathbb Z}$ or any other number system.

Is it true that ${\mathcal M} \models \exists x \; (x \leq x)$ ? What about ${\mathcal M} \models \forall x \; (x \leq x)$ ?

Similarly, what about ${\mathcal M} \models \exists x \; (x + x \leq x)$ ? ${\mathcal M} \models \forall x \; (x + x \leq x)$ ?

Do the sentences $\exists x \; \forall y \; (x \leq y)$ and $\forall x \; \exists y \; (x \leq y)$ mean the same thing? Are they true or false?

Can you think of a formula $A$ in this language, with one free variable $x$ , such that ${\mathcal M} \models \forall x \; A$ but ${\mathcal M} \not \models \exists x \; A$ ?

These questions indicate a subtle, and often tricky, interplay between the universal and existential quantifiers. Once you’ve thought about them a bit, read the answers:

Both of these statements are true. For the former, we can (for example) interpret $x$ as the natural number 0. Then, ${\mathcal M} \models x \leq x$ , so the existential is true. For the latter, pick an arbitrary natural number $n$ ; it is still the case that when we interpret $x$ as $n$ , we have ${\mathcal M} \models x \leq x$ .

The first statement is true, since we can interpret $x$ as 0. The second statement, though, is false. When we interpret $x$ as 1 (or, in fact, as any natural number besides 0), we see that ${\mathcal M} \not \models x + x \leq x$ .

These sentences do not mean the same thing, although in the specified model, both are true. The first expresses that some natural number is less than or equal to every natural number. This is true: 0 is less than or equal to every natural number. The second sentence says that for every natural number, there is another natural number at least as big. Again, this is true: every natural number $a$ is less than or equal to $a$ . If we took our domain to be ${\mathbb Z}$ instead of ${\mathbb N}$ , the first sentence would be false, while the second would still be true.

The situation described here is impossible in our model. If ${\mathcal M} \models \forall x A$ , then ${\mathcal M} \models A [\bar 0 / x]$ , which implies that ${\mathcal M} \models \exists x A$ . The only time this situation can happen is when the domain of our model is empty.

Now consider a different language with constant symbol 2, predicate symbols $\mathit{prime}$ and $\mathit{odd}$ , and binary relation $<$ , interpreted in the natural way over domain ${\mathbb N}$ . The sentence $\forall x \; (2 < x \wedge \mathit{prime}(x) \to \mathit{odd}(x))$ expresses the fact that every prime number bigger than 2 is odd. It is an example of relativization , discussed in Section 7.4 . We can now see semantically how relativization works. This sentence is true in our model if, for every natural number $n$ , interpreting $x$ as $n$ makes the sentence true. If we interpret $x$ as 0, 1, or 2, or as any non-prime number, the hypothesis of the implication is false, and thus $2 < x \wedge \mathit{prime}(x) \to \mathit{odd}(x)$ is true. Otherwise, if we interpret $x$ as a prime number bigger than 2, both the hypothesis and conclusion of the implication are true, and $2 < x \wedge \mathit{prime}(x) \to \mathit{odd}(x)$ is again true. Thus the universal statement holds. It was an example like this that partially motivated our semantics for implication back in Chapter 3; any other choice would make relativization impossible.

For the next example, we will consider models that are given by a rectangular grid of “dots.” Each dot has a color (red, blue, or green) and a size (small or large). We use the letter $R$ to represent a large red dot and $r$ to represent a small red dot, and similarly for $G, g, B, b$ .

The logical language we use to describe our dot world has predicates $\mathit{red}$ , $\mathit{green}$ , $\mathit{blue}$ , $\mathit{small}$ and $\mathit{large}$ , which are interpreted in the obvious ways. The relation $\mathit{adj}(x, y)$ is true if the dots referred to by $x$ and $y$ are touching, not on a diagonal. The relations $\mathit{same{\mathord{\mbox{-}}}color}(x, y)$ , $\mathit{same{\mathord{\mbox{-}}}size}(x, y)$ , $\mathit{same{\mathord{\mbox{-}}}row}(x, y)$ , and $\mathit{same{\mathord{\mbox{-}}}column}(x, y)$ are also self-explanatory. The relation $\mathit{left{\mathord{\mbox{-}}}of}(x, y)$ is true if the dot referred to by $x$ is left of the dot referred to by $y$ , regardless of what rows the dots are in. The interpretations of $\mathit{right{\mathord{\mbox{-}}}of}$ , $\mathit{above}$ , and $\mathit{below}$ are similar.

Consider the following sentences:

$\forall x \; (\mathit{green}(x) \vee \mathit{blue}(x))$

$\exists x, y \; (\mathit{adj}(x, y) \wedge \mathit{green}(x) \wedge \mathit{green}(y))$

$\exists x \; ((\exists z \; \mathit{right{\mathord{\mbox{-}}}of}(z, x)) \wedge (\forall y \; (\mathit{left{\mathord{\mbox{-}}}of}(x, y) \to \mathit{blue}(y) \vee \mathit{small}(y))))$

$\forall x \; (\mathit{large}(x) \to \exists y \; (\mathit{small}(y) \wedge \mathit{adj}(x, y)))$

$\forall x \; (\mathit{green}(x) \to \exists y \; (\mathit{same{\mathord{\mbox{-}}}row}(x, y) \wedge \mathit{blue}(y)))$

$\forall x, y \; (\mathit{same{\mathord{\mbox{-}}}row}(x, y) \wedge \mathit{same{\mathord{\mbox{-}}}column}(x, y) \to x = y)$

$\exists x \; \forall y \; (\mathit{adj}(x, y) \to \neg \mathit{same{\mathord{\mbox{-}}}size}(x, y))$

$\forall x \; \exists y \; (\mathit{adj}(x, y) \wedge \mathit{same{\mathord{\mbox{-}}}color}(x, y))$

$\exists y \; \forall x \; (\mathit{adj}(x, y) \wedge \mathit{same{\mathord{\mbox{-}}}color}(x, y))$

$\exists x \; (\mathit{blue}(x) \wedge \exists y \; (\mathit{green}(y) \wedge \mathit{above}(x, y)))$

We can evaluate them in this particular model:

R	r	g	b
R	b	G	b
B	B	B	b

There they have the following truth values:

For each sentence, see if you can find a model that makes the sentence true, and another that makes it false. For an extra challenge, try to make all of the sentences true simultaneously. Notice that you can use any number of rows and any number of columns.

10.4. Validity and Logical Consequence ¶

We have seen that whether a formula is true or false often depends on the model we choose. Some formulas, though, are true in every possible model. An example we saw earlier was $\forall y \; (\mathit{le}(0, y) \to \mathit{le}(0, y))$ . Why is this sentence valid? Suppose ${\mathcal M}$ is an arbitrary model of the language, and suppose $a$ is an arbitrary element of the domain of ${\mathcal M}$ . Either ${\mathcal M} \models \mathit{le}(0, \bar a)$ or ${\mathcal M} \models \neg \mathit{le}(0, \bar a)$ . In either case, the propositional semantics of implication guarantee that ${\mathcal M} \models \mathit{le}(0, \bar a) \to \mathit{le}(0, \bar a)$ . We often write $\models A$ to mean that $A$ is valid.

In the propositional setting, there is an easy method to figure out if a formula is a tautology or not. Writing the truth table and checking for any rows ending with $\mathbf{F}$ is algorithmic, and we know from the beginning exactly how large the truth table will be. Unfortunately, we cannot do the same for first-order formulas. Any language has infinitely many models, so a “first-order” truth table would be infinitely long. To make matters worse, even checking whether a formula is true in a single model can be a non-algorithmic task. To decide whether a universal statement like $\forall x \; P(x)$ is true in a model with an infinite domain, we might have to check whether $P$ is true of infinitely many elements.

This is not to say that we can never figure out if a first-order sentence is a tautology. For example, we have argued that $\forall y \; (\mathit{lt}(0, y) \to \mathit{lt}(0, y))$ was one. It is just a more difficult question than for propositional logic.

As was the case with propositional logic, we can extend the notion of validity to a notion of logical consequence. Fix a first-order language, $L$ . Suppose $\Gamma$ is a set of sentences in $L$ , and $A$ is a sentence of $L$ . We will say that $A$ is a logical consequence of $\Gamma$ if every model of $\Gamma$ is a model of $A$ . This is one way of spelling out that $A$ is a “necessary consequence” of $A$ : under any interpretation, if the hypotheses in $\Gamma$ come out true, $A$ is true as well.

10.5. Soundness and Completeness ¶

In propositional logic, we saw a close connection between the provable formulas and the tautologies—specifically, a formula is provable if and only if it is a tautology. More generally, we say that a formula $A$ is a logical consequence of a set of hypotheses, $\Gamma$ , if and only if there is a natural deduction proof of $A$ from $\Gamma$ . It turns out that the analogous statements hold for first order logic.

The “soundness” direction—the fact that if $A$ is provable from $\Gamma$ then $A$ is true in any model of $\Gamma$ —holds for reasons that are similar to the reasons it holds in the propositional case. Specifically, the proof proceeds by showing that each rule of natural deduction preserves the truth in a model.

The completeness theorem for first order logic was first proved by Kurt Gödel in his 1929 dissertation. Another, simpler proof was later provided by Leon Henkin.

Theorem. If a formula $A$ is a logical consequence of a set of sentences $\Gamma$ , then $A$ is provable from $\Gamma$ .

Compared to the version for propositional logic, the first order completeness theorem is harder to prove. We will not go into too much detail here, but will indicate some of the main ideas. A set of sentences is said to be consistent if you cannot prove a contradiction from those hypotheses. Most of the work in Henkin’s proof is done by the following “model existence” theorem:

Theorem. Every consistent set of sentences has a model.

From this theorem, it is easy to deduce the completeness theorem. Suppose there is no proof of $A$ from $\Gamma$ . Then the set $\Gamma \cup \{ \neg A \}$ is consistent. (If we could prove $\bot$ from $\Gamma \cup \{ \neg A \}$ , then by the reductio ad absurdum rule we could prove $A$ from $\Gamma$ .) By the model existence theorem, that means that there is a model ${\mathcal M}$ of $\Gamma \cup \{ \neg A \}$ . But this is a model of $\Gamma$ that is not a model of $A$ , which means that $A$ is not a logical consequence of $\Gamma$ .

The proof of the model existence theorem is intricate. Somehow, from a consistent set of sentences, one has to build a model. The strategy is to build the model out of syntactic entities, in other words, to use terms in an expanded language as the elements of the domain.

The moral here is much the same as it was for propositional logic. Because we have developed our syntactic rules with a certain semantics in mind, the two exhibit different sides of the same coin: the provable sentences are exactly the ones that are true in all models, and the sentences that are provable from a set of hypotheses are exactly the ones that are true in all models of those hypotheses.

We therefore have another way to answer the question posed in the previous section. To show that a sentence is valid, there is no need to check its truth in every possible model. Rather, it suffices to produce a proof.

10.6. Exercises ¶

In a first-order language with a binary relation, $R(x,y)$ , consider the following sentences:

$\exists x \; \forall y \; R(x, y)$

$\exists y \; \forall x \; R(x, y)$

$\forall x,y \; (R(x,y) \wedge x \neq y \to \exists z \; (R(x,z) \wedge R(z,y) \wedge x \neq z \wedge y \neq z))$

For each of the following structures, determine whether of each of those sentences is true or false.

the structure $(\mathbb N, \leq)$ , that is, the interpretation in the natural numbers where $R$ is $\leq$

the structure $(\mathbb Z, \leq)$

the structure $(\mathbb Q, \leq)$

the structure $(\mathbb N, \mid)$ , that is, the interpretation in the natural numbers where $R$ is the “divides” relation

the structure $(P(\mathbb N), \subseteq)$ , that is, the interpretation where variables range over sets of natural numbers, where $R$ is interpreted as the subset relation.

Create a 4 x 4 “dots” world that makes all of the following sentences true:

$\exists x \; (\exists z \; \mathit{right{\mathord{\mbox{-}}}of}(z, x) \wedge \forall y \; (\mathit{left{\mathord{\mbox{-}}}of}(x, y) \to \mathit{blue}(y) \vee \mathit{small}(y)))$

$\forall x, y \; (\mathit{same{\mathord{\mbox{-}}}row}(x, y) \wedge \mathit{same\mathord{\mbox{-}} column}(x, y) \to x = y)$

$\exists y \; \forall x \; (\mathit{adj}(x, y) \to \mathit{same{\mathord{\mbox{-}}}color}(x, y))$

Fix a first-order language $L$ , and let $A$ and $B$ be any two sentences in $L$ . Remember that $\vDash A$ means that $A$ is valid. Unpacking the definitions, show that if $\vDash A \wedge B$ , then $\vDash A$ and $\vDash B$ .

Give a concrete example to show that $\vDash A \vee B$ does not necessarily imply $\vDash A$ or $\vDash B$ . In other words, pick a language $L$ and choose particular sentences $A$ and $B$ such that $A \vee B$ is valid but neither $A$ nor $B$ is valid.

Consider the three formulas $\forall x \; R(x, x)$ , $\forall x\; \forall y \; (R (x, y) \to R (y, x))$ , and $\forall x \; \forall y \; \forall z \; (R(x, y) \wedge R(y, z) \to R(x, z))$ . These sentences say that $R$ is reflexive, symmetric, and trainsitive. For each pair of sentences, find a model that makes those two sentences true and the third false. This shows that these sentences are logically independent: no one is entailed by the others.

Show that if a set of formulas $\{\psi_1, \ldots, \psi_n\}$ is semantically inconsistent, then it entails every formula $\phi$ . Does the converse also hold?

Give a formula $\psi$ such that the set $\{P(c), \neg P(D), \psi \}$ is consistent, and so is the set $\{P(c), \neg P(D), \neg \psi \}$ .

For each the following formulas, show whether the formula is valid, satisfiable, or unsatisfiable.

$\exists x \; \forall y \; R (y, x) \wedge R (x, y)$

$(\exists x \; \forall y \; R (x, y)) \to (\exists x \; \exists y \; R (x, y))$

$(\exists x\; P (x)) \wedge (\exists x \; \neg P(x))$

Logic and Proof

1. Introduction
2. Propositional Logic
3. Natural Deduction for Propositional Logic
4. Propositional Logic in Lean
5. Classical Reasoning
6. Semantics of Propositional Logic
7. First Order Logic
8. Natural Deduction for First Order Logic
9. First Order Logic in Lean
10.1. Interpretations
10.2. Truth in a Model
10.3. Examples
10.4. Validity and Logical Consequence
10.5. Soundness and Completeness
10.6. Exercises
12. Sets in Lean
13. Relations
14. Relations in Lean
15. Functions
16. Functions in Lean
17. The Natural Numbers and Induction
18. The Natural Numbers and Induction in Lean
19. Elementary Number Theory
20. Combinatorics
21. The Real Numbers
22. The Infinite
23. Axiomatic Foundations
24. Appendix: Natural Deduction Rules
PDF version

Quick search

11. Implementing First-Order Logic
View page source

11. Implementing First-Order Logic 

Our implementation of first-order logic in Lean is similar to our implementation of propositional logic in Lean, covering both the syntax and the semantics. We will also show how to implement unification , and algorithm that is fundamental to the mechanization of first-order reasoning.

11.1. Terms 

Our implementation of terms is straightforward.

A term is either a variable or a function symbol applied to a list of terms. We have defined syntax for FOTerm :

The notation %x is used for a variable. Notice that a constant like c is represented as an application of the symbol to the empty list. Notice also that the definition does nothing to check the arity of the function symbols. Ordinarily, first-order logic allows us to specify that f and g are binary functions and that another function, h , is unary. Our definition of FOTerm allows the application of any string to any number of arguments. This simplifies a number of aspects of the implementation. As an exercise, you might want to write a function well-formed in Lean that, given a specification of a list of symbols and their arities, checks that an FOTerm uses only those symbols and with the correct arity. Later in the course, we will talk about systems more expressive than first-order logic that provide other ways of specifying a function’s intended arguments. Lean’s type system provides a very elaborate and expressive means for doing so, and you can think of the specification of arities in first-order logic as being a minimal form of a typing judgment.

Remember that to evaluate a first-order language, we need an assignment of values to the variables, as well as interpretations of the function and relation symbols. Since our symbols are identified as strings, in general an interpretation of symbols is an assignment of values to strings:

Any function definable in Lean can serve this purpose. Keep in mind that we have to fix a type α , corresponding to the universe of the structure in which we carry out the interpretation.

Since it is often useful to specify an assignment by giving a finite list of values, we have implemented syntax for that:

You can type the symbol ↦ as \mapsto . Formally, the notation produces an association list , essentially just a list of key / value pairs. But we have also told Lean how to coerce such an association list to an FOAssignment when necessary. The following examples provide a few different Lean idioms for specifying that an assign! expression should be interpreted as an FOAssignment . (It should also happen automatically when you pass such an expression as an argument to a function that expects an FOAssignment .)

It is now easy to define substitution for terms. Such a function should take a term and an assignment of terms to variables, and replace the variables by the assigned terms.

Here we try it out:

11.2. Evaluating terms 

To evaluate a term, we need not only an assignment of values to the variables occurring in the term, but also an interpretation of all the function symbols. Setting aside concerns about arities, we can interpret any function taking some number of elements of α to α as an element of type List α → α .

If a function is intended to be used as a binary function, we really care about the interpretation when it is applied to lists of length two. In our quick-and-dirty implementation, we have to define values for lists of other lengths, but any values will do. For example, we can define an interpretation of constants and functions on the natural numbers as follows:

Or, alternatively:

With FnInterp in place, it is easy to define a function that evaluates terms:

Even though the function always terminates, Lean 4 is not yet able to prove termination automatically, so we use the keyword partial . Let’s try it out.

When we talked about propositional logic, we proved a theorem that says that evaluating the result of a substitution is the same as evaluating the original formula relative to an assignment of the values of the substituted formula. In the context of terms, the identity is as follows:

The proof is essentially the same. Our current implementation is more general in that it allows us to substitute multiple terms at once, but we can see the principle at play in the fact that the two evaluations below produce the same answer.

And here is another crazy idea: we can view substitution as the result of evaluating a term in a model where the universe consists of terms, and where each function symbol f is interpreted as the function “build a term by applying f .”

You should think about what is going on here. Such a model is known as a term model .

11.3. Formulas 

Since the universe of a first-order model may be infinite, we would not expect to be able to evaluate arbitrary first-order formulas in an arbitrary model. Evaluating quantifiers in our model of arithmetic would require testing instantiations to all the natural numbers. If we could do that, we could easily settle the truth of the sentence

which says that there are infinitely many values $y$ such that $y$ and $y + 2$ are both prime. This is known as the twin primes conjecture , and it is a major open question in number theory.

We can, however, evaluate quantifiers over finite universes. In the definition of a first-order model below, we assume that the universe is given by a finite list of values.

In our quick-and-dirty implementation, we don’t require that the universe univ is closed under the functions. In other words, it’s possible that we can apply a function to some elements on the list univ and get something that isn’t in the list. It wouldn’t be hard to write a procedure that checks that, given a finite list of functions and their intended arities. (A more efficient way of handling this is instead to prove that the functions all return values in universe, using Lean’s theorem proving capabilities.) In the examples in this section, we won’t use function symbols at all, except for some constants that are clearly o.k.

To handle the quantifiers, we need a procedure that takes an assignment $\sigma$ and produces an updated assignment $\sigma[x \mapsto v]$ .

With that in hand, the evaluation function is entirely straightforward.

Let’s try it out on a baby model of arithmetic that only has the numbers 0 to 9 in the universe. We reuse the function interpretation arithFnInterp from before, so that we have the constants zero , one , two , and three . The interpretation also gives us addition and multiplication, but we won’t use those. As far as relations, we interpret two: the binary less-than relation lt and the predicate even . We also define the trivial assignment which assigns 0 to all the variables.

We can try it out:

It’s an unpleasant feature of our syntax that we have to put a percent sign in front of variables in order to distinguish them from constants, while we do not use the percent sign with the quantifiers. To facilitate testing sentences, we write a simple function testeval that evaluates any formula in our model with respect to the trivial variable assignment.

A software package called Tarski’s World by Jon Barwise and John Etchemendy offers a fun way of experimenting with first-order logic. It allows users to lay down blocks on an $8 \times 8$ grid and evaluate sentences about them. Each block is either a tetrahedron, a cube, or a dodecahedron, and each is either small, medium, or large. The language includes predicates for these, as well as relations like FrontOf(x, y) and Between(x, y, z) . The second one of these holds if and only if x , y , and z are either in the same row, in the same column, or on the same diagonal, and x is between y and z .

The file TarskisWorld in the Examples folder includes a simple implementation in Lean. You can define a world and display it:

Here a plus symbol means that the object is large, a minus symbol means that it is small, and no symbol means that it is of medium size. You can then evaluate statements about the world:

The file TWExamples provides two puzzles, taken from Tarski’s World , for you to try.

11.4. Unification 

Suppose we are working with a language that is meant to describe the real numbers and we have either proved or assumed the following sentence:

Suppose also that we are trying to prove

Even though we haven’t talked about proof systems for first-order logic yet, it should be clear that we want to instantiate the universal quantifiers in the sentence by substituting $ab$ for $x$ , $c$ for $y$ , and $7$ for $z$ , so that the conclusion matches the goal.

You probably did not have to think about this much. You identified the problem as that of finding a substitution for $x$ , $y$ , and $z$ that has the effect of making the expression $x + z < y + z$ the same as $ab + 7 < c + 7$ . This is what is known as a matching problem for first-order terms. This kind of pattern matching is fundamental to reasoning, and hence also fundamental to logic. The general formulation of the problem is as follows: we are given pairs of terms $(s_1, t_1), (s_2, t_2), \ldots, (s_n, t_n)$ and we are looking for a substitution $\sigma$ with the property that for every $i$ , $\sigma \, s_i = t_i$ .

The generalization of the matching problem in which we are allowed to substitute for the variables in the terms $t_i$ as well as the terms $s_i$ is known as unification . In other words, the input to a unification problem is the same as before, but now we are looking for a substitution $\sigma$ with the property that for every $i$ , $\sigma \, s_i = \sigma \, t_i$ . For example, consider the following two expressions:

If we substitute $b$ for $x$ , $f(b, a)$ for $y$ , and $c$ for $z$ , both expressions become $f(b, f(b, a)) < c$ . When we discuss resolution proofs for first-order logic, we will see that such unification problems come up in a context where are are trying to prove a contradiction and we have derived something like $\fa {x, z} f(x, f(x, a)) < z$ and $\fa y f(b, y) \not< c$ . The unification problem tells us how to instantiate the universal quantifiers in order to prove a contradiction.

To prevent confusion in the future, we would like to point out that what counts as a variable or a constant depends on the context. For example, we can ask for an assignment to $x$ and $y$ that unifies $f(x, z)$ and $f(z, y)$ without assigning anything to $z$ . In that case, we are treating $x$ and $y$ as variables and $z$ as a constant. In Lean, the variables $x$ and $y$ that can be assigned in a unification problem are sometimes called metavariables and written as $?x$ and $?y$ . For simplicity, we will continue to use letters like $x$ , $y$ , and $z$ for variables and letters like $a$ , $b$ , and $c$ as constants. What is important when specifying a unification problem is simply that it is clear which symbols play the role of variables and which have to remain fixed.

There is a linear-time algorithm that solves any unification problem or determines that there is no solution, and, in fact produces a most general unifier , or mgu . A most general unifier $\sigma$ for a problem is a substitution that unifies each pair in the list and has the property that if $\tau$ is any unifier for the problem, then $\tau$ can be expressed as the result of following $\sigma$ by another substitution. Here we will describe such an algorithm, but we will not go so far as to prove its correctness or show that it produces a most general unifier. Our implementation is adapted from one by John Harrison in his Handbook of Practical Logic and Automated Reasoning , which is an excellent reference for most of the topics we cover in this book, and a lot more. In particular, it proves that the algorithm we describe below always terminates with a most general unifier if the pairs can be unified at all, and fails with none otherwise. There is also a nice presentation of unification in the book Term Rewriting and All that by Franz Baader and Tobias Nipkow.

Some unification problems are easy. To unify $x$ and $f(a, z)$ , we simply assign $x$ to $f(a, z)$ . To be a most general unifier, it is important that the resulting term, $f(a, z)$ has the variable z . We can also solve the problem by assigning $f(a, a)$ to $x$ and $a$ to $z$ , but that is less general. It can be seen as the result of mapping $x$ to $f(a, z)$ and then applying another substitution that maps $z$ to $a$ .

For another easy example, we can unify $f(x, b)$ and $f(g(c), b)$ by mapping $x$ to $g(c)$ . Since both expressions are of the form $f(\cdot, \cdot)$ , to unify the expressions it is clearly necessary and sufficient to unify the arguments. For the same reason, it is clear that $f(x, b)$ and $g(c)$ can’t be unified.

An interesting phenomenon arises with the unification problem $(x, f(y)), (y, g(x))$ . The first pair tells us we have to map $x$ to $f(y)$ , and the second pair tells us we have to map $y$ to $g(x)$ . Applying this substitution to each pair yields $(f(y), f(g(x)))$ in the first pair and $(g(x), g(f(y)))$ in the second, which doesn’t solve the problem. Repeating the substitution doesn’t help. The problem is that when we start with $x$ , we find a chain of assignments to variables in the terms on the right-hand side that ultimately leads to a term that involves $x$ . In others words, the list of associations contains a cycle . If we ever reach a point where we are forced to admit a cycle of associations, the algorithm should fail. This is known as the occurs check .

The algorithm below maintains an association list of pairs $(x, t)$ indicating that the variable $x$ should be unified with the term $t$ . (An association list is essentially just a list of pairs, but for efficiency it uses a constructor with three arguments to cons a pair onto the list.) Each variable $x$ occurs only once on the left side of a pair. We allow the list to contain pairs like $(x, y)$ , $(y, z)$ , and $(z, w)$ , since we can clean that up later, say, by assigning all the variables to $w$ .

Suppose we have an association list $\fn{env}$ and we are considering adding the pair $(x, t)$ . The following function returns some true if the assignment is trivial, which is to say, $t$ is $x$ or there is a chain of variable associations that amounts to assigning $x$ to $x$ . In that case, we can ignore the pair. The function returns some false for any nontrivial assignment, unless it detects a cycle, in which case it returns none to indicate failure.

With that in place, the following function takes an association list, env , and a list of pairs to unify, and it returns an association list. The clauses are as follows:

If the list of pairs is empty, there is nothing to do.

If the first pair on the list is a pair of function applications, then

if the pair is of the form $f(t_1, \ldots, t_n)$ and $f(s_1, \ldots, s_n)$ , add the pairs $(s_1, t_1) \ldots (s_n, t_n)$ to the list of pairs to unify and continue recursively, and

if the function symbols don’t match or the number of arguments is not the same, fail.

If the pair is of the form $(x, t)$ , then

if there is a pair $(x, s)$ already in $\fn{env}$ , add $(s, t)$ to the list of pairs to unify and continue recursively, and

otherwise add $(x, t)$ to $\fn{env}$ unless it is a trivial assignment, and continue recursively with the remaining pairs.

If the pair is of the form $(t, x)$ , then turn it around and recursively use the previous case.

The algorithm is implemented as follows.

The final association list might contain pairs $(x, t)$ and $(y, s)$ where $s$ contains the variable $x$ . This means that the variable $x$ has to unify with $t$ , which we can achieve by mapping $x$ to $t$ . But the resulting substitution will also replace $x$ in $s$ , so we had better carry out the substitution for $x$ there too. The following function, usolve , cleans up the list of pairs by iteratively substituting the terms on the right for the variables on the left, until the association list no longer changes. The fact that we have avoided cycles guarantees that it terminates. The function after that, fullUnify , puts it all together: given a list of pairs of terms to unify, it computes the association list and uses usolve to turn it into a substitution.

Below we try the procedure out by computing some unifiers and applying them to the original pairs to make sure that the pairs are indeed unified.

First-Order Logic: Formulas, Models, Tableaux

Cite this chapter.

Mordechai Ben-Ari 2

9613 Accesses

3 Altmetric

The axioms and theorems of mathematics are defined on sets such as the set of integers $ Z $ . We need to be able to write and manipulate logical formulas that contain relations on values from arbitrary sets. First-order logic is an extension of propositional logic that includes predicates interpreted as relations on a domain.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Available as PDF
Read on any device
Instant download
Own it forever
Available as EPUB and PDF
Compact, lightweight edition
Dispatched in 3 to 5 business days
Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

M. Fitting. First-Order Logic and Automated Theorem Proving ( Second Edition ). Springer, 1996.

Book MATH Google Scholar

A. Nerode and R.A. Shore. Logic for Applications ( Second Edition ). Springer, 1997.

R.M. Smullyan. First-Order Logic . Springer-Verlag, 1968. Reprinted by Dover, 1995.

Download references

Author information

Authors and affiliations.

Department of Science Teaching, Weizmann Institute of Science, Rehovot, Israel

Prof. Mordechai Ben-Ari

You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

About this chapter

Ben-Ari, M. (2012). First-Order Logic: Formulas, Models, Tableaux. In: Mathematical Logic for Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-4129-7_7

Download citation

DOI : https://doi.org/10.1007/978-1-4471-4129-7_7

Publisher Name : Springer, London

Print ISBN : 978-1-4471-4128-0

Online ISBN : 978-1-4471-4129-7

eBook Packages : Computer Science Computer Science (R0)

Share this chapter

Anyone you share the following link with will be able to read this content:

Sorry, a shareable link is not currently available for this article.

Provided by the Springer Nature SharedIt content-sharing initiative

Publish with us

Policies and ethics

Find a journal
Track your research

Stack Overflow Public questions & answers
Stack Overflow for Teams Where developers & technologists share private knowledge with coworkers
Talent Build your employer brand
Advertising Reach developers & technologists worldwide
Labs The future of collective knowledge sharing
About the company

Collectives™ on Stack Overflow

Find centralized, trusted content and collaborate around the technologies you use most.

Q&A for work

Connect and share knowledge within a single location that is structured and easy to search.

Get early access and see previews of new features.

First order logic assignment

I don't understand the assignment in this image:

respectively:

α[x↦a](x)=a α[x↦a](y)=α(y) for y≠x

Someone,can help me?

variable-assignment
first-order-logic

I've inlined the image. I presume your confusion is with the two that have "if for (some/every) a ...". Can you explain what parts of it you do (think you) understand and what part(s) are confusing to you please (please edit your question to add this information) – Damien_The_Unbeliever Commented Aug 22, 2018 at 10:09
I'm sorry. Done! – Luca Commented Aug 22, 2018 at 10:43

We start with α being an assignment. These final lines are saying that α[x↦a] produces a new assignment. In this new assignment (first line), x is now a . And for all other variables that aren't x (second line), whatever they were in the old assignment α is what they still are in this new assignment.

Both lines have to be read/interpreted together.

(Apologies if some of my terminology is a bit off in the above. I haven't had to discuss this topic for quite a long time)

Ok i understand your explanation.So y is used to say for all other variables doesn’t change nothing.is correct? – Luca Commented Aug 23, 2018 at 20:41
@Luca - yep, y is a metavariable here, standing for other variables. – Damien_The_Unbeliever Commented Aug 24, 2018 at 5:24

Your Answer

Reminder: Answers generated by artificial intelligence tools are not allowed on Stack Overflow. Learn more

Sign up or log in

Post as a guest.

Required, but never shown

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy .

Not the answer you're looking for? Browse other questions tagged variable-assignment assign first-order-logic or ask your own question .

Featured on Meta
Upcoming sign-up experiments related to tags
The 2024 Developer Survey Is Live
The return of Staging Ground to Stack Overflow
Policy: Generative AI (e.g., ChatGPT) is banned

Hot Network Questions

Convention of parameter naming - undocumented options
Are there any precautions I should take if I plan on storing something very heavy near my foundation?
Ideal test/p-value calculation for difference in means with small sample size and right skewed data?
Cannot install gnome-control-center upon upgrading Ubuntu (unmet dependencies with libpython3.10)
Does anyone know what Psatlees is more than it has something to do with silk?
Project Euler 127 - abc-hits
What is PS1 prompt \[\e]0; vs \[\e]2; , it looks like one is for title name of tab, one is for title name of windows
Why is "Colourless green ideas sleep furiously" considered meaningless?
How to avoid getting scammed?
UTF-8 characters in POSIX shell script *comments* - anything against it?
What was the first modern chess piece?
Has Marvel shown Thor's hammer, Mjolnir, breaking through Invisible Woman's force fields?
What will happen if we keep bringing two protons closer and closer to each other, starting from a large distance?
A Fantasy movie with a powerful humanoid being that lives in water
Was Croatia the first country to recognize the sovereignity of the USA? Was Croatia expecting military help from USA that didn't come?
Am I wasting my time self-studying program pre-requisites?
How to temporarily disable a primary IP without losing other IPs on the same interface
Does the NJ Sewerage Authorities Act say that failure to receive bills does not exempt late charges?
Recommendations Modifying/increasing a bicycles Max Weight limits
Possible negative connotations of "Messy Kitchen" for a blog and social media project name
Am I using "for your peace of mind" correctly: "You should back up your file for your peace of mind"? Is the phrase equal to "to feel secure"?
Question regarding validity of argument
How much time is needed to judge an Earth-like planet to be safe?
How do languages where multiple files make up a module handle combining them into one translation/compilation unit?

IMAGES

First Order Logic (Solved Problems)
Lecture 14-3 First-order logic substitution
Introduction to First Order Logic
PPT
What is first-order logic (FOL)?
First Order Logic (Solved Problems)

VIDEO

First Order Logic 1
Propositional and first order Logic
DM-21-First order logic Inference rules, GATE problems
First Order Logic
First Order Logic 3
First order logic Part 1

COMMENTS

First-order logic
First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. ... First, the variable assignment μ can be extended to all terms of the language, with the result that each term maps to a single element of the ...
PDF First-Order Logic
What is First-Order Logic? First-order logic is a logical system for reasoning about properties of objects. Augments the logical connectives from propositional logic with predicates that describe properties of objects, functions that map objects to one another, and quantifiers that allow us to reason about many objects at once.
PDF Notes on First Order Logic
2.2 First Order Models De nition 2.4 (Model) A model is a pair A = hW;Iiwhere W is a nonempty set (called the domain) and I is a function (called the interpretation) assigning to each function symbol F, a function denoted FI, to each constant symbol, an element of Wdenoted cI and to each predicate symbol P, a relation on Wof the appropriate arity.
PDF First-Order Logic
First-Order Logic is the calculus one usually has in mind when using the word ''logic''. It is expressive enough for all of mathematics, ... Definition 10.3.1 A first-order valuation v of EU is an assignment of truth values to elements of EU such that (1) v is a boolean valuation of EU, i.e. v[:A] = t iff v[A] = f
Introduction to Logic
The resulting logic is called First-Order Logic. In this chapter, we start by introducing the idea of a language-independent space of objects. ... That is, there is exactly one Herbrand Logic truth assignment over the language {a,b,c,d,e, on} that satisfies the above set of sentences. In contrast, under First-Order Logic, the set of five object ...
PDF First-Order Logic
Introduction Part 1: First-Order Logic • formalizes fundamental mathematical concepts • expressive (Turing-complete) • not too expressive (not axiomatizable: natural numbers, uncountable sets) • rich structure of decidable fragments • rich model and proof theory First-order logic is also called (ﬁrst-order) predicate logic. Ruzica Piskac First-Order Logic - Syntax, Semantics ...
PDF First Order Logic
First Order Logic Mahesh Viswanathan Fall 2018 First order logic is a formal language to describe and reason about predicates. Modern e orts to study ... An assignment maps every variable to an element in the universe of the structure. De nition 9. For a ˝-structure A, an assignment over Ais a function : V!u(A) that assigns every ...
PDF 1 Syntax of First-Order Logic
First-Order Logic James Worrell First-order logic can be understood as an extension of propositional logic. In propositional logic the ... Given a signature σ, a σ-structure (or assignment) Aconsists of: • a non-empty set U Acalled the universe of the structure; • for each k-ary predicate symbol Pin σ, a k-ary relation P A⊆U A× ...
PDF Lecture 15: Semantics of First Order Logic
Lecture 15: Semantics of First Order Logic 1 Review The vocabulary of predicate calculus consists of predicate symbols (with arity), ... A,α|= ϕwhere Ais a structure, ϕis a formula and αis a variable assignment, i.e., α: Var→ D. Note that our notion of truth is now a ternary relation, as opposed to the binary relation of propositional logic.
PDF First Order Logic
First Order Logic. First Order Logic extends Propositional Logic with. Non-boolean constants. Variables, functions and relations (or predicates, more generally) Quantification of variables. Sample first order formula: ∀x. ∃y. x < y. ∧ y ≤ x + 1. "for each x, there exists y such that (x is less than y) and (y is less or equal than x ...
PDF 2. First-Order Logic (FOL)
Assignment αI each variable x assigned value xI ∈ DI each n-ary function f assigned fI: Dn I → DI In particular, each constant a (0-ary function) assigned value aI ∈ DI each n-ary predicate p assigned p I: Dn → {true, false} In particular, each propositional variable P (0-ary predicate) assigned truth value (true, false) 2- 7 Example:
PDF First Order Logic
An interpretaon of a sentence (wff) is an assignment that maps. Object constants to objects in the worlds, n-ary funcon symbols to n-ary funcons in the world, n-ary relaon symbols to n-ary relaons in the world. Given an interpretaon, an atom has the value "true" if it denotes a relaon that holds for those individuals denoted in the terms.
Knowledge Representation and Reasoning: First Order Logic
This page defines first order logic, following the same general structure as in the general definitions of a logic. ... Given an interpretation (Δ, 𝓘), a variable assignment (or simply assignment) is a mapping μ : V Δ from variables to elements of the universe of interpretation. For an interpretation (Δ, ...
PDF 8 FIRST-ORDER LOGIC
We used propositional logic as our representation language because it sufﬁced to illustrate the basic concepts of logic and knowledge-based agents. Unfortunately, propositional logic is too puny a language to represent knowledge FIRST›ORDER LOGIC of complex environments in a concise way. In this chapter, we examine ﬁrst-order logic,1
PDF Semantics of First-Order Logic
Semantics of First-Order Logic syn.1 Introduction fol:syn:its: sec Giving the meaning of expressions is the domain of semantics. The central ... Thedomaintogether with assignments to the basic vocabulary constitutesastructure.Variablesmay appear informulas, and in order to give a semantics, we also have to assignelementsof thedo- ...
What is the signficance and intended purpose of variable assignments in
In so many words: what use is the notion of a variable assignment in first-order logic? Why care about variable assignments at all? I'm not asking "what is a variable assignment?" I know what a variable assignment is: it's a function that maps from every variable in a (fragment of) a language to an element of the domain in the model for that ...
PDF Semantics of First-Order Logic
first-order language, and assigning them values xU = yU = zU = a. This assignment is completely arbitrary, and in fact, in general the initially given assign-ment function serves only to get us "off the ground" in the recursive semantic interpre-tation of our first-order language. As we shall see, the values assigned to variables will
3.1: First Order Logic Syntax and Semantics
From Natural Language to First order logic (or vv.). Consider the following three sentences: - " Each animal is an organism". - " All animals are organisms". - " If it is an animal then it is an organism". This can be formalised as: Observe the colour coding in the natural language sentences: 'each' and 'all' are ...
7. First Order Logic
7.2. The Universal Quantifier¶. What makes first-order logic powerful is that it allows us to make general assertions using quantifiers.The universal quantifier $\forall$ followed by a variable $x$ is meant to represent the phrase "for every $x$."In other words, it asserts that every value of $x$ has the property that follows it. Using the universal quantifier, the examples with ...
10. Semantics of First Order Logic
10.2. Truth in a Model¶. Fix a first-order language. Suppose we have chosen a domain $D$ in which to interpret the language, along with an interpretation in $D$ of each of the symbols of that language. We will call this structure—the domain $D$, paired with the interpretation—a model for the language. A model for a first-order language is directly analogous to a truth assignment for ...
11. Implementing First-Order Logic
Implementing First-Order Logic. Our implementation of first-order logic in Lean is similar to our implementation of propositional logic in Lean, covering both the syntax and the semantics. We will also show how to implement unification, and algorithm that is fundamental to the mechanization of first-order reasoning. 11.1.
First-Order Logic: Formulas, Models, Tableaux
First-order logic is an extension of propositional logic that includes predicates interpreted as relations on a domain. Download chapter PDF. Keywords. ... Semantics (Sect. 7.3): An interpretation consists of a domain and an assignment of relations to the predicates. The semantics of the Boolean operators remains unchanged, but the evaluation ...
assign
We start with α being an assignment. These final lines are saying that α[x↦a] produces a new assignment. In this new assignment (first line), x is now a.And for all other variables that aren't x (second line), whatever they were in the old assignment α is what they still are in this new assignment.. Both lines have to be read/interpreted together.