Re: need help in understanding Torkel's ZFC comment

From: Charlie-Boo (chvol_at_aol.com)
Date: 12/04/04 

Date: 3 Dec 2004 23:08:50 -0800

> >>Ullrich> That's not a formal proof from the axioms of ZFC.
> >>
> >>>Neither is the MetaMath proof of 2+2=4.
> >>
> >>Yes it is. If you believe otherwise then point out an axiom that is used
> >>in the proof but is not part of ZFC.
> >
> > Very few of the terminal nodes of the proof tree are ZFC axioms,
> > because ZFC has nothing to do with the fact that 2+2=4. (Only 1 set
> > is involved, so we need not consider the question of what sets exist
> > in general. 2+2=4 regardless of what ZFC says.)
> >
> > At these nodes you will find other "axioms", rules that allow
> > arbitrary wffs to be considered proven (unsound) and unverified
> > definitions (also unsound) which must be set up to verify new theorems
> > (a strict no-no in axiomatic systems.) There are also many nodes that
> > have no links or justification, such as ECOPRASS at
> > http://us.metamath.org/mpegif/ecoprass.html . What is the
> > justification for lines 23 and 24 (and the other lines labeled
> > "ecoprass")?
>
> Looks like hypotheses of the theorem to me.

What are the hypotheses to 2+2=4?

> > An axiomatic system is one that derives everything from a fixed set of
> > axioms and rules (and perhaps definitions.) After it is set up, (1)
> > you don't have to add anything to the system to develop a theorem, and
> > (2) only actual theorems can be constructed. (Agree?)
> >
> > Otherwise you have no more than a word processor with a Mathematical
> > font.
> >
> > C-B

You know, this is kind of like deja vue. All these people yelling and
screaming and I'm the one who (as is often the case) puts out the
formal definition to resolve technical issues - and they all go
running for the hills until time for the next skirmish.

What a life!

Quantcast