Sam Sanders - 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 AnalysisArticle

Authors: Sam Sanders

    The technique known as Grilliot's trick constitutes a template for explicitly defining the Turing jump functional (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 Π01-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
    Accepted on: November 30, 2017
    Submitted on: November 30, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 2391 times.
    This article's PDF has been downloaded 603 times.