Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
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.
You can consult http://plato.stanford.edu/entries/logic-higher-order/ for explanations, examples, and further references.
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.
