6
$\begingroup$

If we take a first-order theory (like $\mathsf{ZFC}$, or $\mathsf{ZFC}$ plus some additional axioms) as the foundation of mathematics, does that imply that mathematical reasoning (theorems, proofs, algorithms, etc.) must be expressible in first-order logic (and associated rules of inference) in order to be "legitimate"? (not that you necessarily have to actually write it all out in FOL syntax, but that you have confidence that you could do so). Is there any sort of consensus around whether such "first-orderizability" is deemed a requirement of "legitimate" mathematical reasoning?

Some comments/observations related to the question:

In Mathematical Logic by Ebbinghaus et. al. (2nd ed.), section VII.2 states that, given a foundation of set theory with axioms $\boldsymbol{\Phi_0}$ (and the first-order language of set theory denoted by $L^S$), then:

Mathematically provable propositions have formalizations which are derivable from $\boldsymbol{\Phi_0}$. Thus it is in principle possible to imitate all mathematical reasoning in $L^S$ using the rules of the sequent calculus. In this sense, first-order logic is sufficient for mathematics.

But then later (section IX.2) they say:

The class of torsion groups cannot be characterized in first-order logic. But we can axiomatize this class if we add to the group axioms the "formula" $\forall x (x \equiv e \lor x \circ x \equiv e \lor x \circ x \circ x \equiv e \lor \ldots)$. Thus we gain expressive power when allowing infinite disjunctions and conjunctions. Such formations are characteristic of the so-called infinitary languages...This leads to the system $\mathcal{L}_{\omega_{1},\omega}$

This seems like a direct contradiction of the first quote (from VII.2). If a notion like "let $\mathfrak{G}$ be a torsion group" can't be expressed in (finitary) first-order logic, then it's hard to see how one can argue that this language is "sufficient for all mathematics".

More generally, the following considerations seem to weigh against restricting mathematical reasoning to arguments expressible in standard (finitary) first-order logic ("FOL"):

  1. Since an infinitary language like $L_{\omega_{1},\omega}$ is an extension of FOL, it seems like one could take $L_{\omega_{1},\omega}$ (instead of FOL) to be the language of a set theory like $\mathsf{ZFC}$ (the axioms remain valid statements of the language). In that case it would seem at least plausible that with a more expressive language (i.e. $L_{\omega_{1},\omega}$) having become available, one might be able to use it to formally prove statements which are true in every model of $\mathsf{ZFC}$ yet are not provable in FOL (maybe not even expressible in FOL).
  2. This post re "non-first-orderizability" on Terence Tao's blog (see especially last paragraph staring with "It seems to me that first order logic is limited") appears to take the position that mathematical reasoning need not be "first-orderizable", or even formalizable at all in any known formal language (see Tao's comments regarding "mathematical English").

Update/Clarification:

I realize that different axiom systems differ as to which first-order statements they can prove. So potentially statement $S$ is not formally derivable as a consequence of first-order axioms $\boldsymbol{\Phi}$, but $S$ is a formal consequence of some stronger first-order axiom system $\boldsymbol{\Psi}$.

But what I have in mind is a different issue, namely the notion of a statement in “mathematical English” (to borrow Tao’s phrase) which, due to its logical “structure”, cannot in any way even be expressed as a formula in first-order logic (regardless of what axioms or ontological assumptions one stipulates).

  • Such “inherently non-first-orderizable” statements are what Tao seems to be describing in the last paragraph of the blog post, starting with “first order logic is limited by the linear…nature of its sentences” and following up with “this does not fully capture all of the dependency tree of variables” and “subtleties may appear when one deals with large categories”.
  • A concrete example might be something equivalent to a formula involving infinite disjunction in $L_{\omega_{1}, \omega}$: given a well-defined infinite collection of (finite) sub-formulas $\Phi_{n}$, imagine the (infinite) formula $\Phi_{0}(x) \land (\Phi_{1}(x) \lor \Phi_{2}(x) \lor \Phi_{3}(x) \lor \ldots)$ Surely such a statement is not, in general, expressible in (standard, finitary) first-order logic (unless somehow it can always be made first-order-expressible by “upgrading” to a stronger theory? like upgrading from $\mathsf{ZFC}$ to Kelley-Morse set theory, or something like that?)
$\endgroup$
3
  • $\begingroup$ How do we decide what qualifies as a “mathematical theorem”? $\endgroup$
    – Porky
    Commented Apr 1 at 7:44
  • $\begingroup$ I presume it to mean: a statement which is shown to be true in every model of one’s chosen foundational axiom system (such as $\mathsf{ZFC}$). The wrinkle there regards what it means for a statement to be “shown” to be true…which is kind of the crux of my question. $\endgroup$
    – NikS
    Commented Apr 1 at 7:57
  • $\begingroup$ No. However, second-order descriptions are often seen as presuming an underlying theory of sets/relations/properties, and many set theorists want to avoid that presumption. $\endgroup$
    – Corbin
    Commented Apr 1 at 17:56

2 Answers 2

14
$\begingroup$

Yes, when someone says that ZFC is a suitable foundation for mathematics, that means that all standard mathematical notions can be expressed in the language of ZFC using first-order logic and all standard mathematical arguments can be written as derivations from ZFC using first-order logic.

For your particular example of torsion groups, there is a first-order formula $\psi(x)$ with one parameter in the language of set theory such that, for any $x,$ $\psi(x)$ holds iff $x$ is a torsion group.

The statement that torsion groups can't be characterized in first-order logic means something different, namely:
There is no first-order sentence $\varphi$ in the language of group theory such that, for every group $G,$ $G$ is a torsion group iff $G$ satisfies the sentence $\varphi.$
Note that $\varphi$ here is required to be in the language of group theory; it can only quantify over elements of the group (not subsets of the group, or natural numbers, or anything else), and it can't refer to any functions or relations other than the multiplication operation of the group.

So how would you write the original formula $\psi$ in the language of set theory? The formula $\psi(x)$ would say something like the following (you'd have to expand all the circumlocutions fully, of course, but, although that's a bit unwieldy, it's routine to do):

  1. $x$ is an ordered pair $\langle G, \circ\rangle.$

  2. $\circ$ is a function mapping $G\times G$ to $G$ satisfying the axioms for a group.

  3. For every $a\in G,$ there exists a natural number $n$ and a function $f: n+1\to G$ such that:

(i) $f(0) = a;$

(ii) $(\forall k\lt n)(f(k)\circ a = f(k+1));$

(iii) $f(n)$ is the identity element of the group $\langle G, \circ\rangle.$

This is a first-order formula in the language of set theory, but you can see that it is not a formula in the language of group theory; it talks about objects other than elements of $G,$ and it involves quantifying over natural numbers (and also functions, or finite tuples from $G).$

(For anybody who hasn't seen the usual set-theoretic convention regarding natural numbers, I should mention that $\psi$ as written above uses the formulation that for any natural number $m,$ we have $m = \{k \mid k \lt m\}.)$

$\endgroup$
7
  • $\begingroup$ I see, that makes sense. But does it mean that one should read Terence Tao’s aforementioned blog post as advocating a philosophy (somewhat) contrary to the one you describe? He seems to be endorsing the “legitimacy” of non-first-orderizable reasoning (or maybe I’m just misunderstanding him?) $\endgroup$
    – NikS
    Commented Apr 2 at 1:29
  • 1
    $\begingroup$ @NikS It looks to me like Tao, in the blog post, is pointing out that arguments involving proper classes can involve subtle points that are easily missed -- which I agree with. But I'm not sure how he would propose to address this by extending first-order logic (rather than simply changing the axiomatization being used within first-order logic), or how such an extension could be put on a solid foundational footing. I agree that it sounds like he's thinking of something specific that he has chosen not to elaborate on. Maybe he talks about this elsewhere? $\endgroup$ Commented Apr 2 at 1:57
  • 1
    $\begingroup$ FYI -- you can nest (i-iii) under list item #3 by adding three spaces at the beginning of each of those lines. (I tried to suggest an edit that does this, but StackExchange doesn't allow proposed edits that modify only whitespace.) $\endgroup$
    – ruakh
    Commented Apr 2 at 17:06
  • $\begingroup$ @ruakh Thank you; I appreciate the comment. I remembered there was a way to do it but didn’t want to bother looking it up since it looked OK and it was just a one-off use. $\endgroup$ Commented Apr 2 at 17:51
  • 1
    $\begingroup$ This answer addresses the question as I described it, so I’ll mark it as “accepted” (and post follow-ups as a separate question) $\endgroup$
    – NikS
    Commented Apr 14 at 0:21
0
$\begingroup$

The question of whether first-order logic is sufficient for all of mathematics is different from the question of whether first-orderizability is a requirement for legitimate mathematical reasoning.

Possibly first-order logic (in the sense of first-order set theory, as explained by Mitchell Spector) is sufficient for all of mathematics. This does not at all imply that whether some is a piece of legitimate mathematical reasoning depends on its first-orderizability.

For example, people were already proving theorems of the form

For each $x$ in [some domain] there are only finitely many $y$'s in [some domain] such that [some property holds for $x$ and $y$].

a long time before anyone invented ZFC or even first-order logic. So, if you want to claim that first-orderizability is necessary for legitimate mathematics, you and thereby claiming that for several centuries it was unknown or indeterminate whether such theorems are legitimate pieces of mathematics. This, to me, is non-sense. People didn't have to wait until someone invented first-order set theory to see that

Every polynomial which is not identically zero has finitely many roots.

is a legitimate piece of mathematics. (Yes, this theorem can be expressed as a first-order claim in the language of set theory, but the point is that its status as a legitimate piece of mathematics does not depend on this.)

$\endgroup$
14
  • 1
    $\begingroup$ I think OP's question was how to reconcile the idea that first-order ZFC could be a suitable foundation for mathematics with the fact that torsion groups can't be characterized in a first-order way. The key point is that the languages involved are different in those two statments (as in my answer). $\endgroup$ Commented Apr 1 at 19:28
  • $\begingroup$ I also don't think anyone has ever claimed that first-order logic was a prerequisite to doing mathematics; as you pointed out, people were doing mathematics long before first-order logic was invented. The relevant claim is that first-order ZFC can be a suitable foundation for all of mathematics. (continued...) $\endgroup$ Commented Apr 1 at 19:35
  • $\begingroup$ ... It's hard to see how second-order logic (or some infinitary logic) could be a suitable foundation for mathematics, because those logics have to rest on set theory. But it's also true that even first-order logic depends on Peano arithmetic or some other foundation for discrete mathematics. So there are a number of issues here. However, OP's question had to do with the more straightforward issue of the language being used in the two claims (first-order ZFC being a foundation for all math vs. torsion groups not being characterizable in a first-order way) which look contradictory at first. $\endgroup$ Commented Apr 1 at 19:57
  • $\begingroup$ @MitchellSpector Part of the OP's question is indeed based on this essentially linguistic confusion, and you do a good job addressing this. But they also explicitly ask (in the title and twice in the body of the question) whether all mathematical reasoning must be first-orderizable in order to count as "legitimate mathematical reasoning". $\endgroup$
    – Pilcrow
    Commented Apr 2 at 1:41
  • 1
    $\begingroup$ I certainly agree that there's a deeper question there -- I just think that OP was actually stuck on that other issue. (For what it's worth, I don't think ZF exhausts our mathematical intuition, but trying to go beyond first-order logic for a foundation seems problematic to me.) (By the way, Pilcrow, I can't seem to tag you -- is your name being misinterpreted because it's the same as the name of a character?) $\endgroup$ Commented Apr 2 at 1:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .