Prenex normal form theorems in semi-classical arithmetic

前束范式和公式的层次分类

Prenex normalization and the hierarchical classification of formulas

本文在一阶理论的一般语境中论证了层次前束范式分类的合理性，通过形式化标准变换过程，证明了类 E_k 和 U_k 分别恰为 Σ_k 和 Π_k 经该过程诱导的类。

关于半经典前束范式的分层公式类

Hierarchical formula classes with respect to semi-classical prenex normalization

本文引入具有双参数的一阶公式新类，证明其由第n层半经典前束范式导出，从而在半经典视角下细化了经典前束范式对应的累积公式类。

Epsilon Theorems in Intermediate Logics

Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert's $\varepsilon$-calculus. The first and second $\varepsilon$-theorems for classical logic establish conservativity of the $\varepsilon$-calculus over its classical base logic. It is well known that the second $\varepsilon$-theorem fails for the intuitionistic $\varepsilon$-calculus, as prenexation is impossible. The paper investigates the effect of ad…

Conservation theorems on semi-classical arithmetic

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf{PA}$ and intuitionistic arithmetic $\mathsf{HA}$. Using a generalized negative translation, we first provide a new structured proof of the fact that $\mathsf{PA}$ is $Π_{k+2}$-conservative over $\mathsf{HA} + Σ_k\text{-}\mathrm{LEM}$ where $Σ_k\text{-}\mathrm{LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $Σ_k$. In addition, we show that this conservation theorem is optimal in the sense that for any semi-classical arithmet…

Tame topology of arithmetic quotients and algebraicity of Hodge loci

In this paper we prove the following results: $1)$ We show that any arithmetic quotient of a homogeneous space admits a natural real semi-algebraic structure for which its Hecke correspondences are semi-algebraic. A particularly important example is given by Hodge varieties, which parametrize pure polarized integral Hodge structures. $2)$ We prove that the period map associated to any pure polarized variation of integral Hodge structures $\mathbb{V}$ on a smooth complex quasi-projective variety $S$ is definable with respect to an o-minimal structure on the relevant Hodge variety induced by the…