A Ghost at $\omega_1$
Logic in Computer Science
2023-06-22 v5
Abstract
In the final chain of the countable powerset functor, we show that the set at index , 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.
Cite
@article{arxiv.1612.09514,
title = {A Ghost at $\omega_1$},
author = {Paul Blain Levy},
journal= {arXiv preprint arXiv:1612.09514},
year = {2023}
}