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\[ T \vdash p \]
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\[ T \vDash p \]
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\[ \forall x . p(x) \]
that is, p is true of all x. Similarly\[ \exists x . p(x) \]
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.