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 $(\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
    Accepted on: November 30, 2017
    Submitted on: November 30, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1776 times.
    This article's PDF has been downloaded 578 times.