Generalizing realizability and Heyting models for constructive set theory

This article presents a common generalization of the two main methods for obtaining class models of constructive set theory. Heyting models are a generalization of the Boolean models for classical set theory which are a variant of forcing, while realizability is a decidedly constructive method that has first been developed for number theory by Kleene and was later very fruitfully adapted to constructive set theory. In order to achieve the generalization, a new kind of structure (applicative topologies) is introduced, which contains both elements of formal topology and applicative structures. This approach not only deepens the understanding of class models and leads to more efficiency in proofs about these kinds of models, but also makes it possible to prove new results about the two special cases that were not known before and to construct new models.     

The natural numbers in constructive set theory

Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Large sets in intuitionistic set theory

We consider properties of sets in an intuitionistic setting corresponding to large cardinals in classical set theory. Adding such ‘large set axioms’ to intuitionistic ZF set theory does not violate well-know metamathematical properties of intuitionistic systems. Moreover, we consider statements in constructive analysis equivalent to the consistency of such ‘large set axioms’.     

The semantics of realizability for the constructive set theory based on hyperarithmetical predicates

A semantics of realizability based on hyperarithmetical predicates of membership is introduced for formulas of the language of set theory. It is proved that the constructive set theory without the extensionality axiom is sound with this semantics.     

Categorical set theory: A characterization of the category of sets

We consider Zermelo-Fraenkel set theory ZF and the theory ETS(ZF) of the elementary topos of ZF sets, which is an extension of Lawvere-Tierney's theory of elementary topoi, and prove that the theory ETS(ZF) characterizes the category (topos) of ZF-sets in the following sense. The category (topos) of ZF sets satisfies the axioms of ETS(ZF), and conversely we can define within topos theory ETS(ZF) the model of set-objects in which the ZF axiloms hold, and, furthermore, the model of set-objects in the topos of ZF sets is “equivalent” to set theory ZF and the topos of set-objects in ETS(ZF) is “logical equivalent” to topos theory ETS(ZF). Actually, the corresponding result for a weak set theory Z and the theory ETS(Z) of the elementary topos of Z sets is proved. Adding further axioms (axiom of choice, continuum hypothesis, etc.), various results of the same character are obtained.The construction of the model of set-objects uses a universal mapping property of transitive sets, which enables us to introduce transitive-set-objects in any elementary topos and to prove their basic properties.     

A hierarchy of hereditarily finite sets

This article defines a hierarchy on the hereditarily finite sets which reflects the way sets are built up from the empty set by repeated adjunction, the addition to an already existing set of a single new element drawn from the already existing sets. The structure of the lowest levels of this hierarchy is examined, and some results are obtained about the cardinalities of levels of the hierarchy.      

A constructive theory for shock-free,isentropic flow

We construct by finite differences solutions of the Cauchy problem for the nonlinear wave equation in one space dimension. We make certain monotonicity assumptions about the initial data, and we show that the resulting solution is Lipschitz continuous for positive times. In addition, we prove the uniqueness of the solution in a certain class, and we characterize its large-time behavior in terms of the equilibrium state for a corresponding Riemann problem. Finally, we show how our results can be extended to more general 2 × 2 systems of hyperbolic conservation laws which are genuinely nonlinear.     

Canonical form of Tarski sets in Zermelo-Fraenkel set theory

We establish the equivalence of the notions of an inaccessible cumulative set and uncountable Tarski set. In addition, the equivalence of these notions and that of a galactic set is proved.Translated from Matematicheskie Zametki, vol. 77, no. 3, 2005, pp. 323–333.Original Russian Text Copyright © 2005 by E. I. Bunina, V. K. Zakharov.This revised version was published online in April 2005 with a corrected issue number.     

A local hierarchy theory for acyclic digraphs

Local hierarchy theory focuses on direct links in acyclic digraphs. In- and out-degrees are used to determine the local hierarchical number for each vertex in the graph. Together, these local hierarchical numbers form a vector through which hierarchical properties are studied. The main tool, leading to a partial order of acyclic digraphs is a form of generalized Lorenz curve. Gini-like measures respecting this partial order can be derived. Local hierarchy theory is then the theory related to this particular partial order. Results have possible applications in administration and business organizational charts and in citation analysis. In the latter, a direct link represents a reference or a citation of a document. Finally, we study rooted trees as a concrete example of local hierarchy theory.     

Valuation theory: A constructive view

The theory of valuations on fields is developed in the constructive spirit of Errett Bishop. As a consequence of the general theory we are able to construct all nonarchimedean valuations on algebraic number fields and compute their ramification indices and residue class degrees. The notion of a field with a valuation for which the infimum of the values of any polynomial function can be computed plays an important role. Numerous limiting counterexamples are provided.     

Type theories,toposes and constructive set theory: predicative aspects of AST

We introduce a predicative version of topos (stratified pseudotopos) based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.     

A constructive theory of ordered affine geometry

We give a constructive axiomatization of ordered geometry, based on an ordering with directed lines, and using constructions instead of existential axioms. A new duality is found such that, classically, equally and oppositely directed lines turn out dual to parallel and orthogonal lines. Principles such as the axiom of Pasch and ordered versions of the triangle axioms are shown to follow naturally from our approach. Then combinatorial properties of the geometrical plane are studied, and the relation to the usual axiomatization in terms of betweenness is established.     

Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe

We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T₀, thus providing relative lower bounds for the proof-theoretic strength of the latter.     

A constructive proof for a theorem on contractive mappings in power sets

Recently I proved the following theorem: To every positive integer m there exists a positive integer h such that the following holds: If S is a set of h elements and f a mapping of the power set B of S into B such that f(T)?T for all T?B, then there exists a strictly increasing sequence T₁?…?T_m of subsets of S such that one of the following three possibilities holds: (a) All sets f(T_i), i=1,…,m, are equal. (b) For all i=1,…,m we have f(T_i)=T_i (c) T_i=f(T_i+1) for all i=1,…,m?1.The proof given in [2] was non-constructive. In this paper now we give a constructive proof. By the way, this also yields a solution of a problem of Rado [3, p. 106].