3 papers
cs.LO2024
Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
Yuta Takahashi
Rathjen proved that Aczel's constructive set theory extended with inaccessible sets of all transfinite orders can be interpreted in Martin-Löf type theory $\mathbf{M…
cs.LO2021
Harmony in the Light of Computational Ludics
Alberto Naibo, Yuta Takahashi
Prawitz formulated the so-called inversion principle as one of the characteristic features of Gentzen's intuitionistic natural deduction. In the literature on proof-theoretic seman…
cs.LO2019
On Quasi Ordinal Diagram Systems
Mitsuhiro Okada, Yuta Takahashi
The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version…