Re: What is a proof, exactly?
From: G. Frege (no_spam_at_aol.com)
Date: 11/30/04
- Next message: David C. Ullrich: "Re: Uncountable many reals without Cantor"
- Previous message: Ron Peterson: "Re: logic is innate?"
- In reply to: Jasper Stein: "Re: What is a proof, exactly?"
- Next in thread: Josh Purinton: "Re: What is a proof, exactly?"
- Reply: Josh Purinton: "Re: What is a proof, exactly?"
- Messages sorted by: [ date ] [ thread ]
Date: Tue, 30 Nov 2004 16:40:53 +0100
On Tue, 30 Nov 2004 16:27:05 +0000, Jasper Stein
<J.J.Stein.Stein@cs.cs.ru.ru.nl.nl> wrote:
> Josh Purinton wrote:
>
> > In article <4765002.0411221804.9c639dc@posting.google.com>,
> > Acid Pooh <poopdeville@gmail.com> wrote:
> > > Ideally, a proof is a finite sequence of sentences in a (formal)
> > > language with rules of inference such that if A_i is a sentence, it
> > > "follows" from some sentences A_j, ... A_k with j ... k<i or is an
> > > axiom in the language. [...] Now, granting that most of mathematics
> > > can be formalized in ZFC, *formal proofs* of any but the most trivial
> > > facts, in, say, group theory, are unimaginably long.
> > >
> > This need not be the case.
> >
> > In Norm Megill's formalization of set theory in Metamath, a formal proof
> > of the irrationality of sqrt(2)
> > <http://us.metamath.org/mpegif/sqr2irr.html> takes just 42 steps.
> >
> Hm? This proof seems to depend on a number of lemmas, too.
>
> So a full proof is a lot longer indeed, and Acid Pooh's remark stands.
>
Agree. If we "expand" all the lemmas (to get a proof with "atomic"
steps), this proof will be rather long (m u c h longer than just 42
steps. ;-)
Compare with the following:
2 + 2 = 4 Trivia
~~~~~~~~~~~~~~~~~
The complete proof of a theorem all the way back to axioms can be
thought of as a tree of subtheorems, with the steps in each proof
branching back to earlier subtheorems, until axioms are ultimately
reached at the tips of the branches. An interesting exercise is,
starting from a theorem, to try to find the longest path back to an
axiom. Trivia Question: What is the longest path for the theorem 2 + 2 =
4?
Trivia Answer: The longest path back to an axiom from 2 + 2 = 4 is 127
levels deep! By following it you will encounter a broad range of
interesting and important set theory results along the way. You can
follow them by drilling down this path. Or you can start at the bottom
and work your way up, watching mathematics unfold from its axioms.
2p2e4 (2+2=4) <- 2cn <- 2re <- addrcl <- axaddrcl <- addresr <- 0idsr <-
addsrpr <- enrer <- addcanpr <- ltapr <- ltaprlem <- ltexpri <-
ltexprlem7 <- ltaddpr <- addclpr <- addclprlem2 <- addclprlem1 <- ltrpq
<- recclpq <- recidpq <- recmulpq <- mulcompq <- dmmulpq <- mulclpq <-
mulpipq <- enqex <- niex <- omex <- zfinf <- inf4 <- inf3 <- inf3lem7 <-
inf3lem6 <- inf3lem5 <- inf3lem4 <- inf3lem3 <- inf3lem2 <- inf3lemd <-
inf3lemc <- frsuc <- rdgsuct <- rdgsuc <- rdgfnon <- tfr1 <- tfrlem13 <-
tfrlem12 <- tfrlem11 <- tfrlem9 <- tfrlem7 <- tfrlem5 <- tfrlem2 <-
tfrlem1 <- tfis2 <- tfis2f <- tfis <- tfi <- onsst <- ordsson <-
ordeleqon <- onprc <- ordon <- ordtri3or <- ordsseleq <- ordelssne <-
tz7.7 <- tz7.5 <- wefrc <- epfrc <- epel <- epelc <- brab <- brabg <-
opelopabg <- opabid <- opex <- prex <- zfpair <- 0inp0 <- 0nep0 <- snnz
<- snid <- snidb <- snidg <- elsncg <- dfsn2 <- unidm <- uneqri <- elun
<- elab2g <- elabg <- elabgf <- vtoclgf <- hbeleq <- hbel <- hbeq <-
hblem <- eleq1 <- cleq2 <- cleq1 <- birbid <- bilbid <- birimd <- bilimd
<- pm5.74d <- pm5.74 <- im2and <- prth <- imp4b <- imp4a <- impexp <-
birim <- impbi <- bi3 <- expi <- expt <- pm3.2im <- con2d <- con2 <-
nega <- pm2.18 <- pm2.43i <- pm2.43 <- pm2.27 <- com12 <- syl <- a1i <-
ax-1
The list above was produced by typing the commands "read set.mm" then
"show trace_back 2p2e4 /essential /count_steps" in the Metamath program.
| By the way, the complete proof of 2 + 2 = 4 involves 1,957 subtheorems
| including these. (The command "show trace_back 2p2e4 /essential" will
| list them.) These have a total of 20,726 steps — this is how many steps
| you would have to examine if you wanted to verify the proof in complete
| detail all the way back to the axioms.
-----------------------------------------
Source:
http://us.metamath.org/mpegif/mmset.html#trivia
Even for the complete proof of 2 + 2 = 4 we already need
a total of 20,726 steps (!)
F.
- Next message: David C. Ullrich: "Re: Uncountable many reals without Cantor"
- Previous message: Ron Peterson: "Re: logic is innate?"
- In reply to: Jasper Stein: "Re: What is a proof, exactly?"
- Next in thread: Josh Purinton: "Re: What is a proof, exactly?"
- Reply: Josh Purinton: "Re: What is a proof, exactly?"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|
