Re: How do We Know that ZF is the Axiomatization that Proves everything Provable?

On Feb 9, 9:36 am, Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On Feb 8, 4:26 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:

My response to this post has not shown up in my interface. So I'll
rewrite an abbreviated version just in case the original version
doesn't show up.

On Feb 7, 9:25 am, Charlie-Boo <shymath...@xxxxxxxxx> wrote:

How do you define formalizing in ZFC?

As in a previous post, personally, I'd say, by the "reading off the
formulas" approach.

 Are you allowed to add axioms?

Only definitional axioms, which do not extend the substance of the
theory

You'll have to give an example to really debate that one.  The
distinction can get blurred.

No, no blurring. 'definitional axiom' is a precisely given term of
mathematical logic.

But I'll give you an example anyway:

AxAy(yeUx <-> Ezex yez).

First of all, added definitions should not be within the proof, only
before and after.

Correct. And that's how we do it.

 Otherwise you can call most axioms a "definition".

No, definitions meet specific criteria not met by ordinary axioms.

And in fact they are derived from definitions.  As is most everything,
no?

We derive from axioms with a logic. In one approach, the definitions
are a special kind of axiom, called a 'definitional axiom'. Other
approaches by different people too, but I like the definitional axiom
approach.

Remember that people will steal anything that isn't tied down.

I have no idea what that has to do with this.

Otherwise, we should indicate by 'ZFC+S' to show that a particular
result used S in its proof.

Then ZFC's axioms have nothing to do with it?

What a bizarre question. The claim is that virtually all of ordinary
mathematics can be expressed and proven in ZFC. If there is a
particular theorem that needs axioms other than ZFC, then one may
indicate what additional axioms were used. If that is a theorem of
ordinary mathematics, then it is exception to the generalization about
proving using only ZFC, but still the claim is that VIRTUALLY all (or
MOST of) the theorems of ordinary mathematics can be proven in ZFC, so
such exceptions do not refute the claim. If there were enough
exceptions though, then, yes, the claim would be refuted.

 If it is done
completely in CBL, we say CBL|-Pythagorean Theorem.  Otherwise we say
CBL+S|-Pythagorean Theory.

We say, if CBL with S added as an axiom proves the Pythagorean
theorem.

Okay. So what?

 That's true, you know.  So CBL works just
as well as ZFC (actually a lot better.)

Wonderful.

If not, I'd like to see how the Pythagorean Theorem is proven.  If you
do have to add axioms, then I would still like to see it, and
especially how the ZFC axioms played any actual role in that
particular proof (as opposed to saying "You need ZFC to state that
there is an infinite set." in response to every theorem, which is not
the point.)

The claim is not that ZFC is necessary for such a formalization, but
rather that it is sufficient.

What do you mean by "ZFC is necessary"?

You know what the word 'necessary' means. Are you trolling me to
answer just arbitrary questions you make up?

Obviously, in this context, 'ZFC is neccessary for such a
formalization' means that a formalization cannot be achieved without
using ZFC. And I'm making the point that that is NOT claimed.

 Are we talking about the
distiction of whether any of ZFC's axioms are used in a particular
proof?  

No.

But I think we have already established that ZFC's axioms are
irrelevant.

I have no idea how you think you established that or even what your
defintion of 'relevent' is in such context.

 We're now talking about using set theory expression for
symbols, amd what the result would be.

No, the language and the definitions provide the symbolization. The
axioms and the logic provide the deductive power.

As to proving the Pythagorean theorem in ZFC, we can take an ordinary
proof (say, Euclid's), then make sure we've defined all the
terminology in that proof into set theoretical terminology and have
proven in ZFC all the lemmas used in the ordinary proof. Then we can
give pretty much the ordinary proof itself as an informal rendering
that convinces us of the existence of a formal proof in ZFC.

Is that it?  Can you actually carry out that process?  Or at least
tell me which proof, how you define some of the terminology, and how
you would prove a lemma or two?  Nothing elaborate, just a couple of
samples of a term and definition and proof of a little lemma.

If I have time and interest, I'll post some of it (NOT a promise). I
can put it in pdf format (a lot better for reading than ASCII) but I
don't know where I can post that pdf.

Or maybe we can be open about it: You won't give it because you don't
have it.

I was ALREADY open to say that I haven't typed out all of material to
prove the Pythagorean theorem in ZFC. I have typed out some of the
material leading up to it though. Maybe I can figure out how to get a
PDF put up somewhere (I don't want to use my personal web space). But
this is not a promise. If you really don't believe that you can
express a suitable version of theEuclid-Hilbert axioms as a certain
kind of system in ZFC and thereupon prove the Pythagorean theorem,
then so be it, but using a book such as Moise's would allow you to see
how to start such a project.

 So you say it's too complicated.

I hope it would not be too complicated given a fair amount of time,
interest, and patience. But I can't promise to have those rescources
of time, interest, and patience to do all the typing and formatting
just to prove a point. Again, if you know first order logic, the
axioms of set theory, and have some geometry books (especially
Moise's), then you have the tools for such a project.

 But that argument does not
hold for anything.  You are now totally outside of the original
question and simply declaring things to be complex and so you need not
prove anything.  I mean, rather than hinting at it.

No, I admit that if I don't show you how to prove the Pythagorean
theorem in ZFC then I have not proven to you that it can be done.

The ZFC axioms have nothing to do with anything but an attempt to
avoid Russell's Paradox.  The Peano Axioms are another matter, as they
guarantee that Addition, Multiplication and the Universal Set are
representable, which has many implications.  But that's all you have -
some theorems of Set Theory from ZFC proper, and much of simple
Arithmetic from the Peano Axioms that are added to that.

No, theorems of ZFC include all kinds of stuff about mathematics other
than arithmetic.

Examples?  I won't even ask for substantiation.  Now isn't that
another good idea?  So you don't have to skip all those good examples
that are too complex to explain.

I gave examples by now (see Friday's and today's earlier post). Please
stop asking me just to type names of theorems.

The fact that there are no references to anything outside of sets and
integers (not e.g. Geometry or Trigonometry) ever being carried out in
ZFC shows that.

ZFC talks about all kinds things other than integers. Of course, in
ZFC, with a suitable definition of 'set', we prove that every object
is a set; but that doesn't preclude that there are certain kinds of
sets and that certain kinds of sets are taken to be certain kinds of
mathematical objects such as real numbers, lines, topologies, graphs,
etc.

But can you prove their theorems???

Yes. We've already said that. When I read proofs in a topology,
analysis, abstract algebra, or graph theory, one part of my mind is
mentally verifying that each step uses nothing but first order logic
and set theory axioms applied to previously proven statements that
I've previously verified use nothing to prove but first order logic
and set theory axioms. Then for those proofs that are complicated
enough that I can't do that just mentally, I write it out. That's what
one does if one is interested in the question of provability in ZFC.
Of course, not everybody is interested in that question, but if one is
sufficiently interested, then it can become almost a habit to have a
continual mental monitor checking that everything in the proofs are
within ZFC.

 I can speak 100 languages myself.

Wonderful.

And it's not the ability to "represent" the objects of the system that
is at issue.  You can pair up any two r.e. sets of expressions, and
call the first set or graph or list or wff or program zero.  And the
next one you call one.

You can do that. But that doesn't preclude that set theory can be used
to represent the kinds of objects of ordinary mathematics.

No, not that it precludes it, but that it can be done for any formal
system and ZFC provides nothing.

Not by any formal system. First order PA is not going to prove Bolzano-
Weierstrass.

 We don't use its axioms because they
do not suffice for anything outside of arithmetic and sets.  Certainly
not for everything.

No one said 'everything'. The claim is that ZFC suffices for proving
the theorems proven in the ordinary mathematics of arithmetic,
analysis, topology, abstract algebra, graph theory, etc. Of course,
everything in ZFC is about sets (since, with a suitable defintion of
'set', we can prove in ZFC that every object is a set), but with the
membership relation, we are able to express numbers, planes, vector
spaces groups, topologies, manifolds, etc. etc. in terms of set and
prove the ordinary theorems about them.

 And its syntax is arbitrary and any expressions
can in fact be used.  Those are actually just Models.

I don't know what you would mean by a 'non-arbitrary syntax'. I have
no idea what you mean by 'any expression can be used'. And I have no
idea what mathematical sense of 'model' you have in mind, if any.

I am not saying that we cannot interpret ZFC axioms to be statements
about other things!!!  I am saying that ZFC has a fixed set of axioms,
and they will not magically produce axioms for other branches of
Mathematics by substitution.  That's ludicrous.

So? No one said that ZFC magically produces anything.

The problem is that you need to know specific relationships among
those objects, and the ZFC axioms state only certain relationships.
You could probably prove the following interesting question: For any
r.e. set, use Peano's Axioms to prove that it is r.e.  But this
doesn't give you things like the Pythagorean Theorem and the rest of
common Mathematics.

Whether such and such a thing about PA gives the Pythagorean theorem
does not govern whether we can prove the Pythagorean theorem in ZFC.

You'll have to define that distinction.

You said somethhing about PA and the Pythagorean theorem, and my
response is that whatever goes on about PA and the Pythagorean theorem
doesn't rule whether we can prove the Pythagorean theorem in ZFC.

MoeBlee

.

Relevant Pages
Loading