
Re: Formal Proof Language Example  HumanReadable?
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 100times > 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 Truthpreseving 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.

