
Our goal is to build an artifact that can think. A more concreat question is: what is i the head of our thinker. I particiular what does it think of nombers.. This essay revisits the discussion of over a century about the nature of the natural numbers numbers and proposes a new vision of what is actually i the head of an artifact that can think about numbers.
The computable ancestral
(FORALL obj
(IMPLIES
(AND (HOST-NATNUM? obj) (NOT (EQUAL obj Host-Natnum-Zero)))
(RXIST (h [host-natnum]) (HOST-NATNUM-PRED h obl)) ) )
If (NATUM-REP? obj) (ATTACHED n obj) (E
(deflam pred*-aux (n l)
(IF (EQUAL n 0)
(list-cons l 0)
(list-cons (pred*-aux (pred n) l) n) ) )
Theorem:
1)
(pred* n m)
(forall (n [umeral])
(EQUAL (least-ancestral n) 0) )
The Skolem view of iductio
(forall (n [numeral])
(IMPLIES
(AND
(A (a-mak-umeral 0)))
(forall (m [nueral]) (IMPLIES AND (less-than m n) (A m)) (A (succ m)))
(A n) ) )
(IMPLIES (LIST? l) (
Bibliography