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 ]
 Jan Burse Posts: 1,472 Registered: 4/12/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 3:11 PM

Andrew Tomazos schrieb:
> On Jun 21, 8:46 pm, Jan Burse <janbu...@fastmail.fm> wrote:
>>> Please consider the following formal proof language example:
>>> [Snip] Euclid's primitive pythagorean triple theorem [Snip]

>> This is not a formal proof example, since
>> the important part, the proof, is left out.

>
> My question was about the language of the "theorem statement". Do you
> consider it both human and machine readable?
> -Andrew.

But this is not a challenge. Since your theorem comes from
algebra. And even in undergraduate notation for algebra is
learnt. The only difference in your example is, that there
is some sugar for implication and quantifiers.

a formal proof language is more than only a language for
theorem statements. The problem is that for proofs there
are more choices than for theorem statements.

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.

I maybe would only start using semicolon in proof figures.
You know formulas as above are part of proof figures.
If I remember well, some of the original papers of
Gentzen gives a nice introduction what structure a proof
figure has...

So Gentzen is one person to keep in mind. The other person
would be Knuth, the inventor of Tex. I think he was once
even proving that 2-dimensional things can be expressed
in a sequential and thus 1-dimensional language...

Bye

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