This is a question about terminology, as I am clearly confused on the topic.

The Wikipedia page on higher-order logic defines it as follows:

Higher-order logic is the union of first-, second-, third-, …, nth-order logic; i.e., higher-order logic admits quantification over sets that are nested arbitrarily deeply.

So this is worded vaguely. Taken at face value, it says that higher-order logic is the union of all logics up to some arbitrary $n$. This would imply that higher-order logic is not one thing, but that for each $n$ there is a higher-order logic, so that higher-order logic is sort of just a catch-all term for logic of some order > 2, or what have you.

But then it says that higher-order logic admits quantification over arbitrary-order predicates, which one could interpret as being the union of first-, second-, third-, ... order logic without stopping at any $n$, meaning quantifiers of all orders are included. However, this does not imply that there are "infinite-order" predicates that can simultaneously quantify over all finite-order predicates, just that you can have arbitrarily large finite-order predicates.

Then on this Stanford page, it says under "Higher-Order Logic" that $\omega$-order logic is "type theory," with continuation into the transfinite being conceivable.

Is the correct idea that higher-order logic has all quantifiers of finite order, each of which quantifiers over all predicates up to a certain order type, whereas type theory has infinite-order quantifiers enabling you to quantify over all finite-order predicates?

  • $\begingroup$ This paper (sciencedirect.com/science/article/pii/S157086830700081X) describing type theory also calls it higher-order logic. Every variable in it belongs to a definite order, so quantifiers only quantify over predicates of a certain order, not the union of predicates of different orders. $\endgroup$ – Matt Dickau Oct 13 '17 at 19:07
  • $\begingroup$ I guess this is "simple" type theory, which they distinguish from Russell's ramified type theory. It seems to be different from the way I see type theory described elsewhere. $\endgroup$ – Mike Battaglia Oct 13 '17 at 19:34
  • 1
    $\begingroup$ There is nothing vague about the Wikipedia definition apart from the fact that (in context) the article is defining the language of higher-order logic to be the union of the languages of $n$-th order logic for all $n$. What's wrong with that? $\endgroup$ – Rob Arthan Oct 13 '17 at 20:39
  • 1
    $\begingroup$ If you are just complaining about the wording of the Wikipedia article, you should take that up on Wikipedia. You are also reading too much into the Standard article, the $\omega$-order logic discussed there is exactly the same as what the Wikipedia article means (but doesn't quite describe correctly), i.e., the union $\bigcup_{n \in \omega} \cal L_n$ where $\cal L_n$ is the language of $n$-th order logic. This doesn't allow a single quantifier to range over predicates of all orders. As the Stanford article says, there are conceivable extensions, but that's not what they are talking about. $\endgroup$ – Rob Arthan Oct 13 '17 at 20:48
  • 1
    $\begingroup$ I am just trying to help you make sense of the two references you mention. Church's simple type theory and higher-order logic (in the sense of the Wikipedia article) are equivalent and both can be viewed as the union of a family of finite-order logics. But there are many other type theories and many generalisations of higher-order logic. So your question as phrased ("is the correct idea that ...?") isn't really answerable in general. It can only be answered in the context of a specific system. $\endgroup$ – Rob Arthan Oct 13 '17 at 21:58

While they don't own the term, the HOL family of mechanized proof assistants (HOL4, HOL Light, Isabelle/HOL) is highly successful and influential. These are all implementations of (extensions of) simple type theory as described by this paper referenced on the HOL4 site. The most significant extension that applies to all of them is that they use a polymorphic typed lambda calculus and not purely a simply typed lambda calculus.

While "type theory" nowadays usually means systems based on typed lambda calculi or the study thereof, to the extent that it is being contrasted to HOL, it is likely to mean specifically dependently typed lambda calculi. Even more specifically, it often means a descendant of Intuitionistic or Martin-Löf Type Theory (ITT). Again, there are highly successful and influential implementations of these, most notably Coq and the LF-family including Twelf. Dependently typed lambda calculi generalize simply typed lambda calculi (and in practice, often generalize polymorphic lambda calculi as well), so something like HOL is, roughly speaking, a sub-language of ITT. However, these systems are used in dramatically different ways. In HOL, a proposition is literally a Boolean expression and the goal is to show that it is the true Boolean. In ITT, a propositions-as-types perspective is typically taken so that a proposition is modeled as a type and the goal is to produce a value of that type.

People usually don't mean Russell's theory of types unless they are talking about the early history of formal logic. "Higher order logic" could possibly also be used simply as a contrast to first-order logic, i.e. as "not-first-order logic" and in that sense second-order logic would be a "higher order logic", but people rarely talk about third- or fourth-order logic, so they'd be likely to specifically refer to second-order logic where most of the good and bad things that come with moving beyond first-order logic have already occurred.

  • 2
    $\begingroup$ Thanks - I think the problem is that there are so many different type theories that I'm having trouble keeping them all straight. Let's consider the simply typed lambda calculus, which I think is what people have called "simple type theory," which I think means not dependently typed. Is the idea that HOL is equivalent to this simple STT, and the dependent types extend it? If so, how do I convert between HOL and STT? $\endgroup$ – Mike Battaglia Oct 20 '17 at 21:24
  • $\begingroup$ To clarify, by HOL, I just mean the system that I was talking about with Rob Arthan in my original comments, not the proof system mentioned above. $\endgroup$ – Mike Battaglia Oct 20 '17 at 21:26
  • $\begingroup$ The Seven Virtues of Simple Type Theory which I linked above describes the embedding of $n$th-order logics into STT and states (but does not further prove) a theorem that the embeddings are faithful. Furthermore, the embedding does not rely on definite description for the "usual" connectives. Ignoring definite description (or targeting a logic with it), the only tricky part about going the other way is handling abstraction of functions which we can either encode as functional relations or disallow with a minor tweak. $\endgroup$ – Derek Elkins left SE Oct 20 '17 at 23:13
  • 1
    $\begingroup$ As a field, the situation for type theory is similar to the situation for logic. (I don't even consider them separate fields.) Most type theories have a corresponding logic and vice versa. If you find the landscape of type theory confusing you should also find the landscape of logic confusing. If you don't, it's only due to the excessive focus on classical first-order logic. A small but important part of the type theory landscape is described by the lambda cube. This illustrates the relationships between STT, dependent type theory and CoC. $\endgroup$ – Derek Elkins left SE Oct 20 '17 at 23:13
  • 1
    $\begingroup$ That much I understand, but why define $\mathsf{T}$ like that? Why not just define $\mathsf{T}$ as the primitive boolean value true directly, expressed as a primitive constant element of $\ast$? $\endgroup$ – Mike Battaglia Oct 22 '17 at 21:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.