4 papers
math.LO2026
Dilator-based analysis of KP
Hanul Jeon
Proof theorists developed various frameworks to analyze impredicative systems like or ; One is an operator-controlled derivation system, a…
math.LO2026
The Axiom of Double Complement and its opposites
Hanul Jeon, James E. Hanson
Powell introduced the Axiom of Double Complement () to give his double-negation interpretation of into . However, the consistency,…
math.LO2023
The proof-theoretic strength of Constructive Second-order set theories
Hanul Jeon
In this paper, we define constructive analogues of second-order set theories, which we will call , , , and . Each of them ca…
math.LO2020
Constructive Ackermann's interpretation
Hanul Jeon
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-int…