# What is higher-order logic?

**24 Feb 2018, 05:19 • logic, semantics**

*Formal logics are axiomatic systems that formalise inference. Let’s look at what higher-order logic is and how it can be worked with.*

The simplest formal logic is propositional logic (also called sentential logic), which only uses propositional variables, i.e., with values true and false. A propositional theory is a set of formulae that can be used to model some rule-based knowledge. We say that a proposition *p* follows from a theory *T* if *p* can be shown to always be true in the presence of *T*. In symbols

A model of a theory is a valuation of all the variables occurring in it such that the theory is true. We then say that *p* is valid in *T* if it's true in all models of *T*. In symbols

It can be shown that in propositional logic \( T \vdash p \) iff \( T \vDash p \), which is a very strong result because it means the every consistent theory has a model.

Another useful logic is predicate logic, also called first-order logic (which would make propositional logic "zeroth-order"). FOL's stronger that propositional logic because it has individuals, predicates and functions. If *p* is a unary predicate, we can, for example, say that

that is, *p* is true of all *x*. Similarly

means that there's a *x* such that *p(x)*. FOL models are more complicated, they consist of a set of individuals (the domain, carrier, or universe) and n-ary relations on the universe that adequately model predicates and functions. As in the case of propositional logic, a formula provable from a theory is true in all models of that theory and vice versa so again consistent theories have models.

We now come to higher-order logics where we can have something like

\[ \forall P . P(x) \]for a predicate *P*. Such a logic is often less cumbersome if we want to model a complex knowledge domain. The important question is: If we have a consistent higher-order theory, does it have a model?

To answer this question we'll embed higher-order logic into Church's simple theory of types. In type theory we have formulae of concrete types. There are two atomic types, ι for individuals and ο for truth values. Whenever α and β are types, αβ is also a type, namely the type of functions from β to α (in computer science, αβ would be written as β→α).

Let's now have a consistent higher-order theory *T*. We'll create its type-theoretic model. For ο the domain are the constants \(\top\) and \(\bot\), i.e., true and false. For ι the domain is the set of equivalence classes of ι-expressions. So we have a valuation function Φ for ι and ο.

If α and β are types for which we already have a valuation function, we can extends Φ to include αβ. For every closed formula *A*_{αβ} we can define Φ(*A*_{αβ}) as the function that takes Φ(*B*_{β}) to Φ(*A*_{αβ}*B*_{β}). The corresponding domain for αβ is then the image of Φ for all closed formulae of type αβ. Such a so-called canonical model can be constructed for any consistent theory of any (finite) order.

We've seen that any consistent theory has a model. The proof is by constructing domains for closed formulae of compound types αβ. It's also noteworthy that canonical models of higher-order theories are countable.