# Higher-Order Logic in ordinary Mathematics?

Do we use the language of higher-order logic in ordinary mathematics? (If yes: Can you give some examples?) Or are we always working with first-order logic?

Comment: Maybe you are going to say that the definition of a topological space is higher-order because we quantify over sets of sets of ... individuals. But that is not what I mean with "using higher-order logic". The example "definition of topological space" can be expressed in set theory which is a first-order theory. Thus with "using higher-order logic" I do not mean quantification over sets, which is a first-order concept, but I mean "quantification over properties".

• If it can be formalized, then set theory can translate this into a first-order statement in the language of set theory. Simply because we can formalize high-order logic inside set theory. – Asaf Karagila Sep 22 '15 at 14:56
• Crossposted at MO (mathoverflow.net/questions/218956/…) - please don't do that. – Noah Schweber Sep 22 '15 at 15:02
• Despite the crossposting, I think this is a fine question for this site. – Noah Schweber Sep 22 '15 at 15:24
• @Noah: Even if your answer you point out that it's not entirely clear what will satisfy the OP. That is the definition of "unclear". I agree it can be made into a reasonable question. But it's not entirely clear what that question is, and if that is in fact the question the OP wants to ask. – Asaf Karagila Sep 22 '15 at 15:37
• @AsafKaragila This is true, but I give more leeway to such questions in logic, since it often takes quite a lot of work to figure out what one means oneself. Of course, this is a subjective take, and the question could definitely be improved. – Noah Schweber Sep 22 '15 at 15:39

I think it's unquestionably true that we use the language of higher-order logic all the time in mathematics - for instance, if I write a paper in algebra and prove something by induction, my proof by induction will be phrased as a second-order argument.

Now, your comment suggests you're really interested in times when we use the language of higher-order logic, and need to. The problem is, one of the things set theory (or class theory, or . . . ) is designed to do is let us reason about higher-order objects - properties - in a first-order way. For instance, a property of natural numbers is just a set of natural numbers, from the point of view of set theory. So I'm not sure what you would consider a satisfying example.

Note that higher-order logic (with the standard semantics - so, not just first-order logic in disguise) doesn't have a notion of proof - in particular, the set of validities of even second-order logic is not recursively enumerable (this is a huge, huge, HUGE understatement). So as soon as we're interested in formal(izable) mathematics, we can't be talking about genuine higher-order logic anymore.

In fact, first-order logic is basically the best available for reasoning about countable objects! This is (one of) Lindstrom's theorem(s): there is no logic strictly stronger than first-order logic with the Lowenheim-Skolem property (any consistent sentence has a countable model) and a recursive proof procedure.

Yes. Every set of real numbers has a least upper bound. That is a second-order statement (about the real numbers). (The fact that it is a first-order statement in some imaginary ZFC approximation of reality is irrelevant.)

Peano's original axiom system for the natural numbers had a second-order axiom. Every nonempty subset of $\mathbb N$ has a least element. Nowadays for use in model theory, they replace this with a first-order axiom scheme, using only subsets that can be defined within a certain system.

• The OP stated that he/she views quantification over sets as a first-order statement, so there is some gap between the question and this answer. – Carl Mummert Sep 22 '15 at 17:49
• Then the OP certainly needs to explain: What is a property, and why is it not a set? – GEdgar Sep 22 '15 at 18:32