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.
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.
[natnum]s are read and written using any number of digitsor.
749321 6 0 293 128328287193289487593485992843579238749579459
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) )
(|type| {natnum] |subtype| [base-type]
(|def|
(|recognizer| #'NATNUM)
)
)
FOL contexts make a clear distinction between use and mention. Things in the the language of a context are symbols (mention) and things in the simulation structures may be any objects (use). The language might contain numbeals that 'name' numbers.
FOL context are finite objects. Not all natural numbers can be 'in' a context. On the other hand, explicit declarations for some particular set of natural numbers either declares unnecessary individual constants or leaves out just the one you need.
The speech act interpreter used by our thinker solves this dilemma by using the same pun used by human listeners. When it reads/hears a sequence of digits it decides to interpret as a natural number it creates a muneral for that number,declares it to be an individual constant of the current context and attaches it to the appropriate number in such a way that if it decides to mention that number the numeral created is used.
For example reading
(= x 42758)
creates a numeral '42758' and declares it an individual constant in the current context and attaches it to the number 42758. It was not necessary that the system 'understand' 42758 before it read this (but if it did it adopts the preexisting data). This might be the only number it knows about.
If it decides to mention the number, for example, it prints/saya
Yes, the value of x is 42758.
it uses the ambigeuos pun to mention the number. This means that when using a numeral consisting of digits to mention the number, it just uses that sequence of digits.
(|type| [integer] |subtype [natnum]
(|sign| {+ -})
(|size| [natnum])
)