Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

 Messages: [ Previous | Next ]
 Andrew Tomazos Posts: 137 Registered: 8/1/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 3:34 PM

On Jun 21, 9:11 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> For example your theorem could also be formalize as follows:
>
>      forall a, b, c in nat
>         (a^2 + b^2 = c^2 &
>          rel_prim(a,b) &
>          odd(a) => exists m, n in nat
>           (m<=n &
>            a = n^2 - m^2 &
>            b = 2*m*n &
>            c = n^2 + m^2))
>
> And I think this is better than distributing conjuncts
> over C like statements separated by semicolon ";". First
> of all because this language has already been 100-times
> formally introduces in logic books.

Are you sure the way you have written it is really clearer?

When you think about it - if I state that a series of propositions:

A
B
C
D

are individually true in some context, than it is exactly the same as
saying:

A and B and C and D

This also mirrors the way that (what I suspect to be) at the core of
every proof:

Axiom A
A'
A''
A'''
Theorem X

ie Truth-preseving transformations of an axiom(s) to a theorem.

..is identical on some level to:

Axiom A and A' and A'' and A''' and Thereom X

Also the way you have indented and spaced out the theorem doesn't seem
to follow any logical pattern. It is almost like you have written it
on one line and randomly inserted carriage returns.

The way I formatted it was deliberate, to indicate the relevant scope
connections and compound statements. This is an important
consideration when complexity increases.
-Andrew.

Date Subject Author
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/24/09 Andrew Tomazos
6/25/09 MeAmI.org
6/25/09 Jan Burse
6/26/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Joshua Cranmer
6/27/09 Andrew Tomazos
6/21/09 Marshall
6/21/09 Spiros Bousbouras
6/24/09 Tim Smith
6/21/09 Charlie-Boo
6/21/09 William Elliot
6/22/09 MeAmI.org
6/22/09 MeAmI.org
6/23/09 Slawomir
6/24/09 David Bernier
6/24/09 MeAmI.org
6/24/09 MeAmI.org
6/24/09 Andrew Tomazos
6/24/09 Andrew Tomazos
6/25/09 Slawomir