Reasoning: An Introduction to Logic, Sets, and Functions

Subsection 7.6.4 Higher Order Logic

The logical framework that we have been describing is called first-order because it allows quantification over variables (and thus the objects to which they refer) but not over predicates or functions. So, for example:

• We can say: ∀x (Bear(x) → Mammal(x))

We’ve quantified over the objects of which Bear or Mammal might be true.

• We cannot say: ∀P (∀x ((LivingProp(P(x)) ∧ Dead(x)) → ¬P(x)))

What we’re trying to do here is to quantify over predicates to say that if P is any predicate that describes a property of living things, then it ceases to be true if the thing in question becomes dead. In a first-order system, we can’t do this.

Here’s an example of how we could exploit quantification over predicates if only it were allowed:

We’ll let LivingProp be true of any predicate that is true only of living things. Then we can assert:

[1] LivingProp(Breathing(x)) Breathing is a property of living things.

[2] LivingProp(NeedsWater(x)) Needing water is a property of living things.

[3] LivingProp(CellsDivide(x)) Cells dividing is a property of living things.

[4] LivingProp(CanSing(x)) Can sing is a property of living things.

[5] P (x ((LivingProp(P(x))  Dead(x))  P(x))) Properties that hold of living things become false when something dies.

s

[6] Dead(Elvis)

Now we’d like to be able to conclude:

[7] Breathing(Elvis)

[8] NeedsWater(Elvis)

[9] CellsDivide(Elvis)

[10] CanSing(Elvis) This is the one that makes many people sad.

A system that allows quantification over predicates is called second-order. Even higher order logics exist. In them, it’s possible to quantify over properties of properties, and so forth.

The reason that we don’t allow these sorts of quantification in the formal system that we’re defining is that, if we do, both the computational and the formal logical properties of the resulting system would make using it very difficult.

This means that, to get the same effect, we must say what we have to say separately for each predicate.

Continuing with our example, we’d need to replace [5] with this set of premises:

[5a] \(\forall\)x (Dead(x)) \(\rightarrow\) \(\neg\)Breathing(x))

[5b] \(\forall\)x (Dead(x)) \(\rightarrow\) \(\neg\)NeedsWater(x))

[5c] \(\forall\)x (Dead(x)) \(\rightarrow\) \(\neg\)CellsDivide(x))

[5d] \(\forall\)x (Dead(x)) \(\rightarrow\) \(\neg\)CanSing(x))

Of course, when we reason informally and don’t care about how computationally difficult it would be to create a formal proof automatically, we do use this sort of higher order reasoning quite often.