Coalgebra and abstraction (Q1981994)

Philosophers now study Frege's fifth basic law of thought (BLV) and related axioms against the backdrop of second-order logic, in which the principle is expressed as \[ \forall X\forall Y\left( \varepsilon X=\varepsilon Y\leftrightarrow\forall x\left( Xx\leftrightarrow Yx\right) \right) \] where \(\varepsilon\), called an \textit{abstraction operator}, is a type-lowering operator combining with a second-order term to form a first-order term. BLV claims that any two subsets of the domain possess the same \textit{extension} iff they have the same elements. Regrettably, BLV is untenable because the mapping \(\varepsilon\)\ from the power set of a set to the set itself is assumed to be injective. One possible modification is George Boolos's new V (NV), which is expressed as \[ \forall X\forall Y\left( \ast X=\ast Y\leftrightarrow\forall x\left( Xx\leftrightarrow Yx\right) \vee\left( \mathrm{Big}\left( X\right) \wedge\mathrm{Big}\left( Y\right) \right) \right) \] which says that any two subsets of the domain possess the same \textit{subtension} iff they are equal or both are of the same cardinality as the full domain. \textit{G. Boolos} [in: Logic, logic, and logic. With introductions and an afterword by John P. Burgess. Edited by Richard Jeffrey. Cambridge, MA: Harvard University Press. 88--104 (1998; Zbl 0972.03511)] showed that NV can be used to interpret a nontrivial set theory \[ \mathrm{ZF2-P-Inf+GC} \] consisting of all the axioms of second-order Zermelo-Frankel set theory with the exception of power set and infinity and with the addition of an axiom of global choice. This paper shows how Boolos's construction amounts to identifying an initial \(F\)-algebra in a certain category, identifying a natural coalgebraic dual to Boolos' axiom which naturally interprets large parts of Aczel's non-well-founded set theory [\textit{P. Aczel}, Non-well-founded sets. Foreword by Jon Barwise. Stanford, CA: Center for the Study of Language and Information (1988; Zbl 0668.04001)] via the construction of a certain terminal \(F\)-coalgebra.