# How does “higher-order logic” differ from “normal” (first order?) predicate logic?

How does “higher-order logic” differ from “normal” predicate logic? I assume the latter is consistently called ”first order logic”. So where are the differences between these? What kinds of statements can be expressed or proven using higher-order logic but not using first-order logic? Intuitive (in the colloquial sense) examples would be very welcome.

This question started out as a proposed question for the proposed Logic SE which has now been declared a duplicate op Philosophy.

-

## 2 Answers

You can consult http://plato.stanford.edu/entries/logic-higher-order/ for explanations, examples, and further references.

-
It seems perverse to downvote a recommendation for an accessible, free-available, written-for-students, reasonably brief article by a much admired expositor! The OPs question isn't the sort of thing that can be illuminatingly answered in a couple of paragraphs here. – Peter Smith Jan 24 '13 at 12:46
It does, which I voted it up. :). – Mozibur Ullah Jan 24 '13 at 13:32

You have Godels completeness theorem in first order classical logic which isn't available in higher order logics. This theorem establishes an equivalence between syntactic or formal truth with semantic truth. Formal truth is what can be proved by your logic by manipulating logical sentences according to your deductive system, semantic truth is established in a model of your logic, in fact one says a sentence is semantically true if its true in every model of your logic.

Lindstroms theorem shows that first order logic is characterised amongst logics as the strongest one satisfying certain natural (at least in mathematical logic) properties.

Moving out of classical logic, topos theory establishes a link between abstract set theory, higher-order intuitionistic logic & geometry. It's currently an area of intensive investigation. One can move on - there is also higher order topos theory where the logic becomes homotopy type theory, this models dependent types specifically the intensional flavour developed by Martin-Lof. This is already being used in computer science as the basis for theorem-provers, such as Coq. Here types are not modelled by interpreting them as sets but as homotopy types of topological spaces.

On a related point, although the synthesis of logic, set theory & geometry appears exciting and wholly novel, philosophically speaking it's already apparent in high school mathematics: propositional logic, set theory, and venn-diagrams. Its simply the sophistication is several magnitudes higher and much more tightly woven, but from an objective point of view, that is outside of mathematics proper, this additional sophistication isn't relevant.

Edit:

Each topos has an associated internal language, this is intuitionistic rather than classical (so the law of the excluded middle doesn't hold), and higher-order. This holds because each topos is a heyting category, which means that its poset of subobjects for any object is a heyting algebra. (Note while classical propositional logic is modelled algebraically as a boolean algebra, intuitionistic propositional logic is modelled by a Heyting algebra). Its higher order because each topos has exponentiation, and this translates via its internal language that predicates of predicates (and so on) are available.

-
I'm a bit unclear how your answer and the mention of topos theory in general corresponds to my question about higher order logic. I haven't followed all the links yet, but I would welcome an edit that makes this more explicit. Or are you trating first and higher order topos theory as an example for first an higher prderorder (predicate?) logics? – MvG Jan 24 '13 at 22:23
I've added an edit. Yes, thats correct. But note that the logic is NOT classical, its intuitionistic. One can make the logic classical by demanding that the topos is boolean. – Mozibur Ullah Jan 24 '13 at 23:44