Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm <tfm@dcs.gla.ac.uk>
Message-Id: <9404121655.AA19356@hawaii.dcs.gla.ac.uk>
To: schneide <schneide@ira.uka.de>
Cc: info-hol@cs.uidaho.edu, tfm@dcs.gla.ac.uk
Subject: Re: number theorie
In-Reply-To: Your message of "Tue, 12 Apr 94 16:12:53 +0100." <"i80fs2.ira.341:12.03.94.14.12.56"@ira.uka.de>
Date: Tue, 12 Apr 94 17:55:55 +0100


>2) Presburger arithmetic is decidable and definitions in HOL are conservative.
>    So, define multiplication in Presburger arithmetic, and obtain the same 
>    theory, which has to be therefore decidable, too. However, the theory num
>    is not decidable at all (Goedel).
>    --> Possible Answer?: 
> 		The definition of * in Presburger arithmetic requires the
> 		primitive recursion theorem, which is not a theorem of
> 		Presburger arithmetic. Proving the primitive recursion theorem
> 		requires the induction axiom which is not available in 
> 		Presburger arithmetic.

I can paraphrase what (I think) this argument is saying as follows -- I 
apologise if my interpretation is wrong. The theory

  T1:  |- 0 + n = n
       |- SUC n + m = SUC(n + m)

is deciable.  We can define multiplication as follows:

  T2:  |- 0 * n = 0
       |- SUC n * m = m + (n * m)

Now, since we can always use the equations in T2 to eliminate * in favour
of +, the theory

  T3 = T1 union T2

must be deciable too.  

The trouble witn this argument is that we can't `always use the
equations in T2 to eliminate * in favour of +'.  Consider the formula

  "P[n * <complicated term>]"

The multiplication in this formula can't be `eliminated' just by
straightforward rewriting with T2 -- since "n" is a *variable*.
Hence the argument fails.

Note that multiplication by a *constant* actually is part of Presburger
arithmetic.

Tom