A Ghost at ω1

Research output: Contribution to journalArticle

Standard

A Ghost at ω1. / Levy, Paul.

In: Logical Methods in Computer Science, Vol. 14, No. 3, 4714, 26.07.2018.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Bibtex

@article{47c5db436512414d92ca3a1166203b56,
title = "A Ghost at ω1",
abstract = "In the final chain of the countable powerset functor, we show that the set atindex 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.",
keywords = "computer science - logic in computer science, 03E75",
author = "Paul Levy",
year = "2018",
month = jul
day = "26",
doi = "10.23638/LMCS-14(3:4)2018",
language = "English",
volume = "14",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "IfCoLog",
number = "3",

}

RIS

TY - JOUR

T1 - A Ghost at ω1

AU - Levy, Paul

PY - 2018/7/26

Y1 - 2018/7/26

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

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

KW - computer science - logic in computer science

KW - 03E75

U2 - 10.23638/LMCS-14(3:4)2018

DO - 10.23638/LMCS-14(3:4)2018

M3 - Article

VL - 14

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 3

M1 - 4714

ER -