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

  • $\begingroup$ 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. $\endgroup$ – Asaf Karagila Sep 22 '15 at 14:56
  • 2
    $\begingroup$ Crossposted at MO (mathoverflow.net/questions/218956/…) - please don't do that. $\endgroup$ – Noah Schweber Sep 22 '15 at 15:02
  • 2
    $\begingroup$ Despite the crossposting, I think this is a fine question for this site. $\endgroup$ – Noah Schweber Sep 22 '15 at 15:24
  • $\begingroup$ @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. $\endgroup$ – Asaf Karagila Sep 22 '15 at 15:37
  • $\begingroup$ @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. $\endgroup$ – 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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Carl Mummert Sep 22 '15 at 17:49
  • $\begingroup$ Then the OP certainly needs to explain: What is a property, and why is it not a set? $\endgroup$ – GEdgar Sep 22 '15 at 18:32

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.