Number of ZFC proofs and are meta-proofs valid ZFC proofs [closed]

Question

How many proofs in the language of ZFC are there? I would say countably infinite, since every proof is a finite sequence of symbols over a finite alphabet (e.g. ASCII).

Consider the proof in https://proofwiki.org/wiki/Woset_is_Isomorphic_to_Unique_Ordinal. In its essence, the reasoning is as follows:

Let $(W, \prec)$ be a well-ordered set. From $(W, \prec)$ construct a well-order of well-orders $(W', \prec')$ which contains $(W, \prec)$ as its largest element. Prove by transfinite induction over $(W', \prec')$ that any of its elements is order-isomorphic to some ordinal. Since $(W, \prec)$ is an element of $(W', \prec')$, $(W, \prec)$ is order-isomorphic to an ordinal. As $(W, \prec)$ was arbitrary, conclude that every well-ordered set is order-isomorphic to an ordinal.

Sounds reasonable. But isn't this exactly the same as saying:

For all well-ordered sets there exists a proof* (by transfinite induction), that proves the existence of an ordinal that is order-isomorphic to that set.

So have we just instantiated proper-class-many ZFC-proofs? Moreover, the existential quantifier quantifies over a proof, not a set, so the reasoning is a meta-proof at most? I don't want proof* to be interpreted as a set that encodes a ZFC-proof inside models of ZFC, because in that models there could exist proofs* of non-standard-integer lengths, correct?

Is this meta-proof valid?

EDIT:

The $\forall x: x=x$ example actually helped, but in a different way.

My thinking was, that a proof of the form "Let $x$ with $P(x)$ be arbitrary, then infer $\phi(x)$" is a prosaic inference of the formula $\forall x: P(x) \rightarrow \phi(x)$ by using inference rules from quantified formulae to quantified formulae. Furthermore have I thought that a hilbert system includes $\forall x: x=x$ implicitly as an axiom. So for your counterexample, there was no need to talk about proofs of $x=x$ for every $x$. For the well-order case however, I could not imagine how the deduction would look like. The reasoning why transfinite induction works on a specific well-ordered set is shown by contradiction. But how could I "suppose otherwise" inside the formula $\forall W ( ... )$? So my conclusion was, that the proof indended to show the existence of proofs.

That said, I see now what I have missed. A hilbert system factually includes $x=x$ for every variable $x$, and via universal generalization one can infer $\forall x: x=x$. Similarly, the well-order proof actually proves a formula that is free in $W$, and the generalization is then implicit.

Sorry and thank you.

Answer 1

The essence of your argument has nothing to do with well-orders. For example, we can also prove that for every real number $x$, the equation $x=x$ holds. That is, we proved $\forall x\in\mathbb{R}\ x=x$. Your suggestion is now to consider every particular real number $a$, and realize that we have a proof that $a=a$. Does this give uncountably many proofs, one for each real number? No, because $a=a$ is not a statement in the formal language, which you said is finite, and so $a=a$ doesn't even count as a statement in the formal language. If we were to expand the formal language with constant symbols to allow us to refer to $a$, then indeed, we could prove $a=a$, but in this case, the language itself would be uncountable and so the first part of your argument would break down.

Similarly, for the proper class case, we can prove $\forall x\ x=x$, where the universal quantifier ranges over all objects $x$, including every ordinal. Does this give a proper class of proofs, of the statements $a=a$ for every object $a$? No, again, because those statements are not in the formal language. If we augmented the formal language with constants for every object (or every ordinal), then indeed we would have a proper class number of proofs, but only because the language itself was already a proper class.

So ultimately, the solution to your confusion is to pay more attention to what exactly is in the formal language and what is not. If we can refer to the objects directly with constants in the formal language, then the claim that the language has a finite alphabet is false, invalidating the first part of the argument that there are only countably many proofs. And if we cannot refer to those objects with constants in the formal language, then we cannot have proofs of the statement $a=a$ or any other statement about $a$, since these assertions are not in the formal language.