## Sanders, Sam - Grilliot's trick in Nonstandard Analysis

lmcs:4114 - Logical Methods in Computer Science, November 30, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:23)2017
Grilliot's trick in Nonstandard Analysis

Authors: Sanders, Sam

The technique known as Grilliot's trick constitutes a template for explicitly defining the Turing jump functional $(\exists^2)$ in terms of a given effectively discontinuous type two functional. In this paper, we discuss the standard extensionality trick: a technique similar to Grilliot's trick in Nonstandard Analysis. This nonstandard trick proceeds by deriving from the existence of certain nonstandard discontinuous functionals, the Transfer principle from Nonstandard analysis limited to $\Pi_1^0$-formulas; from this (generally ineffective) implication, we obtain an effective implication expressing the Turing jump functional in terms of a discontinuous functional (and no longer involving Nonstandard Analysis). The advantage of our nonstandard approach is that one obtains effective content without paying attention to effective content. We also discuss a new class of functionals which all seem to fall outside the established categories. These functionals directly derive from the Standard Part axiom of Nonstandard Analysis.

Volume: Volume 13, Issue 4
Published on: November 30, 2017
Submitted on: November 30, 2017
Keywords: Computer Science - Logic in Computer Science