[FOM] Query for Martin Davis. was:truth and consistency

[Bill Taylor]

I applaud this very nice post of Robin Adams.


> The set of terms is defined thus:
> 
> 1) 0 is a term.
> 2) If t is a term, then t+1 is a term.

... ...

> 1) t + u is defined to be the result of substituting t for the sole
> occurrence of 0 in u.
> 
> 2) t * u is defined to be the result of substituting t for each
> occurrence of 1 in u, then removing every instance of `+0' in the result.


All very nice.  But then there comes a later bit...


> (Alright, I can't write a definition of exponentiation in the style I did
> addition and multiplication; I would have to just write the recursive defn.

But I can't see why.  Why can't you just say something like...

3) t^u  is defined to be the result of writing  u, then replacing every
   appearance of +1  by *t, dropping the initial 0*, then removing from
   the left every appearance of  *  as in rule 2.

What am I missing?  Why can't this be done, Robin?

-------------------------------------------------------------------------------
Bill Taylor                                      W.Taylor at math.canterbury.ac.nz
-------------------------------------------------------------------------------
     In math we decide on the rules - then try to deduce the consequences.
     In science we observe the consequences, then try to deduce the rules.
-------------------------------------------------------------------------------