Hanul Jeon
hanuljeon95.bsky.social
Hanul Jeon
@hanuljeon95.bsky.social
46 followers 42 following 48 posts
A doctoral student at Cornell. Interested in logic and set theory. he/him. Homepage: https://hanuljeon95.github.io
Posts Media Videos Starter Packs
Reposted by Hanul Jeon
'아무튼 공황과 침체는 안된다고' 이러면서 유동성을 공급한 결과는 그 유동성으로 소시오패스를 세계 최고의 부자로 만들었고, 이 스노우볼이 굴러가서 수억 수십억명이 고통받고 수십 수백만명이 사망하는 세상을 만들었다. 비둘기들은 본인들이 벌인 일에 대한 자각이 있는지 궁금하다.

자본주의도 민주주의도 이제 황혼을 지나고 있다는 생각이 계속 든다.
That means, when we ask "If ZFC + {n inaccessibles | n natural} and CIC + LEM + (some choice) prove the same statements," we should formulate it as sth like

If F is an interpretation from type-theoretic language to set theory, then whether "type theory proves P" iff "set theory proves F(P)."
The debate on this question reminded me of what I thought before: Type theory can better force a meaning of a sentence through its syntax, so when we ask about the conservativity between set theory and type theory, we should ask about the conservativity of type-theoretic statements.

t.co/cNGFQBJLoO
https://mathoverflow.net/a/91055/48041
t.co
Junk theorems in set theory are not a bug but a feature.
Good googologists must be logicians (the converse does not hold)
I think Girard's beta cut elimination theorem is essentially cut elimination via operator controlled derivations since we can think of a dilator as an operator taking an ordinal and returning the closure under operators the dilator encodes.
The entrance door of logician's hell has a plaque with a single word "Π¹₃"
Googologists should refrain from making and naming random large countable ordinals for no reason.

I am quite skeptical of how many googologists have even tried to learn Gentzen's ordinal analysis, where the story about recursive ordinal systems started.
I learned that every non-standard model of IE1 contains an initial segment satisfying PA. It really sounds like a low-level version of Ville's lemma, which says every ill-founded ω-model of weak set theory (probably Ø-provident set theory) contains an initial segment satisfying KP.
Team Cherry demands the hardcore user to really be a hardworking hardcore user. Alas, we are already too busy to be a hardcore user in math.
Doing every achievement sounds really tough...
Just for curiosity, to a month-old post: Did you finally free Phaloom?
I hated infinitary types in the proof of projective determinacy when I learned it first time.

Now I think infinitary types are an unavoidable feature of Woodin cardinals.
OTOH, Dorais' equiconsistency proof between ACA0+ and Provident set theory seems to give a bi-interpretation between these two theories in a way to preserve β-models. (A β-model of ACA0+ should be an ω-model of ACA0+ that is correct about recursible well-orders.)
BTW I found my idea about connecting rudimentary set theory and ACA0 turned out to be wrong. I re-checked Taranovsky's claimed proof, and his idea only produces how to generate an ω-model of one from the other.
I believe type theory also has some cumulative nature when we start to talk about large-cardinal-like axioms (like the level of universes). Set theory has better control on the hierarchy, so replacing set theory with type theory as a consistency-strength calibrator may be hard.
One of the main features of set theory as a foundational theory is its cumulative nature. Set theory, in particular, combined with fine-structural machinery, allows fine control in each cumulative hierarchy that often has a role in calibrating the strength of theories.
I believe it is somehow relevant to understanding the iterated Bachmann-Howard collapsing of a dilator.
I am thinking about the possibility that the number of arguments of a predilator can be… functorially variable, so it takes a linear order A first, then takes an A-indexed family of linear orders, then returns a linear order.
You should protect your time from Silksong first (by a person who lost 40+ hours to it).
I think, we should apply the same POV to zero sharp. Adding zero sharp means, we add bunch of ordinals from the least height model of ZFC so that at some height of L-hierarchy, we have an L-ultrafilter, giving an iterable mouse.
We can enhance this theory by adding the axiom "There are two cardinals." The most natural model-theoretic POV for adding the axiom is end-extending from H(ω₁) to H(ω₂).

We do not think something like, "Add the axiom, then the (fixed) largest cardinal now has an additional cardinal below."
One misconception(?) about the zero sharp is that it "makes" ω₁ inaccessible in L. I think it is not a good POV.

To see why, let us go below: Lat us think of ZFC⁻ (= ZFC without powerset) plus "There is the largest cardinal."
We also proved that the supremum of β-ranks of recursive theories is δ^1_2. We also calculated the β-rank of some theories, and for sufficiently strong theories, it coincides with the height of the least transitive model of the theory.
In this paper, we defined an alternative way to rank the strength of theories via β-models called the β-rank, and established its basic properties.

We proved that the supremum of the β-rank of theories in the language of set theory is ω1, and the same for the language of SOA if we assume V=L.
Hanul Jeon, Patrick Lutz, Fedor Pakhomov, James Walsh
Ranking theories via encoded $\beta$-models
https://arxiv.org/abs/2503.20470