Re: need help in understanding Torkel's ZFC comment

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

Date: 3 Dec 2004 09:34:21 -0800

Josh Purinton <usenet-noreply.a.jp@xoxy.net> wrote

> Summary of the discussion so far:
> Frege> http://au.metamath.org/mpegif/2p2e4.html
> Charlie-Boo> [6-line informal proof of 0'' + 0'' = 0'''']
> Charlie-Boo> I beat him by 19,725 steps.
> 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")?

If you want to argue that certain rules "don't count", that is not
productive – the fact remains that each branch of Mathematics has its
own axioms. The assertion that everything comes from ZFC is a lie and
I would love to hear all sorts of professors claim that it is so.

MetaMath derives almost nothing from any axioms. It uses a number of
subterfuges to allow you to declare arbitrary expressions (even
meaningless sequences of symbols) to be theorems.

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

> > Do you have any idea how the theorem was produced? How the proof was
> > produced? To what extent and how it was verified?
>
> Do you? It's only been explained to you two or three times by now.
> For the questions you ask, the web site really does
> explain it in detail.

Ok, then what are the possible justifications for the terminal nodes
in a proof tree?

Relevant Pages