Logical notation: ConnectivesMore Advanced Topics

So far the examples in this guide have used the notation of first order logic, with its standard connectives and quantifiers, to express the constraints on solutions to problems, but on a somewhat intuitive level. The time has now come to look into the matter in a more systematic way.

Consider a simple atomic fact like “Tom loves Mary”. This is conveniently expressed as an atomic formula, using a relation symbol and a couple of names:
Tom loves Mary.
or, if you feel that putting the relation symbol in prefix position looks “more logical”:
loves(Tom,Mary).
This (in either of its forms) will be parsed as a first order formula involving no connectives or quantifiers. The same is true of a slightly more complex sentence such as “Tom loves Henry’s sister”, in which “the_sister_of” is a function symbol:
Tom loves the_sister_of(Henry).
In similar vein, we can use the connectives AND and OR to express “Tom and Mary love each other”:
Tom loves Mary AND Mary loves Tom.
and “Mary loves either Tom or Michael”:
Mary loves Tom OR Mary loves Michael.
Note that we can’t get away with using OR to join the names
Mary loves (Tom OR Michael) %%% ?? ERROR!
because this is a type error: OR can only join boolean expressions such as sentences. Tom and Michael are men, not truth values, so joining their names with a connective is incorrect.

The connective IMP (short for “implies”) is used to state that a constraint holds not unconditionally but rather if some antecedent condition is met. For example, the formula
Tom loves Mary IMP happy(Mary).
requires that in any model Mary is happy if she is loved by Tom. If the condition fails—if Tom doesn’t love her any more—then the above formula imposes no constraint on Mary. More complicated conditional constraints are more of the same. For instance, we can stipulate that if Tom and Mary love each other then at least one of them is happy:
(Tom loves Mary AND Mary loves Tom) IMP (happy(Tom) OR happy(Mary)).

If you have studied formal logic, you will probably be familiar with symbols for connectives. Clicking on the symbols given just below the constraints box will cause them to appear in your text. The effect of this is merely abbreviation, as they mean exactly the same as the corresponding words.