„for all n provable“ is not equivalent to „provable for all n“

So, 06 Sep 2009 23:16:30 +0200

For a person familiar with logic, it is no surprise that the provability of some proposition A(n) for all natural numbers n does not imply the provability of ∀n A(n), that is, ∀n PA⊢A(n) ⇏ PA⊢∀n A(n), where PA shall be Peano Arithmetic. There are known examples for situations where ∀n PA ⊢A(n) holds, but not PA⊢∀n A(n). Maybe for a person not familiar with logic, this could already be a surprise. The reason is, that there are structures satisfying PA which contain numbers which cannot be generated by finite applications of the successor function on zero, i.e. do not have the form ffff0. Of course, inside a nonstandard model. Accept it.

Well, today by coincidence I found something similar for set theory, or actually, something that can be adapted to any theory which allows representations, but for set theory it is the easiest to write down. That is still not surprising, and actually I dont know if the same example is already known, at least I didnt know it yet, so I’ll blog about it. (And of course, I hope I didnt make any mistake, I didnt really have the time to write it down formally and check it.)

Well, let ZFC be the set of axioms of set theory. ZFC is decidable, hence can be defined inside ZFC. Since we can do meta-theory inside ZFC, we can express for any decidable set A of propositons the proposition “A⊢⊥“, hence also “ZFC⊢⊥“. Hence, define ZFC0≔ZFC, ZFCn + 1≔ZFCn∪{“¬ZFCn⊢⊥“}, ZFC’≔⋃i∈ℕ ZFCi. We can also define ZFC‘ inside ZFC (and therefore also in ZFC‘ itself). Assuming ZFC being consistent yields ZFC1 being consistent, and in general – by induction – ZFCn being consistent for all natural n. That is, ZFCn is equiconsistent with ZFC for all natural n. From the compactness theorem it follows that ZFC‘ is equiconsistent with ZFC. By definition, for all finite subsets X⊆ZFC‘ we have ZFC’⊢“¬X⊢⊥“. But we cannot have ZFC’⊢“∀ XfinZFC‘ ¬X⊢⊥“ , because with the compactness theorem this would prove the consistency of ZFC‘, which contradicts Gödel’s second incompleteness theorem. Hence, we have the above situation.

It is trivial to see how the same can be done for any other First-Order-Theory which allows representations. It may be trivial. But its nice.