May. 12th, 2005

gusl: (Default)

Greenspun's tenth law of programming: Any sufficiently complicated C or Fortran program contains an ad-hoc, informally-specified, bug-ridden, slow implementation of half of CommonLisp.

Trying to do science without mathematics is analogous. When Hartry Field tries to formulate science in terms of nominalistic theories (he wanted to demonstrate that one can do science without referring to abstract entities), those theories can't avoid using abstractions (e.g. you could encode PA in terms of his space-points).

Number theory, like Lisp, is a sort of universal structure, just waiting to be discovered. See Minsky - "Alien Intelligence" (search for "A REAL LIFE EPISODE")

It's possible to do science without mathematics, but you might as well develop mathematics on the way.
gusl: (Default)
It's impossible to prove Pi_1 statements without axioms that talk about infinity.

If it were possible, I would like to do it right now with Lisp. I have implemented a refuter for general Pi_1 statements, but even though implementing a verifier would never be successful, I still firmly believe in some proofs of Pi_1 statements. That means that I must implicitly accept axioms about infinity, much as I'd like not to.

Here's a nice theorem:
;;;All numbers with an odd number of divisors are perfect squares:
(forall #'(lambda (n) (implies (not (perfect-square-p n)) (evenp (n-divisors n)))))

And here's a nice proof:

(Lemma 1) Forall n in N, n is a perfect square IFF its prime factorization has an even power at all the primes.
(Lemma 2) Forall n in N, n-divisors(n) = PRODUCT (power(p_i,n) + 1) for each prime p_i in the factorization of n

Suppose n is not a perfect square (1)
Then there is a prime p in the prime factorization of n such that its power is odd. (by 1, L1)(2)
Since power(p,n) is odd, then power(p,n) + 1 is even. (3)
Then n-divisors(n) is even. (by 3, L2) (4)

But which axioms am I using in this proof? Are they too hard to dig out of the lemmas? My justification for the lemmas is my visual intuitions. Somewhere in proving them in any kind of system, you would need an axiom about infinity, right?

in case you want the rest of the Lisp code:
Read more... )


gusl: (Default)

December 2016

18 192021222324

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags