Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: John.Harrison@cl.cam.ac.uk, info-hol@cs.uidaho.edu
Subject: Re: number theory
In-Reply-To: Mail from 'John Harrison <John.Harrison@cl.cam.ac.uk>' dated: Tue, 12 Apr 94 16:08:52 +0100
Date: Tue, 12 Apr 1994 19:02:21 +0200
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.986:12.03.94.17.02.31"@ira.uka.de>


I add the definitions of Andrew's book, since nobody could
answer my first question up to now.

The following are types of higher order logic:
 - ind is a type (ind denotes the type of the individuals).
 - bool is a type (bool denotes the boolean values).
 - If alpha_1,...,alpha_n and beta are types, then 
	(alpha_1 #...#alpha_n) -> beta is a type.

The order of a type is defined as follows:
 - ord(ind):=0
 - ord(bool):=1
 - ord((alpha_1 #...#alpha_n) -> bool) := 1+Max(alpha_1,...,alpha_n)
 - ord((alpha_1 #...#alpha_n) -> beta) := 1+Max(alpha_1,...,alpha_n, beta)
    (for beta<>bool)

Answers to the second problem:
J. Harrison wrote:
|> 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".

Matt Kaufmann wrote:
|> For #2:  yes, there's no way to make inductive definitions in Presburger.  The
|> coding of inductive definitions in Peano arithmetic is traditionally done using
|> some trick involving the Chinese remainder theorem, but that's not available in
|> Presburger.  Something like that.


The answer to the third question is a bit more complicated:
Goedel's Incompleteness theorem can be stated as follows:

  Each consistent minimal adequate recursively axiomatized 
  theory is incomplete.

where minimal adequate means that the following axioms
hold:
   (i) !x. ~ SUC(x) =0.
   (ii) !x. ~x=0 ==> ?y. x=SUC(y)
   (iii) !x y. SUC(x) = SUX*y) ==> x=y
   (iv) !x. x+0 = x
   (v)  !x y. x+SUC(y) = SUC(x+y)
   (vi) !x. x*0 = 0
   (vii) !x y. x*SUC(y) = (x*y)+x

The reference to the above theorem is
   
@book{MaYo78,
   author = {{M. Machtey} and {P.Young}},
   key = {MaYo78},
   publisher = {North-Holland},
   title = {An Introduction to the General Theory of Algorithms},
   year = {1978}
}

The question is what recursively axiomatized means. As J. Harrision
pointed out, there is a significant difference between what is derivable
in HOL and what is really true in the semantical sense.

In order to pick up another issue, I want to add a piece of discussion
with M.Kaufmann. He wrote:

|> But perhaps instead you are imagining two-sorted models of arithmetic, where
|> one sort ("type") contains the numbers and the other contains the "classes"
|> (sets of numbers), and the universal class quantifier ranges over those classes
|> in the model rather than over all classes.  Then you can stay in the realm of
|> first-order logic.  But in that case, once again the axioms do not characterize
|> the standard model.  One can obtain models of this version of PA in which the
|> number part is non-standard, and the class part is (necesssarily) a proper
|> subset of the power set of the number part -- in fact, there are such models
|> (by the Lowenheim-Skolem theorem) in which the class part is countable.

So, one has always to be careful when working with higher order theories.
I think there is a real problem if objects of the real world are to be modelled, i.e.
is my special HOL-theory really a model of my considered piece of world?

I think that this problem is not considered appropriately.

Klaus.