17
$\begingroup$

I know this seems like an obvious question, but I haven't been able to find any examples of sentences in logic higher than second order, so my intuition on how it's supposed to behave is failing me. There are descriptions describing third order logic as 'properties of properties' but without example syntax, I'm not sure if I'm on the wrong track or not.

Propositional logic sentences are simple propositions connected by logical connectives:

$\phi$ $\land$ $\psi$

$\phi \lor \psi$

$\lnot \phi \rightarrow \psi$

First order logic sentences are quantified objects with free predicates and functions:

$\exists$x $\forall$y P(f(x)) $\rightarrow$ Q(y)

Second order logic sentences don't just quantify the objects, but the functions and predicates:

$\forall$Q $\exists$P $\exists$f $\exists$x $\forall$y P(f(x)) $\rightarrow$ Q(y)

How do we go higher than second order? What are some examples of third, fourth, or fifth order logic sentences?

$\endgroup$
2
  • $\begingroup$ Maybe we take a a family of predicates? $\exists \mathcal Q\forall Q\in \mathcal Q\exists P\notin \mathcal Q \exists f\exists y: P(f(x))\to Q(f(x))$. $\endgroup$ – TZakrevskiy Dec 4 '14 at 22:27
  • 2
    $\begingroup$ It may help you to think about simple type theory, which treats functions and predicates as the same kind of thing and associates a type with every object which governs how that object can be used. See en.wikipedia.org/wiki/Type_theory or plato.stanford.edu/entries/type-theory for more information. $\endgroup$ – Rob Arthan Dec 5 '14 at 15:02
17
$\begingroup$

The axioms of topology, for example, can be seen as third-order axioms. Simply because of the axiom that a topology is closed under unions:

$$\forall\mathcal U((\forall U\in\mathcal U\rightarrow U\in\tau)\rightarrow(\exists V\forall x(x\in V\leftrightarrow\exists U\in\mathcal U(x\in U))\land V\in\tau))$$

In the language of arithmetic, a well-order of the second-order predicates (namely, $\mathcal P(\Bbb N)$), or even the existence thereof, is a third-order sentence coming from the numbers themselves.

To some extent this is the great thing about set theory here. It allows us to take any of these high-order sentences and make them first-order in the language of sets. Of course we can make them into first-order in a two/three/four-sorted logic, which acts a bit like type theory, but you do run into issues there (for example, the characterization of $\Bbb R$ as the unique complete ordered field won't translate well into first-order logic).

$\endgroup$
8
  • 1
    $\begingroup$ This sort of helps, but I'm still a bit confused here. This looks syntactically like first order logic with one first order predicate, membership. Are the U's the union function then? I understand there are semantic higher order logics that are 'set-theory in sheeps clothing' but I don't quite understand how they relate to syntax of higher order logic where you quantify predicates and functions. $\endgroup$ – dezakin Dec 4 '14 at 23:26
  • $\begingroup$ Second-order means "Every set ..." and third-order means "Every set of sets". Yes, this is all just first-order in set theory, because set theory is concerned with sets to begin with. This is why we use set theory as a foundational theory to begin with. But from the standpoint of a model of some arbitrary language, first-order means statement on its elements, second-order means statement on its subsets (and relations), third-order means statements on its sets of subsets and so on. $\endgroup$ – Asaf Karagila♦ Dec 4 '14 at 23:32
  • 1
    $\begingroup$ Does that translate to quantification over predicates and functions? "Every set.." becomes "Every function..." and "Every predicate"? I'm having trouble relating the syntax of p-adic second order logic quantifying over functions and predicates to quantifying over sets. Sorry if it seems I'm being obtuse, just trying to bang my brain into a new shape, and this is a bit confusing. $\endgroup$ – dezakin Dec 4 '14 at 23:39
  • $\begingroup$ I'm not sure that I understand your comment about $p$-adic second order logic. $\endgroup$ – Asaf Karagila♦ Dec 5 '14 at 8:14
  • 1
    $\begingroup$ @Shin Kim: Sure. I was trying to capture all orders of variables in the statement. You can even simplify it to $\forall\mathbb O(\mathbb O\subseteq\tau\implies\bigcup\mathbb O\in\tau)$. $\endgroup$ – Asaf Karagila♦ Mar 29 '16 at 6:43
13
$\begingroup$

In the context of higher-order arithmetic, there are many natural third-order statements. In arithmetic, quantifiers over natural numbers are first-order, quantifiers over sets of natural numbers are second-order, and quantification over sets of sets of natural numbers is third-order.

Using standard coding methods, quantifying over real numbers is second-order, so quantifying over sets of real numbers is third-order.

Some English sentences that are expressed as third-order statements in the language of arithmetic, but not as second-order statements, include:

  • There is an nonprincipal ultrafilter on $\mathbb{N}$.

  • Every subset of the unit interval $[0,1]$ has a cluster point.

  • There is a discontinuous function from $\mathbb{R}$ to $\mathbb{R}$.

Similarly, one can obtain fourth-order statements by quantifying over arbitrary subsets of $\mathbb{R}$.

$\endgroup$
4
  • $\begingroup$ To that last line the statement "$\tau$ is a topology on $\Bbb R$" is a fourth-order statement from the standpoint of arithmetic. And here lies the crux of the issue, we often replace the higher-order statement by moving to a more natural language. For example, it would be strange to talk about topologies on $\Bbb R$ from the standpoint of arithmetic, since the elements of the space are subsets of $\Bbb N$; but instead if we talk about topologies over the universe $\Bbb R$ this is a third-order ordeal now. $\endgroup$ – Asaf Karagila♦ Dec 4 '14 at 23:17
  • $\begingroup$ How about some third or fourth order logic statement that is model agnostic in prenex normal form without any predefined predicate like 'membership.' What do these statements look like, the syntax I mean? $\endgroup$ – dezakin Dec 5 '14 at 0:09
  • 4
    $\begingroup$ @dezakin: When you write $x\in A$ it is just a short for $A(x)$. When you write $A\in\mathcal A$ this is a short for $\mathcal A(A)$. $\endgroup$ – Asaf Karagila♦ Dec 5 '14 at 8:13
  • $\begingroup$ @dezakin: the membership symbol $\in$ is one of the logical symbols in higher order logic, analogous to the way that $=$ is often treated as a logical symbol in first-order logic. $\endgroup$ – Carl Mummert Mar 25 '16 at 18:58

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.