We introduce infinitary propositional theories over a set and their models which are subsets of the set, and define a generalized geometric theory as an infinitary propositional theory of a special form. The main result is thatthe class of models of a generalized geometric theory is set-generated. Here, a class $\mathcal{X}$ of subsets of a set is set-generated if there exists a subsetGof $\mathcal{X}$ such that for each α ∈ $\mathcal{X}$ , and finitely enumerable subset τ of α there exists a subset β ∈Gsuch that τ ⊆ β ⊆ α. We show the main result in the constructive Zermelo–Fraenkel set theory (CZF) with an additional axiom, called the set generation axiom which is derivable inCZF, both from the relativized dependent choice scheme and from a regular extension axiom. We give some applications of the main result to algebra, topology and formal topology.

Abstract We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.

In his 1903, Principles of Mathematics, Bertrand Russell mentioned possible definitions of conjunction, disjunction, negation and existential quantification in terms of implication and universal quantification, exploiting impredicative universal quantifiers over all propositions. In his 1965 Ph.D. thesis Dag Prawitz showed that these definitions hold in intuitionistic second order logic. More recently, these definitions have been used to represent logic in various impredicative type theories. This treatment of logic is distinct from the more standard Curry–Howard representation of logic in a dependent type theory.The main aim of this paper is to compare, in a purely logical, non type-theoretic setting, this Russell–Prawitz representation of intuitionistic logic with other possible representations. It turns out that associated with the Russell–Prawitz representation is a lax modal operator, which we call the Russell–Prawitz modality, and that any lax modal operator can be used to give a translation of intuitionistic logic into itself that generalises both the double negation interpretation, double negation being a paradigm example of a lax modality, and the Russell–Prawitz representation.

A generalization of a version of order-sorted logic and an abstract axiomatic setting for the treatment of substitution are given. The two ideas are shown to be related, an equational specification of term declaration logic being a presentation of a finitary generalized composition. The automatic approach to substitution is compared with some other approaches. The relationship between algebraic theories and standard equational logic is reviewed. One of the aims is to lay the foundations for a generalization of these connections to connections between term declaration logic and finitary generalized composita and a suitable generalization of algebraic theories.>

A precise notion of a formal framework, meant to capture the intuition of an open-ended range of deductive interpreted languages, is proposed. A particular framework called the logical theory of constructions (LTC) is developed as an example. A series of languages in the LTC framework is defined, demonstrating how a language can be thought of as gradually evolving.>

Bachmann, in [2] shows how certain ordinals <Ω(Ω = Ω1 where Ωξ is the (1 + ξ)th infinite initial ordinal) may be described from below using suitable descriptions of ordinals <Ω2. The aim of this paper is to consider another approach to describing ordinal <Ω and compare it with the Bachmann method. Our approach will use functionals of transfinite type based on Ω. The Bachmann method consists in denning a hierarchy of normal functions ϕδ: Ω → Ω (i.e. continuous and strictly increasing) for δ ≤ η0 < Ω2, starting with ϕ0(λ) = ω1 + λ. The definition of depends on a suitable description of the ordinals ≤ η0. This is obtained by defining a hierarchy 〈Fδ ∣ δ ≤ Ω2〉 of normal functions Fδ: Ω2 → Ω2 analogously to the definition of the initial segment 〈ϕδ ∣ δ ≤ Ω〉 of . The ordinal η0 is . Note. Our description of Bachmann's hierarchies will differ slightly from those in Bachmann's paper. Let and denote the hierarchies in [2]. Then as Bachmann's normal functions are not defined at 0 we let for λ, δ < Ω2. Bachmann defines for 0 < λ < Ω2 but it seems more natural to omit this so that we let . The situation is analogous for and leads to the following definitions: where n < ω and ξ is a limit number of cofinality Ω, and