HOME

NEWFOL: Arithmetic

Version 0.001 2024-07-01

Author:

Richard Weyhrauch (IBUKI)

Note:

This is one of the many original personal document of Richard Weyhrauch hosted by IBUKI at http://rww.ibuki.com . This document is not in the public domain. The copyright is held by him and anyone wanting to reprint it must get his permission in writing. This document was written while he was employed by IBUKI but on his own time at at his own expense.

Numbers

The notion and definitions of number has a long history. The three kind of numbers that are always supported by IBUKI Data are [rational], [integer] and [natnum]. This document describes [arith], a NEWFOL [context] that nderstands arithmetic. Rather than being the theorertically 'cleanest' formalization of arithmetic it is designed to provide an agent with the ability count things and compute with numbers rather than explain how numbers 'work'.

[arith] also shows how both the theory of numbers can be developed and how problem solving about numbers can be done using NEWFOL.

The development of numbers given here follows the usual path followed by mathematicians but reformalized using a NEWFOL [context]. This shows that we do not need set theory to understand numbers. [arith] embodies the actual constructions used in mathematics and illustrates how the information theoretic semantics of NEWFOL provides a reasonable alternative to set theory.

The difference is stark. In set theory the natural numbers are an infinite set and requires the uncomputable membership relation (usually written ∈) to show that they are a subset of another infinite set, the rationals. In NEWFOL the IBML types [natnum] and [rational] are finite data structures and

(SUBTYPE [natnum] [rational])

Natural Numbers

The whole numbers 0, 1, ... are called by mathematicians the narural numbers and are written ℕ. They are part of what we call common ground, that is, generally understood by everyone. NEWFOL calls an object that it recognizes as a natural number a [natnum]. We say that an object, obj, is (an example of) a [natnum] if it is a whole number and

(NATNUM? [natnum])

[natnum]s are only limited in size because the program #'NATNUM?, the recognizer of [natnum]s, can not recognize a [natnum] whose reprsentation as as a data structure in your an implimentation of NEWFOL would be too big to fit in your computer. Thus a [natnum] may 'have' any number of digits and their meaning is defined in the usual way by the axioms of Peano arithmetic.

Talking about [natnum]s

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

749321
6
0
293
128328287193289487593485992843579238749579459

The [context] called [arith]

The following commands are how [arith] would be made using the IBUKI Context Builder, ICB. It incorporates both the Peano axioms and those of Robinson's Q.

NAMECONTEXT [natnum];

;; define the language of [natnum]
DECLARE SORT NATNUM?;
DECLARE INDVAR n m p q (NATNUM?);
DECLARE FUNCONST suc pred (NATNUM?)= NATNUM?;
DECLARE FUNCONST + * (NATNUM? NATNUM?) = NATNUM?;
DECLARE RELCONST < 2;
DECLARE RELPAR P 1;

;; add facts
AXIOM ONEONE (FORALL (n m) (IMP (= (suc n) (suc m)) (= n m))) )
AXIOM SUCC1 (FORALL (n) (NOT (= 0 (suc n)))) )
AXIOM SUCC2 (FORALL (n)
  (IMP (NOT (= 0 n) (EXISTS (m) (= n (suc m)))))) )
DEFINE PLUS
  (FORALL (n)   (= (+ n 0) n))
  (FORALL (n m) (= (+ n (suc m)) (suc (+ n m)))) )
DEFINE TIMES
  (FORALL (n)   (= (* n 0) 0))
  (FORALL (n m) ( (* n (suc m)) (* suc (+ 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) ICB 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? ) )

[integer]s

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

[rational]s

Teaching an AI agent about arithmetic

If instead of using ICB to build [arith] and the [context]s needed to use it to do problem solving, we wanted to teach an AI agent about arithmetic. We might have the following conversation:

In English we might say

(1) 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]'." Spoken English lacks punctionation and without circumlocution lacks the ability to make this distinction.

So what could (1} mean? That is, given our understanding of meaning, how would the mind of our agent change when it hears (1)? We imagine that it thinks

Our technical solution is to recognize that the mind of the agent internal 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

Notes about Real Numbers

Here we can talk about [real] and [float]