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.

@article{paperbot392,
  title = {A Ghost at $\omega_1$},
  author = {Paul Blain Levy},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 3},
  year = {2018},
  doi = {10.23638/lmcs-14(3:4)2018}
}