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?


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.


closed as off-topic by Andrés E. Caicedo, Stefan Kohl, Wolfgang, Simon Thomas, Myshkin Nov 17 '16 at 8:13

This question appears to be off-topic. The users who voted to close gave these specific reasons:

  • "MathOverflow is for mathematicians to ask each other questions about their research. See Math.StackExchange to ask general questions in mathematics." – Stefan Kohl, Myshkin
  • "This question does not appear to be about research level mathematics within the scope defined in the help center." – Andrés E. Caicedo, Wolfgang, Simon Thomas
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 4
    $\begingroup$ What the paragraph is actually saying is a single proof of the statement "every woset $(W,\prec)$ is isomorphic to a unique ordinal", and the proof proceeds by "take any $W$ and prove stuff". This is still a single proof. It doesn't give you proper class of proofs pretty much because, for most wosets $(W,\prec)$, you can't actually define this woset, so you can't even state "$(W,\prec)$ is isomorphic to a unique ordinal" in the language of ZFC. $\endgroup$ – Wojowu Nov 16 '16 at 12:30

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.


Not the answer you're looking for? Browse other questions tagged or ask your own question.