Re: Justifying transfinite induction in ZF

On Aug 8, 1:38 am, Baudouin Le Charlier
<baudouin.lecharl...@xxxxxxxxxxxx> wrote:

I understand that there are two kinds of sets (in the intuitive or
naive or real sense) in ZF:
(a) those that are definable by a formula F<x> and
(b) those that are definable by a formula F<x> such that one can prove
(exists y: x in y <--> F<x>)

Actually, those are two different senses of definability ITSELF.

There is one kind of definability: Given a structure and a particular
object per that structure, there is a formula in the language, as
intepreted by that structure, such that that formula is satisfied by
the structure and any assigment for the variables iff the free
variable in the formula is assigned to said object. That is, the
formula defines the object per the structure. (The case for more than
one free variable, thus picking out a tuple in the universe of the
structure, is similar; also for n-place functions on the universe.)

Another kind of definability (sometimes called 'representability' or
'capturing') is like the above except it involves what a theory can
PROVE. (I'll give a more precise sense of that if you like; but I'd
rather check my notes first so that I state it correctly.)

Another kind of definability: A theory proves AyE!xP(x) so that an
operation symbol (possibly a 0-place operation symbol) can be defined
per that theory. (Similar for predicate symbols.)

Thus the set of all ordinals can be defined by such a formula F but
(exists y: x in y <--> F<x>) is not provable.

Okay.

Moreover the existence of ordinals as formalized by the scheme you
explained

No, the schemata I mentioned don't formalize the EXISTENCE of
ordinals. Rather, each schema defines a set of theorems of Z set
theory.

is less certain and their 'real nature' is somewhat unclear:
one can prove the existence of some of them but one cannot see clearly
'where they stop' (sorry).

They don't "stop". And that has no bearing on the plain SYNTACTICAL
fact that each instance of the schemata is a theorem of Z set theory.

Another conclusion that I draw is that transfinite induction cannot be
proved in systems such as Z, ZF, ZFC.

Why do you keep saying this? What can be proved is a SYNTACTICAL
matter, and we DO prove the induction schemata. And every instance of
an induction schema is a theorem of Z set theory.

It can only be used as a
metatheoretic procedure.

No, any INSTANCE of a schema is a theorem of Z set theory.

In other words there is no provable formula
which can be interpreted as a formal statement of the transfinite
induction principle.

Every INSTANCE of a schema is a provable formula.

This is a good argument to dismiss the claim that
formal systems for set theory allow one to express all valid
mathematical reasoning

That one may regard ZFC is a presumed standard doesn't entail that one
doesn't also recognize that there are other forms of validity not
confined to first order logic, and that some mathematics may be
formulated in that regard.

since many usual reasoning method are justified
only on metamathematical grounds. At the limit, we can perhaps
conclude that all reasoning techniques must be accepted as obvious
(until we have 'a problem' with it), i.e. either obvious or wrong.
Hence mathematics can only be practiced but cannot be a priori
founded.

Given that that might be a reasonable view, it doesn't affect that we
prove transfinite induction for Z set theory.

PS. Well I realize that the syntax, axioms and inference rules of such
formal systems can be encoded as sets. Thus encoding of metatheorems
and metarules can be formally provable. But I really think it is an
hugly vicious circle.

It can be seen as circular. But I don't see that it is VICIOUS. Also,
my view of it is as forever escalating to meta-meta-meta...rather than
as circling back. Then the "problem" is inherent in ANY system. IF we
KEEP asking to formalize or means of formalization, no matter WHAT the
system or subject matter of that system, either we'll come back in a
circle or we'll keep going with formalization of formalization of
formalization...So I don't see this as a basis of criticism. You can't
fault set theory for what is unavoidable for ANY theory.

Anyway, please, whatever your philosophical views, at least recognize
that transfinite induction schemata are provable schemata in a meta-
theory for Z set theory and that each INSTANCE of a schema is provable
in Z set theory itself, and moreover, that there is no set of ordinals
is not a barrier to proving transfinite induction.

MoeBlee

.

Relevant Pages

  • Re: Justifying transfinite induction in ZF
    ... ordinals not to the scheme of transfinite induction. ... fact that each instance of the schemata is a theorem of Z set theory. ... circle or we'll keep going with formalization of formalization of ...
    (sci.logic)
  • Re: Cantorian pseudomathematics
    ... The axioms have to be consistent. ... formalization, at a level up, for meta-theory. ... much of mathematics is the study of comparing ... study of set theory commits one to dogmatically holding to set theory ...
    (sci.math)
  • Re: Cantorian pseudomathematics
    ... What I mean is set theory was not born just by the great thought of Cantor. ... of mathematics behind, which help greatly, and which even where necessary for the theory to be imagined. ... formalization, at a level up, for meta-theory. ... scientists and engineers doesn't have to be used by engineers. ...
    (sci.math)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... amount of set theory, and then introductory abstract algebra, ... that the characteristic function of S is recursive (and you know what ... formalization, it could look something like this, ... sequence of formulas, or an ND tree, or an ND sequence of pairs of ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... amount of set theory, and then introductory abstract algebra, ... that the characteristic function of S is recursive (and you know what ... formalization, it could look something like this, ... sequence of formulas, or an ND tree, or an ND sequence of pairs of ...
    (sci.logic)