Home
Gustavo Lacerda

> recent entries
> calendar
> friends
> My Website
> profile

Thursday, May 12th, 2005
10:04p - Trying to do science without mathematics is analogous to Greenspun's 10th law

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.

(comment on this)

10:49p - how do you prove theorems about Lisp code?
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... )

(14 comments |comment on this)

<< previous day [calendar] next day >>
> top of page
LiveJournal.com