FOM: finitely axiomatized fragments of ZFC, etc.

[john l. bell]

>Date: Wed, 03 Mar 1999 18:21:30 -0500
>To: fom-digest
>From: "john l. bell" <jbell at julian.uwo.ca>
>Subject: finitely axiomatized fragments of ZFC, etc.
>
>Dear All:
>
>Concerning the recent discussion over the provability within ZFC of its
finitely axiomatized fragments, it seems to me that the whole business
depends on where one places the phrase "ZFC proves." Thus the assertion
>
>(*) If T is a finitely axiomatized fragment of ZFC, then ZFC proves Consis(T)
>
>is (equivalent to) a scheme of assertions, each one of the form
>
>(**) Given theorems f1,...,fn of ZFC, ZFC proves the consistency of
{f1,...,fn}.
>
>Each instance of (**) is a consequence of the usual reflection principle
whose proof involves an induction (which can, for each fixed n, be
formalized in ZF) on the formation of the explicitly given list of
sentences f1,...,,fn (see e.g., Drake, "Set Theory," p 101 et seq. or Bell
and Machover, "A Course in Mathematical Logic," pp. 491-495): this, I take
it, is what Harvey means by "the usual inductive proof" (at least in the
case of set theory). 
>
>On the other hand, perhaps what Colin has in mind is another positioning
of the phrase "ZFC proves". If we formalize within ZFC the syntactical
notions of being a theorem of ZFC, of being a consistent set of first-order
sentences, etc., then (*) could be "conflated" with the assertion 
>
>ZFC proves: (***) for all T, if T is a finite set of theorems of ZFC, then
                                                Consis(T).
>
>Now, assuming ZFC consistent, it cannot prove (***), since that would
violate Godel's 2nd incompleteness theorem. But there is (as far as I am
aware) no "informal" >inductive< proof of (***) not formalizable or
provable in ZFC whose correctness we accept for metatheoretical reasons.
The "informal" acceptability of (***) seems, if anything, to be based on
the correctness of (**) for each specific list of theorems of ZFC. In other
words, the failure of ZFC to prove (***) stems not from the
inexpressibility or unprovability within ZFC of an induction, but rather
from the failure of the omega-rule there.
>
>On the other hand, a genuine instance of "expressible" but "unprovable"
induction can be found in Mostowski's (1951?) Fundamenta Mathematicae paper
"Some Impredicative Definitions in Axiomatic Set Theory." There he shows
that full induction fails in von Neumann-Bernays-Godel set theory NBG. He
first constructs within NBG a truth predicate for ZF-sentences and then a
predicate F(n) of natural numbers n which, roughly speaking, asserts that
all ZF-theorems of "complexity" < n satisfy that truth predicate. Then he
shows that
>
>                   F(0) and for all n [F(n) => F(n + 1)]   
>
>is provable in NBG, but - assuming NBG consistent -
>
>                          for all n, F(n)
>
>is not. Why? Because this latter sentence asserts that every ZF-theorem is
true, and so, if it were provable in NBG, it would follow that the
consistency of ZF would be provable in NBG. But Novak had already shown
that ZF and NBG are equiconsistent, so the consistency of NBG would be
provable in NBG, again violating Godel.
>
>-- John Bell    

*****************
Professor John L. Bell
Department of Philosophy
University of Western Ontario
London, Ontario
Canada N6A 3K7

Web page: http://publish.uwo.ca/~jbell/