3.3. FO in FO(·): Formulas

3.3 Formulas

An expression of type boolean is called a formula. Formulas are built by using boolean operators to combine atomic formulas into larger formulas. An atomic formula can be:

• A user-defined predicate `P: ... -> Bool` applied to an appropriate set of arguments;
• A built-in comparison operator applied to two arguments, such as `=` and `~=`, which are applicable to values of any type, and the operators `>=, =<, <, >`, which are applicable to numerical values.

3.3.1 Basic boolean operators

There are three basic operators on boolean expressions:

• The unary not-operator `~`
• The binary and-operator `&`
• The binary or-operator `|`

In addition, round brackets `(` and `)` can be used to group expressions. In the absence of brackets, the precedence of the operators corrresponds to the order in which they are listed above. For instance, `~p() | q() & r()` is identical to `(~p()) | (q() & r())`.

Exercise

The following theory expresses that one or both of `p` and `q` must be true:

Consequently, as you can verify by clicking the "run" button, this theory has three models: only `p`, only `q`, and both `p` and `q`. The only structure that is not a model is therefore the one in which both `p` and `q` are false.

Can you rewrite the above theory into an equivalent theory (i.e., one which has the same three models as this theory) that uses only the "and" and "not" operators, but no longer the "or" operator?

Can you change the above theory to express an "exclusive or", i.e., that either `p` or `q` is true, but not both. This theory should therefore have only two models instead of three.

As the first of these two exercises shows, the "or"-operator is actually redundant, since we can express it using a combination of "and" and "not". (Alternatively, we can also express the "and" in terms of "or" and "not", so also "and" is redundant once we have the other two.) Of course, there are good reasons for nevertheless having all three operators. One reason is that formulas can be written in a more compact and legible way if we have "or" available as an abbreviation for the more complex formula that uses "and" and "not". Another reason is that "or" appears to a primitive of human thought: it is part of how knowledge is structured in the human brain and therefore its presence in the language is necessary to allow natural representations of this knowledge.

The second of the two exercises above illustrates an important caveat: in everyday speech, we often use the same word for different concepts, counting on our common-sense to figure out which meaning is intended. Compare, for instance, the following two uses of the word "or".

• One detective to another: "The suspect must have left his fingerprints on the gun or on the bullets."
• The robber to the victim: "Give me the money or I'll shoot!"

In the first example, the intended meaning of the word "or" is the "inclusive or" (which has three models), while in the second example it is the "exclusive or" (which has only two models). These different uses of the same word are often entirely unproblematic, since people are typically very good at figuring out which meaning is intended. When building formal representation of knowledge, however, it is important to be aware of the fact that such different meaning exist, and that each operator in the formal language of course only has a single meaning (that of "inclusive or", in this case).

3.3.2 Implications and equivalences

This section introduces two new boolean operators. Similar to the "or", these operators are redundant, in the sense that they can be seen as abbrevations for expressions involving the basic boolean operator. However, they too seem to correspond to how knowledge is structured in our brains and are therefore important to have in the formal language.

The first is the implication operator, which is written as `F => G`. We read this as "`F` implies `G`" or more simply as "if `F` then `G`". Similar to "or", the "if … then …" construct is also used in different meanings in natural language. The implication operator captures the meaning that "if" has in the following example:

• One member of the bomb squad to another: "If the drawing we found in the suspect's apartment is correct, then the red wire is the one we should cut."

There are four situations, of which three are possible according to this statement:

• The drawing is correct and the red wire is the right one.
• The drawing is incorrect and the red wire is not the one to cut.
• The drawing is incorrect but the red wire is the one to cut anyway.

Therefore, this statement only rules out one situation, namely this one:

• The drawing is correct and the red wire is not the one to cut.

This immediately also shows us that `F => G` can indeed be seen as an abbreviation for an expression in the basic boolean operators, namely `~(F & ~G)`. As we learned from an earlier exercise, this expression is equivalent to `~F | G`. In other words, as long as the "if"-part of the statement is not true or the "then" part is true (or both are true), the entire statement is true.

Exercise

Try to express the above example using the boolean variables `drawing` and `red_wire`.

Exercise

The following snippet expresses that `~p() => ~q()`. Can you rewrite this using only "and"- and "not"-operators? Try it without executing the snippet first!

Again, it is important to know that this is the meaning of "if … then" that is captured by the `=>` operator. The case that might create confusion is the "or both" case, i.e., the fact that it is possible that the "if"-part of the statement is false, but the "then"-part is true anyway. To illustrate, consider the following other use of "if":

• A natural number is called prime if it is strictly greater than one and does not have any divisors other than one and itself.

Here, the word "if" is being used with a different meaning, that does not correspond to the `=>` in FO. The difference here is that the statement is intended to define what prime numbers are, so it should not be possible that the "if"-part is false for some number, but that this number is prime anyway. While it should be clear to a typical reader that this is the intended meaning of the statement, mathematicians may prefer to be more explicit about this, in order to make absolutely sure that the statement will be unambiguously understood. In this case, a mathematician may say:

• A natural number is called prime if and only if it is strictly greater than one and does not have any divisors other than one and itself.

The use of the "if and only if" removes any room for misunderstanding. Such a statement is called an equivalence and is denoted in FO by a double arrow `<=>`. An expression `F <=> G` is true if (and only if) `F` and `G` have the same truth value. In other words, the following two situations are possible:

• A number is prime and satisfies the condition of being `>1` and having no non-trivial divisors.
• A number is not prime and does not satisfy this condition.

The following two situations are not possible:

• A number is not prime even though it satisfies the condition.
• A number is prime even though it does not satisfy the condition.

This last case is the one which distinguishes the equivalence `prime <=> condition` from an implication `prime <= condition`. The reason for the choice of a double-headed arrow as the symbol for equivalence is that `F <=> G` is identical to `(F => G) & (F <= G)`. In other words, `F` and `G` are equivalent if and only if `F` implies `G` and also `G` implies `G`.

(As a side remark, the IDP-Z3 software also allows to write `F <=> G` as `F = G`. It is slightly unusual to write an equivalence in this way, but it nevertheless of course makes perfect sense.)

Exercise

In a previous exercise, we saw that it is possible to express an "exclusive or" by a combination of "or", "not" and "and". Use the operators introduced in this section to define "exclusive or" by means of a shorter formula:

In our previous examples, it was always pretty clear whether the word "if" was intended as an implication or an equivalence. The following example is more debatable:

• Detective to witness: "If you don't testify in court, a dangerous criminal will go free."

Does the detective also intend to say that if the witness does testify, the criminal will not go free? This is a question for linguists or psychologists, but not for us. All that matters from a knowledge representation perspective is that once we know what the intended meaning of the statement actually is, we are able to translate it to an expression in the formal logic.

Exercise

Wason's Selection Task is a famous experiment in cognitive psychology. It is performed using a pack of cards, in which each card has a letter on one side and a number on the other side. Participants are shown one side of a few cards from this deck. They are then told the following rule: "If there is a D on one side of a card, then there is a 3 on the other side." Their task is to select those cards that could provide information about the truth or falsity of this rule, if they were to be turned over. Try it out yourself by selecting the correct card(s):

 D
 K
 3
 7

The correct answer is to select D and 7. If we turn over the D card and it shows something other than a 3, we know that the rule is false. (Participants typically get this right.) The K card and the 3 card are both irrelevant. (Participants often think that the 3 card is relevant, but it is not: even if its other side has something other than a D, the rule could still be true, because the statement is an implication not an equivalence.) The 7 is relevant, because if it has a D on the other side, it would be a counterexample to the rule. (Participants typically overlook this.)

As we discussed above, it is not always clear whether the word "if" in intended to denote an implication or an equivalence. In this case, there is nothing in the context to suggest that an equivalence is intended, so presumably everyone would agree that this "if" is an implication. In any case, the most striking thing about this experiment is the fact that people overlook the relevance of the 7, and this does not depend on how the "if" is interpreted.

3.3.3 Quantifiers

With what we have learned so far, we can make pretty complex statements, but only about a fixed number of values. For instance, our earlier expression `L() ~= E()` is a statement about two values, namely that referred to by the constant `L` and that referred to by `E`. The interesting thing about first-order logic is that it also allows to talk about all values of a given type, regardless of how many values there are. This is done using a quantifier of the form:

`!x in T : F`

Here, `T` is a type, `F` is a formula (i.e., a boolean expression), and `x` is a variable. A variable is a new kind of symbol, that we have not encountered before. Unlike other symbols, variables are not declared in a vocabulary. They are simply introduced by using them in a quantifier and they exist only in the scope of their quantifier. In other words, the variable `x` that is introduced by this quantifier can (only) be used in the formula `F`. More specifically, it can be used in `F` as an expression of type `T`.

The appearance of `x` in `F` means that we now need more than only a structure for the vocabulary (which does not contain `x`) to be able to determine the truth value of `F`: in addition to a structure, we also need to know which value of type `T` is assigned to the expression `x`. The meaning of the quantifier is now that the formula `!x in T: F` is true if and only if the formula `F` is true no matter which value of type `T` we assign to `x`. In other words, the formula `!x in T:F` expresses that `F` is true for each value `x` of type `T`.

Exercise

Earlier, we already saw a following vocabulary for describing coloured graphs. Using a quantifier, add a formula to the theory that expresses that all nodes must be coloured red.

Extra: Would you also be able to express this rule if the colors were defined in the structure instead? Try reformalising the specification with the colors in the structure.

The quantifier allows us to express this property, regardless of how many nodes the graph may have. Note that if we knew up-front which nodes there are in the graph, we could express the same property by a big "and"-statement. For instance, for a graph of four nodes:

We can think of a universal quantifier as a convenient shorthand for such a long "and"-statement, with the added important bonus that we do not actually need to know up-front how many components the "and"-statement will need.

The universal quantifier `!x in T: F` expresses that `F` holds for all values `x` of type `T`. There is also an existential quantifier `?x in T: F`, which expresses that `F` holds for at least one value `x` of type `T`. Again, this existential quantifier is strictly speaking redundant, because `F` holds for at least one value if and only if it is not the case that its negation `~F` holds for all values. In other words, `?x in T: F` is identical to `~!x in T: ~F`.

Exercise

Add a formula to the theory saying that there must be at least one blue and at least one green node.

The quantifier allows us to express this property, regardless of how many nodes the graph may have.

What makes quantifiers truly powerful is that they can be nested: in a formula such as `!x in T: F` or `?x in T: F`, the formula `F` can itself again contain quantifiers. For instance, the following formula expresses that for each color, there is at least one node which has that particular colour:

`!c in Colour: ?n in Node: colourOf(n) = c.`

In other words, this formula states that all colours are in fact used at least once.

Exercise

Earlier, we saw how we could express that each node in a graph is red. Add a formula to express that all nodes in the graph must have one particular colour (but this colour no longer must be red).

Earlier, we saw that we can think of a universal quantifier as a convenient shorthand for a long "and"-statement. Similarly, we can think of an existential quantifier as a shorthand for a long "or"-statement:

`(!n in Node: colourOf(n) = red) | (!n in Node: colourOf(n) = green) | (!n in Node: colourOf(n) = blue)`

Again, the additional benefit of using the existential quantifier is that the size of the formula does not depend on how many values there are in the type Colour.