Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?

From: Daryl McCullough (daryl_at_atc-nycorp.com)
Date: 01/11/05 

Date: 11 Jan 2005 08:15:28 -0800

Tim Chow (tchow@lsa.umich.edu) says...
>
>In article <crv0bo$ij7$1@ra.nrl.navy.mil>,
>Ralph Hartley <hartley@aic.nrl.navy.mil> wrote:
>>That isn't the point. Let "A" be the effective procedure used by
>>mathematicians (individually or collectively, just be consistent) to
>>determine mathematical truth.
>
>*Now* this is closer to the point! Who says that mathematicians use an
>effective procedure to determine mathematical truth? You might believe
>that this is true, but this is not a theorem of anyone, and it is also
>not the Church-Turing thesis. Hence even the undecidability of the halting
>problem, together with the Church-Turing thesis, does not entail the
>existence of permanently unknowable truths. You need the dubious assumption
>that mathematicians use an effective procedure to determine mathematical
>truth.

There are two aspects of mathematical research: (1) investigation and
exploration, and (2) codification of the results of that investigation. There
doesn't seem to be anything mechanical or formal about the first type of
activity---who knows where mathematicians get their inspiration for what to
investigate, or inspiration for how to approach proving something? However, once
this unformalizable investigative work is finished, mathematicians clean up the
result, simplify it, polish it, create illustrative examples, formulate helpful
definitions, prove helpful lemmas, generalize it, etc.

The slick finished product, created years after the initial groundbreaking
investigative work, is something that is straight-forward enough for a graduate
student or bright undergrad to understand. It doesn't at all seem implausible to
me that one day we could write a grad-student-level AI program that was capable
of reading textbook quality proofs and see that they are almost certainly
correct. Creating such proofs in the first place is perhaps too hard, in the
same way it is too hard for most grad students.

However, from the point of view of what is in principle possible (as opposed to
in practice), the ability to recognize solid mathematics is as good as the
ability to create it: You just enumerate all possible character strings, and for
each one, you check to see if it is a solid mathematical argument.

That makes me think that the set of possible truths recognizable to
mathematicians is indeed r.e. Mathematicians may make wild leaps in discovering
their mathematical truth, but for their discoveries to be accepted, they have to
be polishable to something that is recognizable as a mathematical proof.

Relevant Pages

  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... mathematicians use an effective procedure to determine mathematical truth. ... But how did we come to accept the axiom of choice? ...
    (comp.theory)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... mathematicians use an effective procedure to determine mathematical truth. ... But how did we come to accept the axiom of choice? ...
    (sci.math)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... mathematicians use an effective procedure to determine mathematical truth. ... But how did we come to accept the axiom of choice? ...
    (sci.logic)
  • Re: Well Ordering the Reals
    ... this boils down to the question of the truth of the axioms. ... I don't have any philosophical thesis to offer about the nature of mathematical truth or existence, but I feel that any proposed thesis should be compatible with what mathematicians actually do and say - or put in another way, I have much more faith in e.g. set theory than in the philosophical ideas about the nature of mathematical truth I've encountered this far. ... Accepting that ZFC has models seems to me rather pointless. ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... >>determine mathematical truth. ... >that mathematicians use an effective procedure to determine mathematical ... this unformalizable investigative work is finished, ...
    (sci.math)
Quantcast