Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: transfinite composition

GhaS Shee (Sep 14 2020 at 15:38):

@[Mod] Morgan Rogers
Do you know any good instruction papers about transfinite compositions which is applied to type theory or logic ?

John Baez (Sep 14 2020 at 15:41):

Not quite what you're asking for, but Todd Trimble just wrote an expository paper proving Tychonoff's theorem using transfinite compositions. You'd have to ask him to take a look. It's not about type theory or logic, but it explains transfinite composition.

(I mention this mainly because I saw the paper just yesterday, and I'd never heard of "transfinite composition" before then.)

GhaS Shee (Sep 14 2020 at 15:43):

@John Baez
Thank you for that information. I am loving to see it! :heart_eyes: ( I would like to avoid using AC! )
I recently found the term "transfinite composition" in Cisinski's Book (Higher Categories and Homotopical Algebra :
Definition 2.1.2).
And my current interest about this question is type theoretic implementation of proof assistant systems, using lambda term, of classical logics.

In some papers, I found three ways how to implement classical logic;

1. "symmetric lambda calculus"
2. assuming "~~A -> A" on MLTT, HoTT or something else
3. "continuation passing style"

Additionally, I felt that these concepts have something to do with the existence of colimit.
I see the definition of the following two terms but do not understand the relation between" transfinite induction" and "transfinite composition" too.

Now I cannot organize the type theory which is correspond to classical Logic well.

Morgan Rogers (he/him) (Sep 14 2020 at 21:07):

I'm afraid this is also the first time I'm encountering this concept (I found the reference you mention)
What relationship to you see between transfinite composition and implementations of classical logic, @GhaS Shee ?

GhaS Shee (Sep 15 2020 at 01:33):

@[Mod] Morgan Rogers
For me, the transfinite composition is saying about the existence of the morphism to some kind of colimits.
Assuming the existence of colimit in the computation, for me, it seems to handle a computation that never ends.
If we have morphisms to the computation that never ends, we can ADD some number to the value which we get from the never-ending computation.
I think that this concept, doing the latter calculation first, is the very what we call "continuation", with which we might construct classical logic.

Morgan Rogers (he/him) (Sep 15 2020 at 08:19):

Ah, I see what you're getting at, more or less.
There are various principles that come under the banner of "classical logic".
One of these is the law of excluded middle, which (as long as you have the relevant logical operators to hand) is equivalent to the double negation elimination rule you mentioned.
Another is the axiom of choice.
However, you should just beware that:

1. There are other, less frequently encountered principles of classical logic. The collection of classical principles do not form a single homogeneous mass: it's possible to explore them independently (although some imply others) so beware that any approach you take to study or implement classical logic may carry only some of these principles.
2. Just because a principle is non-constructive does not make it a principle of classical logic. I don't understand transfinite composition well enough to tell how it fits in yet.
3. The definition of transfinite composition does not assert that the colimit exists, but rather that whenever the colimit does exist, a certain leg of the colimit cone also lies in the class of morphisms being studied.

GhaS Shee (Sep 15 2020 at 10:03):

Yes, indeed :-)

John Baez (Sep 15 2020 at 15:47):

From Todd Trimble's paper I gather that transfinite composition is a case of transfinite recursion. Transfinite recursion is a way to recursively define functions indexed by ordinals. You need to separately treat successor ordinals (as in ordinary finite recursion) and limit ordinals. Transfinite recursion is to the ordinary finite recursive definition of functions as transfinite induction is to ordinary induction. Wikipedia tells me this:

Proofs or constructions using induction and recursion often use the axiom of choice to produce a well-ordered relation that can be treated by transfinite induction. However, if the relation in question is already well-ordered, one can often use transfinite induction without invoking the axiom of choice. For example, many results about Borel sets are proved by transfinite induction on the ordinal rank of the set; these ranks are already well-ordered, so the axiom of choice is not needed to well-order them.

David Michael Roberts (Sep 17 2020 at 09:50):

@John Baez where did you see this paper? Searching "Todd Trimble transfinite composition" doesn't help me, nor does substituting "Tychonoff theorem"

Morgan Rogers (he/him) (Sep 17 2020 at 10:20):

Not yet uploaded, I believe you would need to ask him personally to see it.

John Baez (Sep 17 2020 at 13:52):

Todd is writing this paper now. He paid my student Joe Moeller to put it in the format for submission to the American Mathematical Monthly. Joe, Todd and I are working on another paper together.

I don't know if Todd plans to put this paper on the arXiv. He hasn't published in a long time; he wants to get back into it.