  We consider implicit definability of the standard part {0,1,...} in
nonstandard models of Peano arithmetic (PA), and we ask whether there is a
model of PA in which the standard part is implicitly definable. In section 1,
we define a certain class of formulas, and show that in any model of PA the
standard part is not implicitly defined by using such formulas. In section 2 we
construct a model of PA in which the standard part is implicitly defined. To
construct such a model, first we assume a set theoretic hypothesis
diamondsuit_{S_lambda^{lambda^+}}, which is an assertion of the existence of a
very general set. Then we shall eliminate the hypothesis using absoluteness for
the existence of a model having a tree structure with a certain property.
