Paul Blain Levy - A Ghost at $\omega_1$

lmcs:2626 - Logical Methods in Computer Science, July 26, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:4)2018
A Ghost at $\omega_1$Article

Authors: Paul Blain Levy

    In the final chain of the countable powerset functor, we show that the set at index $\omega_1$, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at each successor index is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of other subfunctors of the powerset functor. This leads to a precise description of which sets in these final chains are strongly extensional.


    Volume: Volume 14, Issue 3
    Published on: July 26, 2018
    Accepted on: July 6, 2018
    Submitted on: January 2, 2017
    Keywords: Computer Science - Logic in Computer Science,03E75

    1 Document citing this article

    Consultation statistics

    This page has been seen 1692 times.
    This article's PDF has been downloaded 357 times.