Re: What is a proof, exactly?

From: J.E. (troubled6man_at_yahoo.com)
Date: 11/23/04 

Date: 22 Nov 2004 19:45:23 -0800

Jasper Stein <J.J.Stein.Stein@cs.cs.ru.ru.nl.nl> wrote in message news:<cnsv56$aos$1@wnnews.sci.kun.nl>...

[snip]

> - Why could I not prove -say- that the set of natural numbers is as large
> as the set of reals? How does the falseness of this come into play? Why
> couldn't I prove -say- the generalised continuum hypothesis either, even
> though it isn't false in any sense? (or is it? why?)

Your first obstacle to such a proof, is a precise definition of "as
large as" and definitions of the naturals and the reals.

> - Does the extremely simple theorem "5=5" need a proof? Why (not)?

Yes, even more you need a definition of "5" "=" and a standard of
proof. Why? Because that's what proving things is all about. If you
define "x=y" as "Az (zex <=> zey)" then there IS a provable theorem
"Ax x=x", so then as long as "5" is a set (usually
{{},{{}},{{{}}},{{{{}}}},{{{{{}}}}}}) then "5=5" is a theorem too, the
proof of the more general theorem already covers when x happens to be
5 assuming you defined 5 to be a set.

> - How is a proof different from just an explanation? Is there a difference
> at all?

The usual standard is that a proof (of T relative to A) is a
demonstration that if T were false then A would be false too. So if
the assumption is "A", then "A" is a theorem, in the usual standard.
I'm assuming the is an ordinary first order logic system.
 
> - What is the status of "=" (equality) with respect to proofs? Is there a
> difference between "meaning of" and "definition of"? Is "=" defined or does
> it only have a (logical) meaning? Can we equate any two mathematical
> objects?

Honest people disagree on this issue. I prefer to define "=" as "x=y
<=> (Az (zex <=> zey))", the main rationale for having a different
status for "=" is that in general set theory axioms aren't enough, you
need rules for logic too, and some people like to have logical rules
for "=" as opposed to set theoretical rules for equality. The words
"meaning of" and "definition of" both "sound" like they could be
discussing the syntactic substitution that is what making a definition
is all about.

> - What does it mean to say that we have two different proofs of theorem T?

Is that even a meaningful concept? You could add a nonsequitor in the
middle of a proof and then it'd be syntactically different. The
strongest possible difference would be if one proof used a different
subset of axioms than another proof.

> - Suppose we defined an object X. Then we state a theorem Thm. about X,
> which we subsequently prove by a proof prf. According to the main school(s)
> of mathematics, what is the ontological status of X, Thm, and prf? Does Thm
> 'exist' in the same sense as X 'exists'? Does prf 'exist' in the same sense
> as Thm?

I'm not sure you meant this as written, just defining something
doesn't entail proving that it exists, so the ontological status of X
is undetermined at this point.
 
> - Once we defined X as above, we can make additional definitions Y, Z, ...
> depending on X. Can we also make definitions depending on Thm? On prf? Can
> you comment on the definition of the reciprocal ($x \to \frac{1}{x}$),
> which seems to depend not only on $x$ but also on a 'theorem' stating that
> $x \neq 0$? Does it also depend on a proof of such a theorem? How?

Yes you can make more definitions, definitions are just syntactic
shortcuts, it isn't actually DOING anything except making future
statements easier to read. For instance instead of saying "let x be a
natural number then T(x)" you could instead saying:
"Ax (
(Ar (xer or ~(
(Es (At ~tes) & ser) & (Au (uer => Ev (ver & Aw
(wev <=> (weu or (Ay (yew <=> yeu))))
)))
)))
& T(x))" and dispense with the "words" natural number, and the
corresponding definition "x is a natural number iff Ar (xer or ~((Es
(At ~tes) & ser) & (Au (uer => Ev (ver & Aw (wev <=> (weu or (Ay (yew
<=> yeu)))))))))" can you see how a definition is just a shorthand for
something mighty inconvient to write? A definition doesn't prove that
the thing defined exists, it is JUST a DEFINITION, it is JUST a
defintion of a SHORTHAND.
 
Theorems can be "used" in proofs, mostly by substituting the proof of
the theorem into a part of a new proof. As for the definition of the
reciprocal, I would consider the theorem "Ef Ax (xef <=> (Ay Az (zex &
yex) => (zeR & yeR & z*y = 1)))" it is the graph of the reciprocal
function, with that any term of the form 1/x can be replaced with
f(x). Of course, this assumed previous definitions of "xeR" and
"z*y=1", as well as the more fundamental function notation, if "a is
in the domain of the graph f" then we know that "Eb Ey (yef & (Az
(zey) <=> ((Ac cez <=> cea) or (At tez <=> ((Ad (det<=>dea)) or (Ag
(get<=>geb)))))))" we even mean that b is unique, this is a pain to
discuss definitions, because then I can't USE any talk to you, and
definitions make it easier to read what someone is writing so I'm not
sure if you can follow me, so I'm going to stop here, the point is
that there is a function f that takes each non-zero real to it's
reciprocal, so 1/x can be thought of as f(x) and checking that ~x=0 is
just like checking that a number is in the domain of a function and
then finding the value of the function.

> - The proof of the four colour theorem is controversial, since it depends
> on a piece of computer code. What is the problem with that?

IMO: There is an existing system of experienced human referees, I
think the controversy is that we don't have hard evidence that the OS
works as "expected" or that the source code is checking the theorems
cases properly, or that the compiler works as "expected" and even if
"someone" was sure they all did, that person (hypothetically) doesn't
have experience having made proofs that other mathematicians have
checked, so how would we know that they even understood the criteria.
I wouldn't trust a computer to count votes, for all the same reasons,
so why should I trust a proof by that is checked only by a computer?
 
> - This code calculated and checked a few thousands of 'configurations'. If
> these calculations and the checking were done by mathematicians, would the
> proof be still as controversial? Why (not)?

It's not one mathematician versus one computer, it's the fact that so
few independant minds would actually go through the bother of checking
it. It's just not as trustworthy, because it's been checked a smaller
number of both quality and independant times.
 
> - Suppose aliens gave us a pack of paper, full of english text and
> mathematical symbols, ending in "... and hence the Riemann Hypothesis is
> proved. QED." Suppose also that this text was so intricate and so involved
> and so convoluted that no one would be able to understand it in full. Does
> this pack of paper constitute a proof?

If we could understand the symbols, then we could make a machine (from
scratch) to check the proof. More likely I would expect that
mathematicians would prefer to make a machine that attempted to
*simplify* the proof. Then you can just read the simplier proof, a
much better case.

Relevant Pages

  • Re: infinity
    ... /uncountability/ of the reals means. ... Cantor theorem that the set of reals is uncountable! ... Of course, if you were to allow infinite naturals, you might ... But no mathematicians are the least bit interested in the number of ...
    (sci.math)
  • Re: Mathematicians are in deep shit for 2 reasons
    ... mathematicians usually concern just the naturals, sets of naturals, ... the reals, sets of reals, functions on reals, and so on -- essentially ... Not only did he delay republication of Was sind und was sollen die Zahlen? ...
    (sci.logic)
  • Re: Mathematicians are in deep shit for 2 reasons
    ... mathematicians usually concern just the naturals, sets of naturals, ... the reals, sets of reals, functions on reals, and so on -- essentially ... a given arbitrary structure exhibiting the relevant characteristics, ...
    (sci.logic)
  • Re: Platonism
    ... I said that they'd retreat to ZFC when pressed. ... To most mathematicians, there is something very ... The set of reals is not hard to construct in ZFC, ... that provide intuition, and better intuition is that which avoids ...
    (comp.theory)
  • Re: Platonism
    ... I said that they'd retreat to ZFC when pressed. ... To most mathematicians, there is something very ... The set of reals is not hard to construct in ZFC, ... that provide intuition, and better intuition is that which avoids ...
    (sci.math)