FOM: Decidable?

[Joseph S. Miller (Grad)]

On Tue, 16 Apr 2002, Hubert Wagner wrote:

> Is there an easy argument showing that the first order theory of 
> positive natural numbers with multiplication and constants 1 and 2 is 
> decidable?
> Without constant2 the theory is decidable by results of Mostowski and 
> Feferman&Vaught.
> 
> Hubert Wagner
> 

There is nothing special about 2; it acts just the same as any other
prime, if you are restricted to multiplication.  So take \phi(2) to be the
sentence that you want to decide in the expanded language and, treating 2
as a variable, decide

  \forall 2 ((2 is prime) -> \phi(2))

using the original decision procedure.  By breaking them down into their
distinct primes, any constants can be handled.

Alternately, you could use automata on finite trees in much the same way
that automata on finite strings can be used to decide Presburger
arithmetic.  An integer can be encoded as the sequence of it's (binary
encoded) prime exponents coming off of a main trunk.  Multiplication is
easily seen to be automata recognizable and using the closure properties
of tree automata you get a decision procedure.  Again, you can see that
all constants are available to you.

Joe Miller