Question

Consider the statement: "ZFC is consistent". Normally this is considered at first sight as a statement in the metatheory. But if we follow Kunen's (informally) description of what the metatheory is (i.e., finitistic reasoning), there seem to be some problems to place that statement precisely at the metatheoretical level.

First of all, since ZFC is not finitely axiomatizable, it seems the metatheory fails to absorb the theory ZFC as a whole, and instead we should first develop some finitely axiomatizable fragment of set theory within which we can correctly formulate the theory ZFC.

But suppose we work with a finitely axiomatizable theory T. Does it make sense now to ask in the metatheory whether T is consistent? At first sight, the consistency of a theory as a concept supposes we can quantify over all possible formal proofs within the theory and assert that none of them actually ends in contradiction. But isn't this a set-theoretical analysis? Shouldn't we first develop some set theory and only then define set-theoretically the concept of consistency?

Of course if T happens to have a finite model, we are inclined to assert, in the metatheory, that we can never find a proof of a contradiction. But instead of saying that T is consistent, shouldn't we just say that T has a finite model? Or is the conclusion of consistency from this a valid finitistic reasoning that should be part of the metatheory?

Finally, what if T does not have a finite model? It seems to me that some intuitionistic approach should be taken in the metatheory, in the sense that concepts such as inconsistency are meaningless unless we can actually find a specific proof of a contradiction.

Answer 1

Most people regard induction and recursion as finitistic. As Andrej Bauer commented:

Induction and recursion are rules which tell you how to do something. They do not presuppose any kind of infinity or anything like that.

As a consequence, the standard weak metatheory used in practice is Primitive Recursive Arithmetic (PRA).

Although very weak, PRA is strong enough to formalize Gödel coding. Using such coding, the axioms of ZFC (to take a concrete example) can be enumerated and recognized by primitive recursive functions. One can also recognize formal proofs from ZFC axioms using a primitive recursive function.

Thus, there is a primitive recursive function $B_{ZFC}(x,y)$ which takes value $0$ if and only if the numeral $x$ is a Gödel code for a formal proof of the Gödel coded sentence $y$ from the axioms of ZFC. Taking $y$ to be the Gödel code for your favorite contradiction, say $0 = 1$. The consistency of ZFC can be expressed as $\forall x (B_{ZFC}(x,y) \neq 0)$. As Carl Mummert pointed out, this is a simple $\Pi^0_1$ statement in PRA. While we don't know whether it is true or false, it is a perfectly meaningful statement from the finitistic point of view.