# What does it mean for a language to have "order"?

In calculus, a polynomial has order $n$ if it contains terms that raise the unknown to a power $n$.

I'm trying to figure out how this definition of "order" relates to the use of the same word when talking about formal languages.

We say a logic or language is "first order", "second order", or "higher order". I know it is related to what kinds of states of expressible within that language,b ut what does this mean, fundamentally, and why is it called the "order" of the language?

• This question is a little unclear. Are you asking what it means for a language to be "higher-order"? Or are you asking a more philosophical question about "why" we use 'order' to describe this property? Jan 15 '11 at 3:32
• This site is for research-level questions in theoretical computer science, that are likely to have short well-defined answers. "Research-level" means, roughly, questions that might be discussed between two professors, or between graduate students working on Ph.D.'s, but not usually between a professor and the typical undergraduate student. It does not include questions at the level of difficulty of undergraduate homework. You may want to try Math.SE. Voting to close as off-topic. Jan 15 '11 at 6:10
• Wikipedia's disambiguation pages have helped me understand an unknown term, either due to different translations or my own lack of knowledge : en.wikipedia.org/wiki/Order_%28mathematics%29 Jan 15 '11 at 22:20
• I agree with @Kaveh, and voted to close. The answer is in the Wikipedia link provided by sclv. Jun 23 '11 at 0:54

My angle on a related distinction: http://chrisamaphone.livejournal.com/751991.html

The "order" of nth-order (including higher-order) logic refers to the level of things that can be quantified over. In first-order logic, the things quantified over are terms of some unrelated domain: "All men are mortal." In second order logic, you can quantify over first-order predicates: "All properties of men also hold of dragons." Higher-order logic is the generalization of this to all higher predicates, which I think is better understood in terms of system F-omega (equivalent to HOL), wherein you can form type operators (constructors of kind type -> type) which can be quantified over as well as types.

The relation to "order" in polynomials is better understood as an analogy pertaining to recursion (nth order polynomials include a term multiplied by itself n times) than anything more rigorous.

A lazy answer from me, but wikipedia explains this perfectly well: http://en.wikipedia.org/wiki/Higher-order_logic

In logic, the order is roughly the number of collections over which you can use quantification.

For example, the first-order logic suppose that you have a lone "container" of elements, called Universe, over which you can quantified universally (for all or $\forall$) or existentially (there exists or $\exists$). The set theory ZF use only one order of quantification : all elements in the Universe are set. You cannot speak about another "type" of element. This is why you must use schemas to provide a "set" (in the usual meaning) of axioms. The axiom schema of restricted comprehension is one of them : $$\forall y \exists z \forall x (x\in z \Leftrightarrow (x\in y \wedge \phi(x))$$ for all well-formed formulae $\phi$. Here, you can see that we do not write $$\forall\phi\forall y \exists z \forall x (x\in z \Leftrightarrow (x\in y \wedge\phi(x))$$ You can wonder why we use the literate formulation "for all well-formed formulae $\phi$" instead. This is because, quantifiers $\forall$ and $\exists$ only apply to set. There is no quantifier that can be apply on formulae.

If we really want them, we have to provide some new quantifiers that can be applied on another "collection" of elements; namely the well-formed formulae. These quantifier will be named "second-order quantifiers" and the language needed to express the new formulae will be referred as a second-order language. It is needed to be able to distinguish both order of quantification and the usage is to write the new operators with $\forall^2$ and $\exists^2$. Considering this, the second-order formula over sets and well-written first-order formulae would have been written as $$\forall^2\phi\forall y \exists z \forall x (x\in z \Leftrightarrow (x\in y \wedge\phi(x))$$

There is some problems that can spawned from using quantifier over formulae (circular definitions for examepl) this is why it is not achieve this way, and why the literate formulation is preferred.

However, there exist other examples of second-order language. To keep logic examples, we can talk about von Neumann–Bernays–Gödel set theory that uses quantifications over set and proper classes, or Computation Tree Logic (CTL) that uses quantification over paths and states.

Hope this is helping you.