A complete axiomatization of infinitary first-order intuitionistic logic over $\mathcal{L}_{κ^+, κ}$
Christian Espíndola · arXiv (Cornell University) · 2018
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 $κ^{