Subsection 4.2.7 Infix Predicates
So far, we’ve written all our predicates using what we call prefix notation. In other words, we write the predicate first, followed by its arguments (in parentheses).
For example, we’ve written:
Bear(Smokey)
MotherOf(Gruffy, Smokey)
CurrentProjectOf(Shazaam, Chris)
Prefix notation is convenient when we are working with predicates with arbitrary names, and when some of our predicates (e.g, Bear) have just one argument, others (e.g, MotherOf) have two arguments, and some have three or more arguments.
But there’s a common special case in which an alternative notation may be more convenient. Infix notation allows us to write binary predicates (ones with exactly two arguments) by putting a predicate symbol in between the two arguments.
The expressions in the second column are infix versions of the ones in the first column:
EQ(x, y) x = y
NEQ(x, y) x y
GT(x, y) x > y
We can use predicates expressed in infix notation in our logical expressions in exactly the same way we’d use prefix ones. If there’s a possibility of confusion, we’ll enclose them in parentheses.
Exercises Exercises
1.
Assume the facts of integer arithmetic. Which of the following expressions isn’t true:
∀x (∀y ((x > y) → (x ≠ y)))
∀x (∀y (∀z (((x > y) ∧ (y > z)) → (x ≠ z))))
∀x (∀y (∀z (((x > y) ∧ (y > z)) → (x > z))))
∀x (∀y ((x ≥ y) → (x ≠ y)))
∀x (∀y (((x = y) ∧ (y ≠ z)) → (x ≠ z)))