arXiv subjects

Hanul Jeon

Publications and source records attributed to Hanul Jeon.

13 recordsLinked to original sources

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↗

arXiv2026

Dilator-based analysis of KP

Proof theorists developed various frameworks to analyze impredicative systems like $Π^1_1\text{-}\mathsf{CA}_0$ or $\mathsf{KP}$; One is an operator-controlled derivation system, and the other is Girard's dilator-based $β$-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 $Σ_1$-over-$L_{ω_1^{\mathsf{CK}}}$-definable function $ω_1^\mathsf{CK}\to ω_1^\mathsf{CK}$ is bounded by a recursive dilator.

math.LO↗

arXiv2026

Ranking theories via encoded $β$-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 $β$-models: $T\prec_βU$ if every $β$-model of $U$ contains a countable coded $β$-model of $T$. The restriction of $\prec_β$ to theories with $β$-models is well-founded. We establish fundamental properties of the attendant ranking. First, though there are continuum-many theories, every theory has countable $\prec_β$-rank. Second, the $\prec_β$-ranks of $\mathcal{L}_\in$ theories are cofinal in $ω_1$. Third, assuming $V=L$, the $\prec_β$-ranks of $\mathcal{L}_2$ theories are cofinal in $ω_1$. Finally, $δ^1_2$ is the supremum of the $\prec_β$-ranks of finitely axiomatized theories.

math.LO↗

arXiv2026

Proof-theoretic dilator and intermediate pointclasses

There are two major generalizations of the standard ordinal analysis: One is Girard's $Π^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 $ω_1^{\mathsf{CK}}$ are assigned to theories. In this paper, we show that these two are systematically entangled, and $Σ^1_2$-proof theoretic analysis has a critical role in connecting these two.

math.LO↗

arXiv2026

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

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

math.LO↗

arXiv2025

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ödel-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↗

arXiv2025

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_{λ+2}\to V_{λ+2}$.

math.LO↗

arXiv2025

Martin's measurable dilator

Martin's remarkable proof of $\mathbfΠ^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Π^1_2$-determinacy, which captures the structural essence of Martin's proof of $\mathbfΠ^1_2$-determinacy.

math.LO↗

arXiv2025

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 $Δ_0$-formulas, which we will denote by $\mathsf{Δ_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↗

arXiv2025

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↗

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ödel's constructible universe; we conclude with generalizations to other inner models.

math.LO↗

arXiv2022

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↗

arXiv2022

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↗