Numbers

The notion and definitions of number has a long history. IBUKI Data includes the capability to compute on numbers and this document describes how both the theory of numbers can be developed using IBML, how reasoning about numbers can be acomplished in FOL systems and we do numericsal computations using SEUS and how to reason about these computations again using FOL contexts.

The development of numbers given here follows the usual path followed by mathematicians but reformalized using IBML. This will illustrate how the development of numbers in set theory results in a formalization that does not reflect the actual constructions used in mathematics and why the information theoretic semantics of IBUKI types provides a reasonable alternative.

The difference is stark. In set theory the natural numbers are a subset of the rationals. In IBML the type [rational] is a subtype of [natnum]. How this works is described below.

Natural Numbers

As usually imagined the whole numbers 0, 1, ... are called by mathematicians the narural numbers. They are generally imagined to be understood by everyone. We call the type of an object that is a natural number a [natnum]. We say that an object, obj, is (an example of) a [natnum] if it is a whole number.

[integer]s can have any number of digits and their arithmetic is defined in the usual way by the axioms od peano arithmetic.

Writing/Speaking about [natnum]s

[natnum]s are read and written using any number of digitsor.

749321
6
0
293
128328287193289487593485992843579238749579459

The Axioms of Natural Number Arithmetic

The following is a conversation we might have with our thinker (who we call FRED) about the arithmetic of natural numbers using the peano/robinson axioms.

;; What we want to say In informal English this might sound like
;;   Let's focus our attention on a new context called Natnum.
;;   Note: The English as written confuses the use and mention
;;     of the word 'Natnum'. If we were more pedantic we might write
;;     "Let's focus our attention on a new context called 'Natnum'."
;;   but informal spoken English lacks punctionation and without
;;     circumlocution lacks the ability to make this distinction.
;;
;; Our technical solution is to change FREDs internal state as follows
;; In Meta (in FRED)
;;   declare the [indconst] Natnum of type [context]  AND
;;   attach it to the empty context
;; In the mind of FRED
;;   make the attachment to Natnum the current context
;; We 'accomplish' this be saying to FRED
(CALL-CURRENT-CONTEXT Natnum)

;; This is a technical detail. It causes FREDs reader to correctly understand
;; the usual expressions for natural numbers and amkes all of the appropriate
;; adjustments. See [SPEAKING-AND-TALKING]
;;
;; this command also 
;;   declares the [sortsym] NATNUM?
;;   declares the [indconst] #'NATNUM?, which names its recognizer
;;   attaches the program nATNUM? to #'natnum?
;;   declares the [indconst] [natnum], which names the type [natnum]
;;   [natnumrep]
(PARSE [natnum]) 

;; In 'the head'
;; define the language of the context Natnum
;;   this means 'update the context called Natnum in Meta'
;;   it also has the consequence of updating the current context
(DECLARE Indvar n m p q [natnum])
(DECLARE Funconst suc pred ([natnum] [natnum]))
(DECLARE Funconst + * ([natnum] [antnum] [natnum]))
(DECLARE Predconst < 2)
(DECLARE Predpar P 1)

;; add facts
(AXIOM ONEONE (FORALL (n m) (IMP (EQUAL (suc n) (suc m)) (EQUAL n m))) )
(AXIOM SUCC1 (FORALL (n) (NOT (EQUAL 0 (suc n)))) )
(AXIOM SUCC2 (FORALL (n)
  (IMP (NOT (EQUAL 0 n) (EXISTS (m) (EQUAL n (suc m)))))) )
(DEFINE PLUS
  (FORALL (n)   (EQUAL (+ n 0) n))
  (FORALL (n m) (EQUAL (+ n (suc m)) (suc (+ n m)))) )
(DEFIND TIMES	forall n . n * 0 = 0,
  (FORALL (n)   (EQUAL (* n 0) 0))
  (FORALL (n m) (EQUAL (* n (suc m)) (*bsuc (+ n m)))) )
		forall n m . n * suc(m) = (m*n) + m;
(AXIOM INDUCTION
  (IMPLIES 
    (AND (P 0) (FORALL n (IMPLIES (P n) (P (suc n)))))
    (FORALL (n) (P n)) ) )

;; build the simulation structure
(ATTACH suc ([natnumrep] [natnumrep]) #'ADD1)
(ATTACH pred ([natnumrep] [natnumrep]) #'SUB1)
(ATTACH + ([natnumrep] [natnumrep] [natnumrep]) #'PLUS)
(ATTACH * ([natnumrep] [natnumrep] [natnumrep]) #'TIMES)
(ATTACH < ([natnumrep] [natnumrep]) #'LT)

After this (among other things) the system will be able to simplify ground terms of the language.

(SIMPLIFY (< (+ 2 3) (pred 7))
(SIMPLIFY (< (+ (* 4 (suc 2)) (pred 3)) (pred (pred 8))) )
(sIMPLIFY (< (* n 0) 3) )

Integers Numbers

(|type| [integer] |subtype [natnum]
 (|sign| {+ -})
 (|size| [natnum])
)

Rationals

(|type| [retional]
 (|sign| {+ -})
 (|num| [natnum])
 (|den| [natnum])
)

Notes about Real Numbers ...