Higher-Order Logic in ordinary Mathematics?

Question

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".

Answer 1

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.

Answer 2

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.