A Categorical Replacement for Replacement

A Categorical Replacement for Replacement

[Paul Taylor]

[-- Attachment #1: Type: text/plain, Size: 3109 bytes --]


I gave an online lecture about this at ItaCa on Tuesday.
I am going to repeat it, again online, in the Birmingham
Theoretical Computer Science seminar series.

Tomorrow, Friday, 21 November at 14:00 UTC.

The abstract and zoom details are at

researchseminars.org/seminar/TheoryCSBham<https://url.au.m.mimecastprotect.com/s/QXY-C0YKgRsGpQPK1S2iNC9xI4G?domain=researchseminars.org>

and the slides are linked from my own webpage

www.paultaylor.eu/ordinals/<https://url.au.m.mimecastprotect.com/s/JZf9CgZ05JfADKQrMt3sPC40jrc?domain=paultaylor.eu>

I will have 50 minutes instead of 30 and the reason
for repeating the talk is so that people can "cross
examine" me on the proof.

The idea (which I have been promising for many years)
for the principle "in the native language of category
theory" is that there be a reflection functor from the
category of well founded coalgebras to the subcategory
of extensional ones.

The strength of this is that it is proposed
for ANY endofunctor (instead of the powerset) and
ANY factorisation system (instead of plain monos),
subject to some conditions.

I have finally learned how ZF works and how to use it.
The lecture shows that the proposal is valid in ZF.

I am still working on how constructions such as
transfinite iteration of functors (in particular the
von Neumann hierarchy) can be obtained from my
proposal. The difficulty is that the constructive
categorical theory of ordinals is intrinsically a
mess. (Those who have followed my work for the past
30 years will be aware that I am not saying this for
want of effort in trying to sort it out.)

I will give another lecture (date and venue to be
decided) about this and the recovery of ZF from my
proposal.

----

I would like to ask the community two questions that
are relevant to this:

(1) Is the General Adjoint Functor Theorem of any use?

I would think that if you can find a "solution set"
or any of the other possible conditions for GAFT
then you should be able to describe the adjoint
directly.

So the interesting situation is when the adjoint has
to be obtained recursively (or corecursively). This
is why I think well foundedness (in some form) has
to be part of the method.

(2) Are there examples in the literature of category
theory or algebra more generally (but not set theory)
where the official first order formulation of ZF and
in particular Replacement is applied?

Paul Taylor


You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 5266 bytes --]

Re: A Categorical Replacement for Replacement

[Vaughan Pratt]

[-- Attachment #1: Type: text/plain, Size: 2366 bytes --]

A question for Paul Taylor.

Are the countable ordinals countable?

Count-erintuitively, no.  That would be a set that is a member of itself.

My question for Paul is, in your approach to ZF, can you prove this as succinctly?

After all, maybe the above proof is exploiting V = L, and maybe another Paul, Paul Cohen, can somehow force the countable ordinals to be countable.  That's where Hartogs' theorem comes in handy, as Paul and others have pointed out back in the day.

I do appreciate the search for shorter proofs, in particular what yet another Paul, Paul Erdős, has called the proof in The Book.  Satan's proof of 1+1=2 can be found spread over the first two volumes of Whitehead and Russell's Principia Mathematica.  I like the proof that writes natural numbers in Roman numerals, which use concatenation to denote addition instead of multiplication.  It is then easily seen that II = II.   The proof generalizes to III = III, and to IIII = IIII with clock Roman numerals.. It further generalizes by simplifying the Roman numerals, namely by omitting V, X, L, C, D, etc., obliging the Roman numerals to be the free monoid on a one-letter alphabet, provided we accept  =  as a theorem about natural numbers.

I also appreciate Paul's translation<https://url.au.m.mimecastprotect.com/s/3vf4CoV1Y2SrQop5KH1f2CpHUEE?domain=paultaylor.eu> of Friedrich Hartogs' 1915 paper, which I added to the references of the relevant Wikipedia article<https://url.au.m.mimecastprotect.com/s/hSJtCp81gYCn7lEqxuDhyCG5L-M?domain=en.wikipedia.org> this morning.

A second question.  Who first pointed out the applicability of Hartogs' theorem to treating ordinals in the internal logic of a topos?  Paul?

Vaughan Pratt


You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 5448 bytes --]