Infinitary first-order categorical logic (Q1625589)

\textit{C. R. Karp} [Languages with expressions of infinite length. Amsterdam: North-Holland Publishing Company (1964; Zbl 0127.00901)] obtained completeness theorems for classical infinitary propositional and first-order logics with Hilbert-type systems, while a related development with Gentzen-type systems were to be seen in [\textit{S. Maehara} and \textit{G. Takeuti}, J. Math. Soc. Japan 13, 357--370 (1962; Zbl 0108.00203)]. \textit{M. E. Nadel} [Ann. Math. Logic 14, 159--191 (1978; Zbl 0406.03055)] developed infinitary intuitionistic propositional logic for countable many conjunctions/disjunctions to establish its completeness with respect to the infinitary version of Kripke semantics. \textit{M. Makkai} [Ann. Pure Appl. Logic 47, No. 3, 225--268 (1990; Zbl 0711.03030)] considered infinitary regular theories together with a corresponding completeness result. The principal objective in this paper is to establish completeness for infinitary intuitionistic propositional and first-order logics with respect to infinitary Kripke semantics, as well as for sheaf and categorical models. The desired completeness is obtained by manipulating sheaf models in place of \textit{L. Henkin}'s method of adding constants [J. Symb. Log. 14, 159--166 (1949; Zbl 0034.00602)]. The crucial contribution is the identification of the transfinite transitivity property, being a generalization of the transitivity property for Grothendieck topologies, as the appropriate categorical property leading to the axiomatic treatment proposed.