A Ghost at ω1

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

Abstract

In the final chain of the countable powerset functor, we show that the set at
index In the final chain of the countable powerset functor, we show that the set at index ω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.

Details

Original languageEnglish
Article number4714
Number of pages27
JournalLogical Methods in Computer Science
Volume14
Issue number3
Publication statusPublished - 26 Jul 2018

Keywords

  • computer science - logic in computer science, 03E75