A complete axiomatization of higher-order intuitionistic logic
Marcelo E. Coniglio, Cristina Sernadas · 2002
Two Hilbert calculi for higher-order logic (or theory of types) are introduced. The first is defined in a language that uses just exponential types of power type, and it is obtained by adapting the sequent calculus for local set theory introduced by Bell in [3]. The second one, originally introduced in [5], is defined in a language with arbitrary functional types. Using usual topos semantics we show that both systems are sound and complete.