how do you prove theorems about Lisp code?

[gusl]

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:

(defun select (test lst)
(cond ((null lst) nil)
((funcall test (car lst)) (cons (car lst) (select test (cdr lst))))
(T (select test (cdr lst)))))

(defun make-set (m n)
(if (= n m) (list m)
(cons n (make-set m (- n 1)))))

(defun dividesp (d n)
(eq (mod n d) 0))

(defun n-divisors (n)
(length (select #'(lambda (x) (dividesp x n)) (make-set 1 n))))

(defun perfect-square-p (n)
(eq n (expt (floor (sqrt n)) 2)))

(defun implies (phi psi)
(or psi (not phi)))

(defun forall (col test)
(cond ((null col) T)
((funcall (car col) test) (forall (cdr col) test))
(T nil)))