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.