A complete axiomatization of infinitary first-order intuitionistic logic over L_{κ⁺, κ}

2018/06/15 by Christian Espíndola, Espíndola, Christian
Computer Science · #Logic, Reasoning, and Knowledge #Formal Methods in Verification #Advanced Algebra and Logic

paper · pdf · doi:10.48550/arxiv.1806.06714

Abstract

Given a weakly compact cardinal κ, we give an axiomatization of intuitionistic first-order logic over 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 L_{ω1, ω}. When κ is a regular cardinal such that κ^

Related

• Logics of Intuitionistic Kripke-Platek Set Theory
• Completeness of infinitary heterogeneous logic
• Realisability for Infinitary Intuitionistic Set Theory
• An intuitionistically complete system of basic intuitionistic conditional logic
• A Note on Extensions of Infinitary Logic