HOME

Computer Arithmetic

Version 2.001 2024-06-19
Started 2015-12-25

Author:

Richard Weyhrauch (IBUKI)

Note:

This is an 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.

This note is called: [COMPUTER-ARITHMETIC]
The notation used in this note is described in [NOTATION]
Under development

Preface

This note gives a theory of Mental arithmetic. The issue addressed here is what do we know about arithmetic and how we can reason about natural numbers.

Introduction

Heads are finite and therefore it is trivial that no head can contain 'all' the natural numbers. The question addressed in this note is what therefore is in our heads when we think about numbers? Clearly we know about small numbers: 0,1,2, ... n. We also know the if we add or multiply two of these numbers we get another one. So far so good. But noe suppose I say 'This morning I heard about a natural number called a googel.' What do I know now? Well ny general knowledge has already told me that if I have two numbers, that their sum is a number so (googel+1) is a number, also (6+googel), ..., likewirs I know (11*google) is a number and even (Google*Google). If now I use my logical trainong I might say 'Aha, since its a number all the theorems of Peano arithmetic will apply to a googel.' But here things start going bad. If this were to be a number like the small ones I mentioned before I should be able to write the theorem google=succ(succ( ... (succ(0)) ... )), which contains googel copies of the function symbol 'succ' and (2*googel) parenthese. I have now become so interested in knowing about the number 'googel' that I go to the Wikipedia and discover a bunch of things

(1) googel=(expt 10 100) = (1 followed by 100 0's)
(2) there is even a bigger number called a googelplex'.
(3) googelplex=(expt 10 googel)

Then I read the following troubling 'fact'.

(4) The number of particles in the universe is less that a googelplex.

This is troubling because it means that inlike a small number like 5 where I can count it as

5=succ(succ(succ(succ(succ(0)))))

First, let's write down some 'facts' we know about numbers on the basis of Peano arithmetic.

(5) 0, 1, 2, 4, 5, 6, googel, googelplex are numbers.
(6) if we use 'plus', 'times'. or 'expt' on any two numbers we get another
    number.

Question
-------------------------------------------------------------------------------
The usual language of Peano Arithmetic only contains the individual constant
symbol '0' and the function constant symbol 'succ' so where do the numerals
for natural numbers and the function symbols 'plus', 'times', ... come from?
-------------------------------------------------------------------------------

Aside
-------------------------------------------------------------------------------
The usual description of a first order language ususlly includes words like
the variable symbols v1, ...,  vn. ... . This has two
problems: one, on the face of it, it is circular (what are the subscripts
1, ..., n, ... ; and two, We can't actually put all these in our heads.

We deal with this problem for NEWFOL [context]s as follows:

(1) A NEWFOL [context] is a finite data structure and so the language of a
    NEWFOL [context] is a finite data structure.

(2) Adding a new symbol to the language of a theory creates a new theory
    that is a conservative extension of the original theory.

(3) In NEWFOL rules of inference are operations on [context]s that preserve
    consistency. The program

      (context-add-new-indvar context sym)

    retuens a new [context] which is like the argument context except that
    syn has been added to its language. The proof that this program preserves
    consistency mimics the proof that adding a new symbol to the language of
    a first order theory is a conversative extention.

(4) The idea of a consistentency preserving operation on [context]s is one
    that takes a coherent/consistent understanding/theory of something and
    produces a new coherent understanding of something. There is a detailed
    discussion of these operations in [SATvsVAL].

(5) In textbook descriptions of logic authors frequently omit the kind of
    issue discussed above. It is simply easier on the learner to avoid
    mentioning the notion of conservative extenson until sometime after
    some understanding has developed about what a theory (and its language)
    might be. It is surely easier to gloss over the difference between a
    language with an 'infinite' supply of symbols and how you might deal
    with a finite one. Notice this issue has been sluffed over above (by me)
    when discussing numerals, i.e., infinite number of individual constants
    and in the question above.
-------------------------------------------------------------------------------

Finally we get to the crux of the matter. In fact the discussion above mimics the discussion of nonestandard models of arithmetic as analysed in kolem [1922]. In that paper he imagined that the standard model of arithmetic contained the normal natural numbers. The question was then, since we know by the LowenHEIM-Skolem theorem that there are an infinite collection of countable models of first order arithmetic, what do they look like? The answer is that they all have the order type N+IQ. This was shown by imagining that in a 'non-standard' model there must be at least one non-standard natural nunber. The characterization follow as a directly.

My observation was that in our heads a 'googel' is much like a 'non-standard' integer. It is 'bigger' than any 'standard' number and must obey all the axions and have all the properties that follow from the Peano axioms. For example it must have a successor. So the idea is like this: we divide the natural numbers into 'small numbers' (standard) and 'large numbers' (non-standard).

Before I present the theory I want to prove some preliminary theorems.

(1) if p,n < 2m then pn,np < 2m2

This neans thay the numbers below 2^m are closed under 'plus' and times' wrt big numbers.

The Theory of Mental Arithmetic

Objects in a head of type [natnum] (natural numbers starting with 0, as is customary in computer science) are ...

Small [natnum]s
large [natnum]s

computer arithmetic

(ISIN n c)
(IMPLIES (AND (gt n 0) (ISIN n c)) (ISIN (pred n) c))
(list-length (l) 
  (IF (EQUAL l EmptyList) 0 (succ (list-lendth (list-rest l)))) )
(IMPLIES (ISIN l c) (ISIN (list-length l) c))
(IMPLIES (ISIN n c) (lt (size n) (size c)) )
(EXIST n (NOT (ISIN n c)))
(IMPLIES (gt (size (+ x y)) (size c)) (NOT (ISIN (+ x y) c)) )653182012566