Course:CPSC522/Higher Order Logic

Higher Order Logic

This document serves as an introduction to higher order logic - focusing on some theoretical results, comparisons with first order logic, and a brief mention regarding some of its applications to artificial intelligence.

Principal Author: Carl Kwan

Abstract

First order logic has fostered an impressive breadth of applications in the field of artificial intelligence. Indeed, one would be hard-pressed to find areas of computer science in general that has not been influenced by first order logic.

However, the expressiveness of sentences one can form in first order logic is ultimately limited due to its lack of quantification over (most notably) functions. Second order logic amends the lack of such expressions by including exactly them. Higher order logic, then, extends this idea.

In this article, we introduce second and higher order logic (focusing on primarily syntactical perspectives), some of its theoretical advantages and limitations, and its place in applications such as automated deduction and natural language processing.

Builds on

Readers familiar with first order logic (also known as predicate calculus) should be comfortable with the contents of this article. Some mathematical maturity is desirable but not imperative as proofs will not be emphasized.

Related Pages

The foundational nature of logic means that most of computer science is related via a mathematical pseudo-trickle-down effect. Nonetheless, we note some interesting connections in this course wiki.

The NARS project uses higher order logic to simulate human-level reasoning (with limited success).

The definition of a measure quantifies over sets of spaces (which are themselves sets) which require higher order logic in order to state.

Natural language processing uses higher order logic in a manner we discuss in this article.

Content

Motivation

Consider this simple sentence in first order logic:

$\lnot a\lor a$

In this case, $a$ is a constant (either “true” or “false”). However, there may come a time when we wish to apply the same sentence to an individual under statements that map to a “true” or “false”. So we introduce Boolean functions which we call predicates:

$\lnot P(a)\lor P(a)$

Now our universe of discourse may include individuals other than Booleans. This allows for greater expressivity. Suppose now we wish to express the same sentence for many individuals in which case we introduce quantifiers over variables that vary through individuals:

$\exists a,\lnot P(a)\lor P(a)$

Like with the individuals, it may be desirable apply the same sentence to different predicates. The natural progression is to quantify over the predicates:

$\exists P,\exists a,\lnot P(a)\lor P(a)$

Unfortunately, first order logic does not permit quantification over predicates. In fact, quantification over sets in general are not permitted (recall that functions are sets). Second order logic remedies such issues by permitting exactly quantification over sets. However, there is no need to stop at merely sets of individuals.

Here is a common intuitive approach to higher order logic:

• First order logic = quantifies over individuals
• Second order logic = first order + quantification over sets
• Third order logic = second order + quantification over sets of sets
• Fourth order logic = third order + quantification over sets of sets of sets

and so on.

However, it is usually better to think of higher order logic as quantification over predicates and relations or, in greater generality, over types due to the inconsistency of naïve set theory.

Basic Definitions

It would be prudent to recall the definition of a formula (sometimes called a well-formed formula) in first order logic:

• Atomic formulas (ie. expressions of the form $f(x_{1},...,x_{n})$ where $f$ is an $n$-ary function or relation) are formulas
• If $u$ is a formula, then $\lnot u$ is a formula
• If $u$, $v$ are formulas, then $u\lor v$ is a formula
• If $u$ is a formula, then $\exists u$ is a formula

Note that in the above, we may equivalently replace $\lor$ or $\exists$ with $\longrightarrow$ or $\forall$, respectively.

Atomic formulas in second order logic are those in first order logic but with the inclusion of new types of variables:

• There is a new type of variables that range over sets of individual variables.
• There is a new type of variable that range over all $n$-ary relations on individual variables.
• There is a new type of variable that range over all $n$-ary functions on individual variables.

Then, if $A$ is any of the above type of variables and $(t_{n})$ a sequence of terms of appropriate length, $\exists A(t_{n})$ is an atomic formula in second order logic (and the construction of other formulas in general follows as before). The extension to higher ($>2$) order logic follows by recursively introducing more types of variables that range over the types of variables in lower order logics.

A set of first (resp. second, $n$-th) order formulas is known as a first (resp. second, $n$-th) order theory. We call a structure $S$ a model of a theory $\Gamma$ if every formula in $\Gamma$ is true in $S$. A collection of structures is first (resp. second, $n$-th) order definable if it consists exactly of models a first (resp. second, $n$-th) order theory. An observant reader might notice that a first order theory is also a second order theory, and a third order theory, and a fourth, etc.

Examples

Before we continue with some important theorems, let’s take a look at some common sentences in higher order logic. A simple way to construct higher order formulas is to make a statement quantifying over functions. For example, consider the fact that no set has a bijection with its power set.

$\lnot \exists S,\exists f,S{\overset {f}{\longleftrightarrow }}{\mathcal {P}}(S)$

This is a second order formula. If one is concerned with the inclusion of the bijection symbol, an equivalent statement would be no set has the same cardinality as its power set.

$\lnot \exists S,|S|=|{\mathcal {P}}(S)|$

To make a third order formula, we simply make a sentence about a set of sets. The axiom that sets of a topology are closed under countable unions is a good example.

$\forall \tau ,\forall \{U_{i}\}\subset \tau ,\bigcup _{i}U_{i}\in \tau$

Here, $\tau$ varies over topologies and $U_{i}$ are members of $\tau$ known as open sets.

Fundamental Results

Expressive Power of Higher Order Logic

The expressive power of second (and higher) order logic can be exemplified in a couple of key theorems. We first make a statement on the “size” of the structures definable in second order logic.

The class of all finite structures is not first order definable. It is, however, second order definable by a single sentence.

The proof of the former statement follows from a simple application of the compactness theorem and a contradiction but will be omitted for the sake of brevity. The proof of the latter is also simple but a lot less verbose: the second order sentence

$\forall \varphi ,{\text{Injective}}(\varphi )\rightarrow {\text{Surjective}}(\varphi )$

where $\varphi$ varies over injective endomorphisms (ie. a morphism with identical domain and codomain) exactly characterizes finite structures. (For a more intuitive proof of a weaker but similar claim, just replace the words "structures" and "(endo)morphism" with "sets" and "function", respectively.) ∎

A pragmatist might remark that a hot air balloon, while much larger than a conventional one, is nonetheless filled with nothing but hot air. Likewise, we have yet to see how higher order logic aids computability. Indeed, let’s take a look at some positive implications of greater expressiveness. In particular, there are some questions that can be posed in second order logic but not in first order.

The notion of mathematical induction has no first order theory of countable size that describes its behaviour appropriately. On the other hand, there is such a second order sentence.

We purposely let "appropriately" remain ambiguous since a rigourous definition is beyond the scope of the article. Thus we only provide a sketch of the latter part of the theorem: recall that a successor function $S$ on the naturals is simply defined to be

$S(n)=n+1.$

In the context of defining the naturals, however, we view $S(n)$ as a formal object and say

if $n$ is a natural, then so is $S(n)$.

As a sentence in logic, this becomes

$\forall n,n\in \mathbb {N} \rightarrow S(n)\in \mathbb {N} .$

The structure of the above sentence should be familiar to the reader. Indeed, it is a disguised inductive definition. Using the notion of a successor function, the Principle (or Axiom) of mathematical induction is simply

$\forall \varphi ,\forall n\in \mathbb {N} ,[\varphi (0)\land \forall m\in \mathbb {N} ,\varphi (m)\rightarrow \varphi (S(m))]\rightarrow \varphi (n)$

where $\varphi$ varies over unary predicates. This is already sufficient to prove our claim. However, if one formalizes the naturals as sets themselves instead of via the Peano axioms, then $n$ is also a second order variable. ∎

Less fundamentally, but more imminent to the realm of artificial intelligence, we have statements regarding data structures such as graphs.

The collection of directed graphs with a path from the source to the target is second order definable in a single sentence but not at all first order definable.

The proof of this, although omitted, is similar to the others in this article. Posing sentences about, say, decision networks then becomes an exercise in second (or higher) order logic.

Limitations of Higher Order Logic

Considering the expressivenes of higher order logic relative to first order, the induced question, then, is “Why not use higher order logic all the time?” Unfortunately, there are some undesirable limitations in the behaviour of higher order logic. We highlight a couple of them here.

One issue, particularly relevant to artificial intelligence, is that the unification problem (ie. the algorithmic process of solving equations between symbolic expressions) is undecidable for higher order terms. For first order logic, however, it is. This has implications in automated reasoning, SMT solving, and logic programming as many advancement in those areas depend on the decidability of unification.

Another computationally relevant characteristic is that second order formulas are not recognizable by computations with a finite number of alternations between nondeterministic and co-nondeterministic guesses. This is Fraïssé's theorem.

Applications

For reasons highlighted above, first order logic finds successful application via the unification problem in many areas including automated reasoning, logic programming, SMT solving, and term rewriting which unfortunately does not extend fluidly to higher order logic.

However, despite such hard theoretical bounds, there has been work towards unification for higher order theories. Although not decidable, progress on this front has resulted in breakthroughs for the ellipsis problem in computational linguistics. The ellipsis problem, superficially stated, is the problem of recovering the original element for which an ambiguous substitute has replaced in a phrase with parallel structure. Take, for example, the English sentence

"Katherine likes math and Cedric does too."

Here, “Katherine likes math” parallels “Cedric does too.” However, it is not explicitly stated that “Cedric likes math” despite this being the taken meaning. The ellipsis problem deals with recovering such information and is reduced to exactly a unification problem for higher order logic.

Moreover, there are immediate applications of higher order logic to natural language processing in general as our semantical understanding of certain sentences instinctively follows higher order structures. For example, the sentence

“There are some critics who admire each other.”

quantifies over sets of critics. There are, however, methods of reducing such statements to first order logic but this comes at the expense of intuition.

The formalization of higher order logic via types leads to an alternative foundation for mathematics in which theorems are more susceptible to certification by way of computational methods. This has introduced significant advances in the areas of automated deduction and formal verification. The existence of automated and interactive theorem provers are very real evidence of this as some of the most successful (in both industrial and academic settings) systems, such as Isabelle and Coq, use type theory as an important method for encoding proofs.

Annotated Bibliography

• Boolos, G. (1984). To Be is to be a Value of a Variable (or to be Some Values of Some Variables). The Journal of Philosophy, 81(8), 430-449. doi:10.2307/2026308

• D. Leivant. Higher order logic. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pages 229–321. Oxford Science Publications, 1994.

• Enderton, Herbert B., "Second-order and Higher-order Logic", The Stanford Encyclopedia of Philosophy (Fall 2015 Edition), Edward N. Zalta (ed.).

• Erich Grädel , P. G. Kolaitis , L. Libkin , M. Marx , J. Spencer , Moshe Y. Vardi , Y. Venema , Scott Weinstein, Finite Model Theory and Its Applications (Texts in Theoretical Computer Science. An EATCS Series), Springer-Verlag New York, Inc., Secaucus, NJ, 2005. ISBN 978-3-540-00428-8

• Franz Baader and Wayne Snyder (2001). "Unification Theory". In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers.

• Mary Dalrymple, Stuart M. Shieber, and Fernando C. N. Pereira. Ellipsis and higher-order unification. Linguistics and Philosophy 14:399-452, 1991.

• McCarthy, J. (1988). Mathematical Logic in Artificial Intelligence. Daedalus, 117(1), 297-311.

• Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.

• Shapiro, Stewart (1991). Foundations Without Foundationalism: A Case for Second-Order Logic. Oxford University Press. ISBN 9780198533917

• Shoenfield, Joseph R. (2001) [1967]. Mathematical Logic (2nd ed.). A K Peters. ISBN 978-1-56881-135-2.

• Van Benthem J., Doets K. (1983) Higher-Order Logic. In Gabbay D., Guenthner F. (eds) Handbook of Philosophical Logic. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), vol 164. Springer, Dordrecht. ISBN 978-90-481-5717-4

To Add

Bibliography (done) Hyperlinks (done) Related pages (done) Compactness(?) Fourth Order Sentences(?) Pictures(?)