
From:  William Sit 
Subject:  Re: [Axiomdeveloper] Proving Axiom Correct 
Date:  Fri, 6 Apr 2018 17:48:29 +0000 
Dear Tim:
I never said, nor implied you are wasting your time.
If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theoremproving while I prefer to trust Axiom code and not so much on theoremproving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theoremproving (including rewriting systems, typetheory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory, model theory, number theory, geometries, etc.).
My reason for not so much trusting theoremproving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "handwaving", which in my opinion, does not necessarily mean nonrigorous. Mathematicians frequently use "handwaving" for results or methods or processes that are wellknown (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.
Believe it or not, theoremproving use the same language and "handwaving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf
There is one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):
"Famously, several hundred pages of PM precede
the proof of the validity of the proposition 1+1=2."
Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):
"PM was an attempt to describe a set of axioms and inference
rules in symbolic
logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history
of mathematics and philosophy,^{[1]} being
one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's
incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any
set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them." "The Principia covered only set theory, cardinal numbers, ordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.
A fourth volume on the foundations of geometry had
been planned, but the authors admitted to intellectual exhaustion upon completion of the third."
Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. Nonetheless, even computers have their limits.
That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's
incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.
William
William Sit
Professor Emeritus Department of Mathematics The City College of The City University of New York New York, NY 10031
homepage: wsit.ccny.cuny.edu
From: Tim Daly <address@hidden>
Sent: Friday, April 6, 2018 6:34 AM To: William Sit Cc: axiomdev; Tim Daly Subject: Re: [Axiomdeveloper] Proving Axiom Correct One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion. Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers. My point of view is that writing Spad code that way is "preproof,
19th century 'handwaving' mathematics". We can do better.
On Fri, Apr 6, 2018 at 1:23 AM, William Sit
<address@hidden> wrote:

[Prev in Thread]  Current Thread  [Next in Thread] 