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: number theorie
Date: Tue, 12 Apr 1994 16:12:53 +0200
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.341:12.03.94.14.12.56"@ira.uka.de>


I wondered about some theoretical points ...


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?

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.

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?