Grilliot's trick in Nonstandard Analysis

The technique known as Grilliot's trick constitutes a template for explicitlydefining the Turing jump functional $(\exists^2)$ in terms of a giveneffectively discontinuous type two functional. In this paper, we discuss thestandard extensionality trick: a technique similar to Grilliot's trick inNonstandard Analysis. This nonstandard trick proceeds by deriving from theexistence of certain nonstandard discontinuous functionals, the Transferprinciple from Nonstandard analysis limited to $\Pi_1^0$-formulas; from this(generally ineffective) implication, we obtain an effective implicationexpressing the Turing jump functional in terms of a discontinuous functional(and no longer involving Nonstandard Analysis). The advantage of ournonstandard approach is that one obtains effective content without payingattention to effective content. We also discuss a new class of functionalswhich all seem to fall outside the established categories. These functionalsdirectly derive from the Standard Part axiom of Nonstandard Analysis.Comment: 21 page