Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@cs.uidaho.edu
Subject: Re: number theorie
In-Reply-To: Your message of "Tue, 12 Apr 94 16:12:53 +0200." <"i80fs2.ira.341:12.03.94.14.12.56"@ira.uka.de>
Date: Tue, 12 Apr 94 16:08:52 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:027650:940412150917"@cl.cam.ac.uk>


As an ignorant non-logician I'll attempt to answer Klaus's questions:

| 1) In many logical textbooks, we find definitions for terms, types and their
| order. Unfortunately, I only found book which considered type theory without
| polymorphic types. Now, I tried to adapt the definitions to type theory with
| polymorphism and I found a problem: What is the order of a type variable?

I'll pass on this one, as I'm not quite sure what "order" means. Have you
looked in Andrews' book? Maybe this is the book you mean...

| 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 think as you say this shows that multiplication is *not* (first-order)
definable in terms of addition. This isn't immediately obvious; in fact if I
recall correctly, exponentiation *is* definable given multiplication, and that
superficially looks "equally difficult".

From Presburger's proof in terms of congruences, I think it follows that the
sets of natural numbers definable in Presburger arithmetic are always
"eventually periodic", ruling out, for example, all squares, which would be
definable given multiplication ("?x. n = x * x"). There's a really superb
treatment of this in Enderton's book on logic, but I can't remember it very
well, unfortunately.

Incidentally (for English speakers rather than Klaus) there's a Cornell
techreport which gives an annotated translation of Presburger's original
article, and it's quite readable once you adjust to Polish notation (e.g. A x y
for x \/ y or something like that...)

| 3) The theory of the natural numbers has a unique model up to isomorphism
|    which can be axiomatized by Peano's Axioms. Therefore the set of closed
|    formulae which become true under the standard interpretation contains
|    either phi or ~phi. However, this means that this theory is complete,
|    in contradiction to Goedels theorem! What is wrong?

The problem is that "true under the standard interpretation" isn't the same as
"deducible in HOL". The true sentences do not form a recursively enumerable
set. In fact Tarski's theorem says they are not even first order definable
(recursively enumerable corresponds to `definable by a Sigma-0-1 sentence',
i.e. one of the form "?n. t[n]" where "t[n]" is free of [unbounded]
quantifiers). The theorems of HOL (even those "in principle" deducible in HOL)
do -- this is fairly obvious by sorting the collection of all possible proofs
in a reasonable way but I wouldn't like to have to prove it formally.

John.