Of course any proof must be, in the most literal sense, finite (must be written down on a finite stack of paper or storage drive of finite capacity). But even on a finite piece of paper one can construct "effectively infinite" statements. For example, suppose I define infinite class of (finite) first-order logic formulas, e.g. "any formula conforming to such-and-such a syntax" (analogous to how the Axiom Schema of Replacement is the infinite class of all sentences conforming to a particular syntax). Then it seems conceptually valid to assert a predicate formed by the (infinite) disjunction of all these formulas (i.e. "if any one of these formulas is true, then..."). Of course, standard (finitary) first-order logic doesn't allow such infinite disjunctions. But an infinitary language such as $\mathcal{L}_{\omega_{1}^{CK},\omega}$ could accommodate this (I think?), as could a non-formalized proof in "mathematical English".
So my question, in a nutshell, is: are proofs that are infinite in the sense described above considered "legtimate"? For example, if a theorem were to be provable in $\mathcal{L}_{\omega_{1}^{CK},\omega}$ but not deducible in standard (finitary) first-order logic from any system of first-order axioms, would it qualify as a "legitimate" mathematical truth?
- I realize this is a matter about which there may be some difference of philosophy/opinion (perhaps depending in part on one's conception of "number" in the metalanguage, and thus whether the notion of an "infinite formula" or "infinite statement" is valid in the first place)
- But Ernst Zermelo, for one, does seem to have regarded such "infinitary proof" as legitimate: see this article (especially section 7 onward).
- Also, this answer seems to imply the legitimacy of proof in the infinitary language $\mathcal{L}_{\omega_{1}^{CK},\omega}$, calling it the "smallest 'nice' fragment of infinitary logic which is stronger than first-order logic", whose Barwise compactness property "has been incredibly useful in proving results relevant to classical computability theory."
Update: Probably worth underscoring that what I’m asking here is in some sense a “sociological” question about what mathematicians believe. I suspect some would say that the only “fully legitimate” mathematics is that which is formalizable in standard (finitary) first-order logic, whereas others would be more accepting of one or another kind of infinitary proof. But I don’t know which view(s) is/are the most prevalent.
