# On the limitations(?) of first-order logic in mathematical reasoning

Note: This is a follow-up to this earlier question. Also, for the purpose of this question, I'll use the term "normal mathematics" to refer to topics other than "foundational" ones like logic and set theory.

On the one hand, it seems like only a relatively small minority of "normal mathematics" is explicitly written out in (or "translated" to) a formal language like first-order logic (the rest is done "non-formally", so to speak).

On the other hand, there seems to be a prevalent view (either explicitly stated or strongly implied) that all of "normal mathematics" (not just "most", but all) is "first-orderizable". That is, that every result can be formally derived in (standard, finitary) first-order logic from some sufficiently strong system of first-order axioms (whether they be the axioms of $$\mathsf{ZFC}$$, or $$\mathsf{ZFC}$$ plus some other axioms like large cardinals, or some stronger set theory like Morse-Kelley, etc.)

But this seems like an awfully strong assumption, to assume that literally all the "non-formally" developed mathematics from all of human history (and the forseeable future) is "first-orderizable" in the sense just described in the preceding paragraph. Hence my questions:

1. Is this assumption of "first-orderizability" in fact a fairly prevalent view?
2. If so, what is the rationale for this belief? It seems like there are plausible reasons to doubt whether this is entirely true (see footnote below).

Footnote -- Possible Counterexamples of Non-First-Orderizability:

An infinitary logic such as $$L_{\omega_{1}^{CK},\omega}$$ seems like a totally valid formalization of logical reasoning. And (to my understanding) it has expressive capabilities that cannot be replicated by any theory formalized in (finitary) first-order logic. How sure can one really be that there doesn't exist any "non-formally" developed mathematics which is, say, formalizable in $$L_{\omega_{1}^{CK},\omega}$$ but not formalizable in (finitary) first-order logic? Indeed, this answer seems to provide a (possible) such counter-example:

Especially in the context of $$L_{\omega_{1}^{CK},\omega}$$ - the smallest "nice" fragment of infinitary logic which is stronger than first-order logic - Barwise compactness has been incredibly useful in proving results relevant to classical computability theory

Also, the answer by Daniil Kozhemiachenko to this Quora question suggests that much but not all of mathematics is "first-orderizable":

No...in the sense that you can express every mathematical statement as a sentence of a standardized first-order language, math is not based on FOL...However...the language of ZFC is enough to express almost every statement in math.

Finally, there are the bullet points below (although they may not be the most compelling counter-examples, in that the issues mentioned might actually be "first-orderizable" if one "upgrades" to a sufficiently stronger first-order theory):

• In volume II, chapter 4 of Logic, Language, and Meaning by van Benthem et. al., they write that "any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer struture than predicate logic", and they posit (if I understand correctly) the "$$\omega$$-th order" language of type theory as the tool for this task.
• This post re "non-first-orderizability" on Terence Tao's blog (latter part, starting with "it seems that one cannot express") discusses some challenges with expressing things in first-order logic.
• Using a form of natural deduction and some basic set theory (subsets and Cartesian products), I am able to prove a variation of The Barber Paradox: In a village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves if and only if that barber is not a man. It seems to me that it cannot be proven without set theory or some higher order logic. See my proof: dcproof.com/BP12.htm Commented May 9 at 2:10
• If it can be proven in a first-order set theory like ZFC, then it’s not quite in the category of “non-first-orderizability” that I had in mind.
– NikS
Commented May 9 at 3:33
• AFAIK there are no axioms in FOL that allow us to construct subsets and Cartesian products. You will need additional axioms for that. Commented May 9 at 3:41

I think the question you are asking is specifically relevant at the foundational level, where (simplifying things a little bit) we choose if our primitive formal objects are "sets", or "functions", etc., as well as the specific logic (language) to use.

That said, two considerations: (1) on top of a foundation, modulo finer details about the actual differences and specific limitations of the different foundations, as well as rather considerations of "adequacy", mathematics of any sort and order can be built: symbolically -- in fact, that is what a foundation is;

(2) the relevance and primality of 1st-order in foundations (as far as I can tell) has essentially to do with two aspects: (2.1) recursivity (effectivity), by which I mean, concocting systems that we can make concrete; but, even more fundamentally, (2.2) because Logical theory insists that there is no such thing as properly infinite reasoning and properly infinite proofs.

• Well, even standard (finitary) FOL admits infinite constructs in a limited sense, e.g. the axiom schemas of ZFC. $L_{\omega_{1}^{CK},\omega}$ (as I understand it) takes this a step further by allowing recursively definable infinite formulas (for example, the disjunction of infinitely many finite sub-formulas). I don’t see a reason why such infinite formulas should be less “legitimate” than the infinite schemas of standard FOL (indeed, see the use of $L_{\omega_{1}^{CK},\omega}$ in the first example in footnote of the question)
– NikS
Commented May 9 at 5:34
• But even if we require formal systems to be expressed in standard (finitary) FOL, that leaves open the original question of whether such first-order formal systems can in fact represent all “non-formal” mathematical reasoning.
– NikS
Commented May 9 at 5:38
• (1/3) The axiom schemas of -say- ZF are themselves justified (at the meta-level) by recursivity: indeed these are not "finitary systems" (which is not the same as "finitary logic", as in FOL), they have induction or equivalent, by which we (assume we can) reason finitely about infinite objects. Commented May 9 at 6:29
• (2/3) That said, keeping in mind the distinction between mathematics and a formal foundation for mathematics, Infinitary logic, which is an instance of the "infinitary reasoning" I have mentioned, and for the reasons I have mentioned, surely (at least) fails to be a valid candidate for foundations. Commented May 9 at 6:31
• (3/3) Finally, as for <<represent[ing] all "non-formal" mathematical reasoning>>, whether there even is such an ultimate foundation is more of a philosophical question, anyway it is a fact that research in foundations of mathematics is, nowadays more than ever (I am thinking Curry-Howard-Lambek, or the very reasons for Univalence), an active field of research. The criterion rather is adequacy, and not in abstract but as per the relationship of (formal) foundations of mathematics to mathematics I have tried to explain. Commented May 9 at 6:35