Standard cut of a nonstandard model of arithmetic (source code)

= Standard cut of a nonstandard model of arithmetic

The standard cut is the external initial segment consisting of the interpretations of the standard numerals. It is not definable, even with parameters, inside the nonstandard model.