Re: Why is ZF not finitely axiomatizable?

On Feb 27, 6:26 am, Aatu Koskensilta <aatu.koskensi...@xxxxxx> wrote:
hurbur...@xxxxxxx writes:
I would like to know please the real reason why separation can't be
replaced by a finite numbers of instances.

What we should take to be the "real reason" for this or that in
mathematics is often obscure. But perhaps the following observations
are of some help nevertheless.

ZFC is not finitely axiomatisable because it proves the consistency of
each of its finite subtheories. How do we prove this? There are
basically two ways: using reflection, or invoking the cut-elimination
for first-order logic. The first alternative is perhaps the more
natural in a set theoretic setting. The second is more informative,
however, and goes as follows. The cut-elimination theorem for
first-order logic is provable in ZFC. Just what this theorem says is
not important, but its provability in ZFC has an important
consequences: ZFC proves, for every sentence P

 (*) if "P" is logically provable, then P

ZFC proves that 0 =/= 1, and hence, for every A, that if "A --> 0 = 1"
is logically provable, then A is false. The contrapositive of this is:
if A is true, then it "A --> 0 = 1" is not logically provable. Now,
for every finite set of axioms of ZFC, their conjunction is certainly
provable, and by the previous observation, it is provable that their
conjunction does not logically imply a contradiction. We can thus
conclude that ZFC proves the consistency of each of its finite
subtheories.

A question now naturally arises: why doesn't the above work for NBG?
The point where the above proof (sketch) falls apart is where we
conclude from the provability of the cut-elimination theorem that it
is provable for every P

 (*) if "P" is logically provable, then P

In fact, it isn't. For ZFC we prove this by using induction on a
property defined by means of a truth predicate for sentences of
quantifier complexity less than equal to P. Alas, induction is not
provable for all formulas in the extended language, that is, for
formulas that contain bound class variables.

Now, we come to what might well be regarded as the "real reason" ZFC
is not finitely axiomatisable: no theory (meeting certain conditions)
in which induction holds for all formulas in the language is finitely
axiomatisable.

--
Aatu Koskensilta (aatu.koskensi...@xxxxxx)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Thank you so much Aatu for this great answer. It clarified a lot.
Your last remark is telling: as in NBG, in NF, induction doesn't hold
for all formulas!
.

Relevant Pages

  • Re: Is this proof valid?
    ... in polynomial time; thus, PROVABLE_X is an element of P. ... Still working in ZFC, assume P!= NP. ... non-membership in P to the provability of P!= NP? ... cannot be solved in polynomial time, then ZFC is provably consistent. ...
    (comp.theory)
  • Re: Why is ZF not finitely axiomatizable?
    ... first-order logic is provable in ZFC. ... conclude from the provability of the cut-elimination theorem that it ... we come to what might well be regarded as the "real reason" ZFC ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (sci.math)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (comp.theory)
Loading