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 ]
 Marshall Posts: 1,936 Registered: 8/9/06
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 5:50 PM

On Jun 21, 12:34 pm, Andrew Tomazos <and...@tomazos.com> wrote:
> 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

Ignoring whitespace (which you should) the difference
between yours and Jan's form is the difference between:

A ; B ; C ; D ;

and

A & B & C & D

The difference is in the choice of conjunction character and
in whether it is a separator or terminator. These differences
are really, really trivial.

The surest sign of a language design noob is a focus on syntax.

Marshall

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