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.
But as I said, your heading is formal proof language, and 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...