Re: need help in understanding Torkel's ZFC comment

From: Chairman of the David Hilbert Appreciation Society (mathgeekxxiiii_at_hotmail.com)
Date: 12/04/04 

Date: Fri, 03 Dec 2004 19:19:36 -0500

Charlie-Boo wrote:
> 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")?

Looks like hypotheses of the theorem to me.

> 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? 

-- 
Replace Roman numerals with digits to reply by email

Relevant Pages