We present an extension of type theory with a fixed point
combinator Y. We are particularly interested in using this Y for
doing unbounded proof search in the proof system. Therefore we treat
in some detail a typed lambda-calculus for higher order predicate
logic with inductive types (a reasonable subsystem of the theory
implemented in COQ) and show how bounded proof
search can be done in this system, and how unbounded proof
search can be done if we add Y.
Of course, proof search can also be implemented (as a tactic) in the
meta language. This may give faster results, but asks from the user
to be able to program the implementation. In our approach the user
works completely in the proof system itself.
We also provide the meta theory of type theory with Y that allows to
use the fixed point combinator in a *safe* way. Most
importantly, we prove a kind of *conservativity result*, showing
that, if we can generate a proof term M of formula 
phi in the extended system, and M does not contain Y, then M
is  already a  proof of phi in the original system.