What is the difference from a theorem and a meta-theorem?

Question

I'm confused about what a meta-theorem exactly is and if a meta-theorem can be used to prove a theorem. To illustrate my confusion i give an example.

Given the three statements:

1. Every vector space has a Hamel basis.

2. If a statement in ZFC cannot be proved without AC then this statement is not constructive.

3. In infinite dimensional vector spaces is generally impossible to construct the elements of a Hamel basis.

I think that all agree that 1) is a theorem in ZFC. I suppose that 2) is a metatheorem about ZFC (but I don't know the proof). Since 3) is a consequence of 1) and 2) is it a theorem or a meta-theorem?

Answer 1

Theorems are things proved from a theory. Meta-theorems are things proved about the theory.

The statement:

If $\sf ZF$ is consistent, then $\sf ZF$ does not prove $\sf AC$.

Is a meta-theorem about the theory $\sf ZF$. It quantifies over all proofs that we can write from the axioms of $\sf ZF$. If you like to think about it semantically, proofs are not objects of the universe of $\sf ZF$, sets are. We can represent proofs as sets, and we can show that this representation is somewhat faithful to the source; but proofs from $\sf ZF$ are not objects of the model of $\sf ZF$ we work with.

On the other hand,

$\sf ZF$ proves that the axiom of choice is equivalent to the statement "Every vector space has a basis".

Is a theorem, cleverly disguised as a meta-theorem. It might talk about provability from $\sf ZF$, but really what we say is that there is a proof from $\sf ZF$ that the axiom of choice is equivalent to some other statement. We are not really interested in the meta-theory here, we are not interested in the proof that there exists a proof. We just write the proof down and check that it is a valid proof.

So you need to separate what is in the theory, what are the objects that the theory is concerned with; and what is in the meta-theory, which are statement about the theory, about proofs, etc.

---

Finally, let me remark, that "something is not constructive" is not a well-defined notion. There are different interpretation for the term "constructive", one of which is by definition "something provable without the axiom of choice".

So since "constructive" has no concrete meaning, it's not quite in the meta-theory or in the theory. It's more of a philosophical argument as for the meaning of the term "constructive". (At least until further clarifications.)