arXiv subjects

Hanul Jeon

Publications and source records attributed to Hanul Jeon.

13 recordsLinked to original sources

arXiv2026

Dilator-based analysis of KP

Proof theorists developed various frameworks to analyze impredicative systems like $\Pi^1_1\text{-}\mathsf{CA}_0$ or $\mathsf{KP}$; One is an operator-controlled derivation system, and the other is Girard's dilator-based $\beta$-logic. In this paper, we provide a functorial formulation of operator-controlled analysis of $\mathsf{KP}$, thereby unifying the two approaches into a single framework. As an application, a new proof of Girard's boundedness theorem is also provided, which states that every $\Sigma_1$-over-$L_{\omega_1^{\mathsf{CK}}}$-definable function $\omega_1^\mathsf{CK}\to \omega_1^\mathsf{CK}$ is bounded by a recursive dilator.

math.LO↗

arXiv2026

The Axiom of Double Complement and its opposites

Powell introduced the Axiom of Double Complement ($\mathsf{DCom}$) to give his double-negation interpretation of $\mathsf{ZF}$ into $\mathsf{IZF_{Rep}}$. However, the consistency, strength, and compatibility of $\mathsf{DCom}$ remain open problems. This article aims to survey the compatibility and consistency strength of $\mathsf{DCom}$, its consequence and opposites, which will be named $\mathsf{NDCom}$ and $\mathsf{ADCom}$. We will also develop Lubarsky's Kripke models over $\mathsf{CZF}$ to derive these results. We will show that $\mathsf{DCom}$ proves the Powerset axiom over $\mathsf{CZF}$ and is independent of $\mathsf{IZF}$. We will also show that $\mathsf{ADCom}$ does not add consistency strength over $\mathsf{CZF}$, by modifying the construction of Lubarsky's model for $\mathsf{CZF+\lnot Pow}$. We will also show that $\mathsf{DCom}$, $\mathsf{ADCom}$, and $\mathsf{NDCom}$ are persistent under realizability under modest conditions.

math.LO↗

arXiv2025

Ranking theories via encoded $\beta$-models

Ranking theories according to their strength is a recurring motif in mathematical logic. We introduce a new ranking of arbitrary (not necessarily recursively axiomatized) theories in terms of the encoding power of their $\beta$-models: $T\prec_\beta U$ if every $\beta$-model of $U$ contains a countable coded $\beta$-model of $T$. The restriction of $\prec_\beta$ to theories with $\beta$-models is well-founded. We establish fundamental properties of the attendant ranking. First, though there are continuum-many theories, every theory has countable $\prec_\beta$-rank. Second, the $\prec_\beta$-ranks of $\mathcal{L}_\in$ theories are cofinal in $\omega_1$. Third, assuming $V=L$, the $\prec_\beta$-ranks of $\mathcal{L}_2$ theories are cofinal in $\omega_1$. Finally, $\delta^1_2$ is the supremum of the $\prec_\beta$-ranks of finitely axiomatized theories.

math.LO↗

arXiv2025

Martin's measurable dilator

Martin's remarkable proof of $\mathbf{\Pi}^1_2$-determinacy from an iterable rank-into-rank embedding highlighted the connection between large cardinals and determinacy. In this paper, we isolate a large cardinal object called a measurable dilator from Martin's proof of $\mathbf{\Pi}^1_2$-determinacy, which captures the structural essence of Martin's proof of $\mathbf{\Pi}^1_2$-determinacy.

math.LO↗

arXiv2025

Proof-theoretic dilator and intermediate pointclasses

There are two major generalizations of the standard ordinal analysis: One is Girard's $\Pi^1_2$-proof theory in which dilators are assigned to theories instead of ordinals. The other is Pohlers' generalized ordinal analysis with Spector classes, where ordinals greater than $\omega_1^{\mathsf{CK}}$ are assigned to theories. In this paper, we show that these two are systematically entangled, and $\Sigma^1_2$-proof theoretic analysis has a critical role in connecting these two.

math.LO↗

arXiv2024

On a cofinal Reinhardt embedding without Powerset

In this paper, we provide a positive answer to the question of Matthews whether $\mathsf{ZF}^-$ is consistent with a non-trivial cofinal Reinhardt elementary embedding $j\colon V\to V$. The consistency follows from $\mathsf{ZFC} + I_0$, and more precisely, it is witnessed by Schlutzenberg's model of $\mathsf{ZF}$ with an elementary embedding $k\colon V_{\lambda+2}\to V_{\lambda+2}$.

math.LO↗

arXiv2024

The behavior of higher proof theory I: Case $\Sigma^1_2$

Walsh [MR4525964, Zbl 1569.03151] has shown that comparing proof-theoretic ordinals is equivalent to comparing $\Pi^1_1$-consequence comparison and $\Pi^1_1$-reflection comparison, all modulo true $\Sigma^1_1$-sentences. In this paper, we prove the analogous result for $\Sigma^1_2$-consequences modulo true $\Pi^1_2$-sentences, that is, the equivalence between $\Sigma^1_2$-proof-theoretic ordinal comparison, $\Sigma^1_2$-consequence comparison, and $\Sigma^1_2$-reflection comparison, all modulo true $\Pi^1_2$-sentences. We also examine the connection between $\Sigma^1_2$-proof-theoretic ordinal and $\Sigma^1_2$-analogue of the robust reflection rank in Pakhomov-Walsh [MR4362917, Zbl 1511.03018]

math.LO↗

arXiv2023

Generalized ordinal analysis and reflection principles in set theory

It is widely claimed that the natural axiom systems$\unicode{x2013}$including the large cardinal axioms$\unicode{x2013}$form a well-ordered hierarchy. Yet, as is well-known, it is possible to exhibit non-linearity and ill-foundedness by means of \emph{ad hoc} constructions. In this paper we formulate notions of proof-theoretic strength based on set-theoretic reflection principles. We prove that they coincide with orderings on theories given by the generalized ordinal analysis of Pohlers. Accordingly, these notions of proof-theoretic strength engender genuinely well-ordered hierarchies. The reflection principles considered in this paper are formulated relative to G\"odel's constructible universe; we conclude with generalizations to other inner models.

math.LO↗

arXiv2023

The proof-theoretic strength of Constructive Second-order set theories

In this paper, we define constructive analogues of second-order set theories, which we will call $\mathsf{IGB}$, $\mathsf{CGB}$, $\mathsf{IKM}$, and $\mathsf{CKM}$. Each of them can be viewed as $\mathsf{IZF}$- and $\mathsf{CZF}$-analogues of G\"odel-Bernays set theory $\mathsf{GB}$ and Kelley-Morse set theory $\mathsf{KM}$. We also provide their proof-theoretic strengths in terms of classical theories, and we especially prove that $\mathsf{CKM}$ and full Second-Order Arithmetic have the same proof-theoretic strength.

math.LO↗

arXiv2023

On Separating Wholeness Axioms

In this paper, we prove that $\mathsf{ZFC+WA}_{n+1}$ implies the consistency of $\mathsf{ZFC+WA}_n$ for $n\ge 0$. We also prove that $\mathsf{ZFC+WA}_n$ is finitely axiomatizable, and $\mathsf{ZFC+WA}$ is not finitely axiomatizable.

math.LO↗

arXiv2022

Very large set axioms over constructive set theories

We investigate large set axioms defined in terms of elementary embeddings over constructive set theories, focusing on $\mathsf{IKP}$ and $\mathsf{CZF}$. Most previously studied large set axioms, notably the constructive analogues of large cardinals below $0^\sharp$, have proof-theoretic strength weaker than full Second-order Arithmetic. On the other hand, the situation is dramatically different for those defined via elementary embeddings. We show that by adding to $\mathsf{IKP}$ the basic properties of an elementary embedding $j\colon V\to M$ for $\Delta_0$-formulas, which we will denote by $\mathsf{\Delta_0\text{-}BTEE}_M$, we obtain the consistency of $\mathsf{ZFC}$ and more. We will also see that the consistency strength of a Reinhardt set exceeds that of $\mathsf{ZF+WA}$. Furthermore, we will define super Reinhardt sets and $\mathsf{TR}$, which is a constructive analogue of $V$ being totally Reinhardt, and prove that their proof-theoretic strength exceeds that of $\mathsf{ZF}$ with choiceless large cardinals.

math.LO↗

arXiv2021

How strong is a Reinhardt set over extensions of CZF?

We investigate the lower bound of the consistency strength of $\mathsf{CZF}$ with Full Separation $\mathsf{Sep}$ and a Reinhardt set, a constructive analogue of Reinhardt cardinals. We show that $\mathsf{CZF+Sep}$ with a Reinhardt set interprets $\mathsf{ZF^-}$ with a cofinal elementary embedding $j\colon V\prec V$. We also see that $\mathsf{CZF+Sep}$ with a Reinhardt set interprets $\mathsf{ZF^-}$ with a model of $\mathsf{ZF+WA_0}$, the Wholeness axiom for bounded formulas.

math.LO↗

arXiv2020

Constructive Ackermann's interpretation

The main goal of this paper is to formulate a constructive analogue of Ackermann's observation about finite set theory and arithmetic. We will see that Heyting arithmetic is bi-interpretable with $\mathsf{CZF^{fin}}$, the finitary version of $\mathsf{CZF}$. We also examine bi-interpretability between subtheories of finitary $\mathsf{CZF}$ and Heyting arithmetic based on the modification of Fleischmann's hierarchy of formulas, and the set of hereditarily finite sets over $\mathsf{CZF}$, which turns out to be a model of $\mathsf{CZF^{fin}}$ but not a model of finitary $\mathsf{IZF}$.

math.LO↗