MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Should consistency be considered as a concept in the metatheory?

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.

-
As long as the metatheory includes a small amount of arithmetic, you can just treat consistency statements about effectively axiomatized theories as the corresponding $\Pi^0_1$ sentences. If that's not what you're asking about, could you clarify the question some? – Carl Mummert Feb 14 2011 at 18:53
In that case consistency just reduces to a statement within the theory. But is there any prior concept in the metatheory that expresses that notion? For example, if a certain theory T does not have the right amount of arithmetic needed to produce consistency statements, the only way I see to express the concept of consistency is to develop first some set theory S that includes infinite sets and work within S to interpret the axioms of T. Then consistency would actually appear at this theoretic level, expressed by some sentence in S, but we would be working with a copy of T inside S. – godelian Feb 14 2011 at 19:36
I beg to differ. In order to be able to treat universally quantified statements about natural numbers there is no need to develop any amount of set theory. It is sufficient to develop induction principles that tell us how to prove universally quantified statements about natural numbers. Such induction principles can be understood as descriptions of what natural numbers are, and they certainly need not presuppose that the totality of natural numbers has the same status as the number 42. – Andrej Bauer Feb 14 2011 at 21:47
Let me clarify another point. Induction and recursion are rules which tell you how to do something. They do not presuppose any kind of infinity or anything like that. Which is why I essentially agree with Carl's first comment. – Andrej Bauer Feb 14 2011 at 21:49
I like to think of myself as being consistent, even though I tend to believe in the axioms of Peano arithmetic. – Andrej Bauer Feb 14 2011 at 22:42

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.

-