Ternary Operations as Primitive Notions for Constructive Plane Geometry VI

In this paper we provide quantifier-free, constructive axiomatizations for several fragments of plane Euclidean geometry over Euclidean fields, such that each axiom contains at most 4 variables. The languages in which they are expressed contain only at most ternary operations. In some precisely defined sense these axiomatizations are the simplest possible.     

Refinement is equivalent to Fullness

In the article [4], a new constructive set theoretic principle called Refinement was introduced and analysed. While it seemed to be significantly weaker than its alternative, the more established axiom of Fullness (a constructive version of the Powerset axiom from classical set theory), it was shown to suffice to imply many of the mathematically important consequences. In this article, we will define for each set A a set of truth values which measures the complexity of the equality relation on A. Using these sets we will show that Refinement is actually equivalent to Fullness on the basis of the other axioms of constructive Zermelo‐Fraenkel set theory (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Constructive Axiomatizations of Plane Absolute,Euclidean and Hyperbolic Geometry

In this paper we provide quantifier‐free, constructive axiomatizations for 2‐dimensional absolute, Euclidean, and hyperbolic geometry. The main novelty consists in the first‐order languages in which the axiom systems are formulated.     

On the constructive Dedekind reals

In order to build the collection of Cauchy reals as a set in constructive set theory, the only power set-like principle needed is exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, Constructive Zermelo–Fraenkel set theory with subset collection replaced by exponentiation, in which the Cauchy reals form a set while the Dedekind reals constitute a proper class.     

A minimalist two-level foundation for constructive mathematics

We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin.One level is given by an intensional type theory, called Minimal type theory. This theory extends a previous version with collections.The other level is given by an extensional set theory that is interpreted in the first one by means of a quotient model.This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the “proofs-as-programs” paradigm and acts as a programming language.     

The strength of Martin-Löf type theory with a superuniverse. Part I

Universes of types were introduced into constructive type theory by Martin-L?f [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say . The universe then “reflects”. This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]). It is proved that Martin-L?f type theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal but well below the Bachmann-Howard ordinal. Not many theories of strength between and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. Received: 14 October 1997     

The Relation Reflection Scheme

We introduce a new axiom scheme for constructive set theory, the Relation Reflection Scheme (RRS). Each instance of this scheme is a theorem of the classical set theory ZF. In the constructive set theory CZF^–, when the axiom scheme is combined with the axiom of Dependent Choices (DC), the result is equivalent to the scheme of Relative Dependent Choices (RDC). In contrast to RDC, the scheme RRS is preserved in Heyting‐valued models of CZF^– using set‐generated frames. We give an application of the scheme to coinductive definitions of classes. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Realizing Mahlo set theory in type theory

 After introducing the large set notion of Mahloness, this paper shows that constructive set theory with an axiom asserting the existence of a Mahlo set has a realizability interpretation in an extension of Martin-L?f type theory developed by A. Setzer. Received: 5 September 2000 Published online: 19 December 2002     

Constructive theory of enumerable species

A constructive semantics for the language of set theory with atoms based on interpreting set variables by enumerable species is defined. The soundness of the axioms of the Zermelo–Fraenkel set theory with this semantics is completely studied.     

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.     

On Commutative and Nonassociative Syntactic Calculi and Categorial Grammars

Two axiomatizations of the nonassociative and commutative Lambek syntactic calculus are given and their equivalence is proved. The first axiomatization employs Permutation as the only structural rule, the second one, with no Permutation rule, employs only unidirectional types. It is also shown that in the case of the Ajdukiewicz calculus an analogous equivalence is valid only in the case of a restricted set of formulas. Unidirectional axiomatizations are employed in order to establish the generative power of categorial grammars based on the nonassociative and commutative Lambek calculus with product. Those grammars produce CF-languages of finite degree generated by CF-grammars closed with respect to permutations.     

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.     

Equivalents of the finitary non-deterministic inductive definitions

We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of constructive set theory CZF. We show that several statements in constructive topology which were initially proved using NID are equivalent to the elementary and finitary NIDs. We also show that the finitary NID is equivalent to its binary fragment and that the elementary NID is equivalent to a variant of NID based on the notion of biclosed subset. Our result suggests that proving these statements in constructive topology requires genuine extensions of CZF with the elementary or finitary NID.     

On some peculiar aspects of the constructive theory of point‐free spaces

This paper presents several independence results concerning the topos‐valid and the intuitionistic (generalised) predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Axioms for function semigroups with agreement quasi-order

The agreement quasi-order on pairs of (partial) transformations on a set X is defined as follows: ${(f, g) \preceq (h, k)}$ if whenever f, g are defined and agree, so do h, k. We axiomatize function semigroups and monoids equipped with this quasi-order, thereby providing a generalisation of first projection quasi-ordered ${\cap}$ -semigroups of functions. As an application, axiomatizations are obtained for groups and inverse semigroups of injective functions equipped with the quasi-order of fix-set inclusion. All axiomatizations are finite.     

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’.     

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.     

The strength of Martin-Löf type theory with a superuniverse. Part II

Universes of types were introduced into constructive type theory by Martin-L?f [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?. This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]). It is proved that Martin-L?f type theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal Γ₀ but well below the Bachmann-Howard ordinal. Not many theories of strength between Γ₀ and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. In this second part of the paper the concern is with the with upper bounds. Received: 8 December 1998 / Published online: 21 March 2001     

The shrinking principle and the axiom of choice

The axiom of choice is equivalent to the shrinking principle: every indexed cover of a set has a refinement with the same index set which is a partition. A simple and direct proof of this equivalence is given within an elementary fragment of constructive Zermelo–Fraenkel set theory. Variants of the shrinking principle are discussed, and it is related to a similar but different principle formulated by Vaught.     

The shrinking principle and the axiom of choice

The axiom of choice is equivalent to the shrinking principle: every indexed cover of a set has a refinement with the same index set which is a partition. A simple and direct proof of this equivalence is given within an elementary fragment of constructive Zermelo–Fraenkel set theory. Variants of the shrinking principle are discussed, and it is related to a similar but different principle formulated by Vaught.