A complete axiomatization of infinitary first-order intuitionistic logic over $\mathcal{L}_{κ^+, κ}$

Abstract

Given a weakly compact cardinal $κ$, we give an axiomatization of intuitionistic first-order logic over $\mathcal{L}_{κ^+, κ}$ and prove it is sound and complete with respect to Kripke models. As a consequence we get the disjunction and existence properties for that logic. This generalizes the work of Nadel for intuitionistic logic over $\mathcal{L}_{ω_1, ω}$. When $κ$ is a regular cardinal such that $κ^{<κ}=κ$, we deduce, by an easy modification of the proof, a complete axiomatization of intuitionistic first-order logic over $\mathcal{L}_{κ^+, κ, κ}$, the language with disjunctions of at most $κ$ formulas, conjunctions of less than $κ$ formulas and quantification on less than $κ$ many variables. In particular, this applies to any regular cardinal under the Generalized Continuum Hypothesis.