Re: What is a proof, exactly?

From: Barb Knox (see_at_sig.below)
Date: 11/23/04 

Date: Tue, 23 Nov 2004 16:49:12 +1300

In article <cnsvv3$b6d$1@wnnews.sci.kun.nl>,
 Jasper Stein <J.J.Stein.Stein@cs.cs.ru.ru.nl.nl> wrote:

>Dear mathematicians,
>
>For my Ph.D. work in automated reasoning I am investigating formalised
>linear algebra. In automated reasoning one tries to capture mathematical
>definitions, theorems as well as mathematical reasoning in (computerised)
>formal systems, notably type theories.
>
>However, due to several technical difficulties formalising linear algebra I
>have begun wondering what exactly it means to have a proof of a theorem. I
>hope to have answers to this question from a number of mathematicians
>unspoilt by the automated reasoning community. Could you please comment on
>this main question ("what is a proof?")?

I'm curious as to what sort of spoilage happens to those who hang around the
A-R community. I presume that you (and they) have had exposure to at least
one mathematical logic or axiomatic set theory class at some point.

If this presumption is correct, then how could they not know what a proof is
in mathematical terms? Especially since the whole point of A-R is to
compute some conclusions from some premises using some more-or-less
well-defined rules, which is pretty-much what proofs are about too. Maybe
the snag is that in A-R the "more-or-less" is often more less than more.

>There are a number of related questions that may be worth taking into
>account as well, such as:
[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?

If the set theory you are working with is consistent (a.k.a "sound") then no
proof ever derives a contradiction. Since it has already been proven that
|N| < |R|, then if the set theory is consistent then there can not also be a
proof for either |N| = |R| or |N| > |R|.

Note that for the established popular set theories (ZFC, NFU, NBG, etc.)
there is plenty of empirical evidence that they are consistent, but
consistency has not been mathematically proven.

AIUI, some A-R systems do not guarantee consistency, and some don't even
consider it to be a virtue, so in those systems you can indeed derive both A
and ~A,

>Why
>couldn't I prove -say- the generalised continuum hypothesis either, even
>though it isn't false in any sense? (or is it? why?)

Because there is a proof in (say) ZFC (which you might usefully consider to
be a meta-proof) that the GCH is "independent" of ZFC. That means that
there is a ZFC (meta-)proof that there is no ZFC proof of GCH.

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

"Need" presupposes some purpose. If an A-R system is asked about "5=5" then
it presumably does a 1-step derivation from some pattern/rule like "For all
x, x=x". That 1-step derivation can be considered to be a 1-step proof.

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

A proof is a certain kind of explanation.

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

A proof is done in some "logical system" plus some "axioms". One popular
logical system is "first-order logic with equality" in which the meaning of
"=" is built in to the logic. But any such proof can be recast into
"first-order logic without equality", in which "=" is defined via axioms in
the same manner as any other predicate, viz:
    Ax x=x
    Ax Ay x=y -> y=x
    Ax Ay Ax x=y ^ y=z -> x=z
    (plus some axioms(s) allowing substitution of equals for equals).

>Can we equate any two mathematical objects?

You can have a predicate "=" that is defined for any pair of objects, which
can be used to test if a=b. And you can take any two objects and assert
that that are indeed equal (by asserting a=b). Does this capture the sense
of the verb "equate" that you have in mind?
[SNIP]

BTW, that's an interesting montage Radboud U has (at <http://www.ru.nl>) --
it looks like the guy is holding a retort containing a floating eyeball
wearing a coat and tie: "It's alive!! And it's even well-dressed!" 

-- 
---------------------------
|  BBB                b    \     Barbara at LivingHistory stop co stop uk
|  B  B   aa     rrr  b     |
|  BBB   a  a   r     bbb   |    Quidquid latine dictum sit,
|  B  B  a  a   r     b  b  |    altum viditur.
|  BBB    aa a  r     bbb   |   
-----------------------------

Relevant Pages