A Ghost at $\omega_1$

TL;DR

This paper demonstrates that in the final chain of the countable powerset functor at , a 'ghost' element exists that is not strongly extensional, revealing new insights into the structure of these transition systems.

Contribution

It introduces the existence of 'ghost' elements in the final chain at  and characterizes when sets are strongly extensional in these chains.

Findings

Existence of ghosts at  in the final chain of the powerset functor

Ghosts are present at larger ordinals in other subfunctors

Provides a precise description of strongly extensional sets in these chains

Abstract

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.