![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslIt'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:
And here's a nice proof:
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)))
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)))
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
Termination
Date: 2005-05-12 08:33 pm (UTC)What makes you think your Lisp code terminates on all inputs?
Re: Termination
Date: 2005-05-12 08:41 pm (UTC)The refuter obviously doesn't terminate when you give it a true statement.
Induction
Date: 2005-05-12 08:47 pm (UTC)Oops. I misunderstood the purpose of your code.
Your proof relies on induction somewhere, I promise.
Re: Induction
Date: 2005-05-12 08:51 pm (UTC)Re: Induction
Date: 2005-05-13 07:30 am (UTC)I would more or less agree with that. There are a few things that you can do without induction. If the number of cases you have to check is bounded by fixed number independent of the input, then you don’t need induction. (Think of induction as a for loop.) However, whether you formally use an induction axiom or not depends on the system you are using. Some systems will require to you use induction to prove ∀n. n = 0 ∨ ∃m. n = Sm even thought I don’t think this fundamentally requires induction.
Re: Induction
Date: 2005-05-13 11:38 am (UTC)How would you prove this without induction?
Re: Induction
Date: 2005-05-13 01:24 pm (UTC)In Coq (http://coq.inria.fr/) the proof is:
OorS = fun n : nat => match n as n0 return (n0 = 0 ∨ (∃m : nat, n0 = S m)) with | O => or_introl (∃m : nat, 0 = S m) (refl_equal 0) | S n0 => or_intror (S n0 = 0) (ex_intro (fun m : nat => S n0 = S m) n0 (refl_equal (S n0))) end : ∀n : nat, n = 0 ∨ (∃m : nat, n = S m)The proof basically does a pattern match on the natural number n, and creates a proof in either of the two possible patterns. There is no recursion (aka induction).
Re: Induction
Date: 2005-05-13 01:28 pm (UTC)Btw, did you get an email at your roconnor.international* account?
Re: Induction
Date: 2005-05-13 01:41 pm (UTC)Are "∀" and "∃" really part of Coq syntax, or is it "forall" and "exists"? Having said that, labels like "(refl_equal 0)"
Should I parse "or_introl (∃m : nat, 0 = S m) (refl_equal 0)" as
PROOF :: [CLAIM] [JUSTIFICATION] ? I can't really make head or tails of this syntax, even though I remember being able to do a lot of stuff with the proof assistant only a few months ago.
Btw, I've credited you in a philosophy of math presentation.
Re: Induction
Date: 2005-05-13 05:13 pm (UTC)No. They are the constructors for the disjunction and existential types. They correspond to introduction rules in natural deduction.
There is a common module that you can load that give you utf-8 notations for
forall,exists, etc.refl_equal ais the proof thata = a.No. The first two arguments to
or_introlare the types of the left and right disjuncts; however the first type is implicit, and doesn’t appear. The last argument is the proof of the first (implicit) type. In this case it isrefl_equal 0 : 0 = 0.Sorry for the confusing syntax. My point was that induction isn’t used in the proof which you can more or less see by the fact that
fixpointdoesn’t appear in the term.I doubt very much that my philosophy of math is original, but thanks!
Re: Induction
Date: 2005-05-13 05:33 pm (UTC)I actually quoted your statement of Gödel's 1st Incompleteness Theorem in Coq in order to refute the ridiculous claim that such a proof couldn't be formalized. I wonder if Penrose would go that far.
Re: Induction
Date: 2005-05-13 06:01 pm (UTC)Still Shankar formalized Incompleteness theorem in 1986. The second incompleteness theorem has yet to be done.
(no subject)
Date: 2005-05-13 02:02 pm (UTC)(evenp (euler-phi n))))
N)
(defun make-set (start end)
(loop for x from start to end collect x))
(defun euler-phi (n)
(length (remove-if-not (lambda (x) (dividesp x n))
(make-set 1 n))))
(defun perfect-square-p (n)
(= n (expt (floor (sqrt n)) 2)))