MathGroup Archive 2012

[Date Index] [Thread Index] [Author Index]

Search the Archive

Re: Command Possible?

  • To: mathgroup at smc.vnet.net
  • Subject: [mg127935] Re: Command Possible?
  • From: Ralph Dratman <ralph.dratman at gmail.com>
  • Date: Mon, 3 Sep 2012 02:56:09 -0400 (EDT)
  • Delivered-to: l-mathgroup@mail-archive0.wolfram.com
  • Delivered-to: l-mathgroup@wolfram.com
  • Delivered-to: mathgroup-newout@smc.vnet.net
  • Delivered-to: mathgroup-newsend@smc.vnet.net
  • References: <20120901062806.D256E6872@smc.vnet.net>

It always seems to me that everything depends on what sort of proof you
want. Mathematica doubtless knows how to classify the square root of a
non-square integer as irrational, but I very much doubt it uses anything
like the kind of logic people prefer to associate with elementary proofs of
important ideas.

Mathematica presumably takes advantage of a large number of accepted
theorems. So the proof that the square root of 2 is irrational would likely
amount to the use of a method which has, at some point in the past,
directly or indirectly, been proved to properly classify various kinds of
numbers as rational or irrational, as well as algebraic, transcendental,
algorithmic or whatever other categories might be relevant to a particular
task.

I have read that Russell and Whitehead's Principia Mathematica occupies
itself for a thousand pages to prove that 1+1=2 (see, eg.,
http://blog.plover.com/math/PM.html). Few people want to see a proof at
that level of detail. Published proofs rely on the Peano axioms and some
well-studied results to which they lead. Yet apparently it is not possible
to prove that the axioms are consistent. That does not represent any sort
of practical problem, but it supports the notion that in proving things,
you have to decide where to call a halt.

Doing so involves a set of aesthetic choices. You say you just want a
proof, but actually you are asking the computer (or rather, the programmer)
to produce a kind of artwork. The results are likely to disappoint.

Ralph Dratman



On Sat, Sep 1, 2012 at 2:28 AM, amzoti <amzoti at gmail.com> wrote:

> Hello,
>
> I have always been curious if Mathematica has ever considered a Prove
> command?
>
> The reason one could ask such is question is simple, who would have ever
> thought that CASs would get to where they are in such a relatively short
> period of time.
>
> Certainly, this is a tall order, but the richness we already see in
> Mathematica leads one to believe that this can be a new area for CAS
> development.
>
> Some easy examples could be Prove[ Sqrt[2], Irrational], Prove[ Exp[x],
> Transcendental], Prove[Sum[i, {i, 1, n}]== n(n+1)/2]...
>
> Certainly, there would be many limitations with proofs in some branches of
> Mathematics. I suppose getting to meatier proofs is problematic in itself,
> but maybe a certain rigor in defining the problem can be mapped out that
> follows how we set problems up today (as there is a pretty consistent way
> to specifying problems that most mathematicians adhere to).
>
> Anyway, why has this not been attempted (as a comparison, I have seen like
> DC Proof)? In the end, maybe it is just not a goal for a CAS.
>
> Thanks for your time.
>
>
>



  • Prev by Date: A new FrontEnd
  • Next by Date: Re: split the sublists into parts according to some rules
  • Previous by thread: Re: Command Possible?
  • Next by thread: Re: Command Possible?