\(\kappa\)-continuous lattices and comprehension principles for Frege structures (Q1104320)

In the paper of the author and \textit{J. Myhill}: ``An extension of Frege structures'' [Mathematical logic and theoretical computer science, Lect. Notes Pure Appl. Math. 106, 197-217 (1987)], we developed a type-free formal system (EFL) extending second-order arithmetic with full comprehension and the axiom of dependent choices. The underlying semantical theory for this system is based on the notion of `\({\mathbb{N}}\)- standard Frege structure' due to \textit{P. Aczel} [The Kleene Symp., Proc., Madison/Wis. 1978, Stud. Logic Found. Math. 101, 31-59 (1980; Zbl 0462.03002)]. The main feature of (EFL), beyond a natural codification of Frege structures is the presence of a new comprehension principle. Informally this principle says that if A is a discrete class, then any functional relation with domain A is represented by a function of the system. A class is discrete if the equality relation restricted to it has a characteristic function. We can develop a considerable amount of analysis within (EFL). However, as \textit{S. Feferman} [Handbook of mathematical logic, 913-971 (1977; Zbl 0443.03001)] observes, to formalize ordinary mathematical practice we need full comprehension also for type one objects. Thus, as a foundation for mathematics, (EFL) is inadequate. In the last section of our companion paper with \textit{J. Myhill} [loc. cit.], we proposed extensions of (EFL) which would be more satisfactory from a fundational point of view. Essentially, these extensions consist of adding axioms asserting that the collection of discrete classes is closed under the natural set theoretic constructions needed in practice; e.g., disjoint unions, products and exponentials. The purpose of the present paper is to show the consistency of these extended systems.