weemba@garnet.berkeley.edu (Obnoxious Math Grad Student) (09/10/88)
In article <918@l.cc.purdue.edu>, cik@l.cc (Herman Rubin) writes: >However, starting with a set of axioms and no rules, nothing more can be >derived. Thus we see that rules are stronger than axioms. Indeed. One can always have a rule that says ( () => axiom ). Deep, no? ucbvax!garnet!weemba Matthew P Wiener/Brahms Gang/Berkeley CA 94720
jbn@glacier.STANFORD.EDU (John B. Nagle) (09/10/88)
In theorem proving, previously proved theorems are often used, correctly,
as rewrite rules. Free addition of new "axioms" to theorem proving systems
generally results in unsoundness. As Boyer and Moore once wrote, "It is
one thing to use axioms about a concept known to mathematics for
a century. It is quite another to write down axioms about an idea
invented yesterday." See Boyer and Moore's "A Computational Logic"
for the constructivist's way of avoiding this problem.
Attempts to use the theorem proving paradigm in less formal domains
were made in the late 70s and early 80s, but without notable success.
John Nagle