[FOM] A subtlety in Takeuti

[Colin McLarty]

There is a point in Takeuti's ``conservative extension of Peano
Arithmetic'' which I want to be sure of gettng right.  He gives a
careful argument using cut removal for simple type theory, to show his
higher order extension of PA (with comprehension and induction only
for arithmetic formulas, admitting free variables of higher type but
not quantifed ones) is conservative over PA.   Before that he leaves
it as an exercise to show that adding type theory with full
comprehension to any first order theory T gives a conservative
extension of T.

Clearly the reason that exercise is easier than his conservativeness
result, is that merely adding type theory with comprehension to a
first order theory creates no serious involvement of the higher types
with the first order statements.  His extension of PA does involve
higher types in both the induction axiom and the equality axiom and it
is a subtle thing to make sure it remains conservative.

But I want to modify his result and so I want to be sure I understand
exactly what kind of involvement matters.  It comes down to the role
of the equality axiom.  In his book Proof Theory he seems to take the
equality axiom as part of second order or higher order type theory,
while in ``conservative extension'' he eventually takes it as a
mathematical axiom of analysis.  I am not clear which version he has
in mind wihen he refers to "type theory" in that exercise.  (It is in
the ``conservative extension'' paper, but before he has introduced his
axioms there, and it cites the book Proof Theory.)

In more detail, the issue is this:

I believe the answer to the exercise is just Henkin's completeness
theorem for type theory: that if we took (first order) PA and merely
added type theory with full comprehension then any model of (first
order) PA would extend directly to a Henkin model of this and so we
get no new theorems in the first order part.  But what if we kept the
first order induction scheme as it is, add type theory with full
comprehension, and add the equality axiom relating equality of first
order terms (natural numbers) to formulas with higher order variables?

I believe the argument I just gave continues to work, so Henkin's
completeness theorem for type theory suffices to show this is a
conservative extension.  Am I right?  Or do we now have to go into the
more involved proof of cut removal for type theory?

Or is it all more complicated than that?

thanks for any help, Colin