Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunctions and infinite disjunctions. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr’s theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.

Abstract The $$\lambda \varPi $$ λ Π -calculus modulo theory is an extension of simply typed $$\lambda $$ λ -calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $$\lambda \varPi $$ λ Π -calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.