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 that the 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 subset G of $\mathcal{X}$ such that for each α ∈ $\mathcal{X}$ , and finitely enumerable subset τ of α there exists a subset β ∈ G such 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 in CZF , 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.

The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Löf’s intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on the problem whether there are (enough) injective sets in CZF. We show that no two element set is injective unless the law of excluded middle is admitted for negated formulas, and that the axiom of power set is required for proving that “there are strongly enough injective sets”. The latter notion is abstracted from the singleton embedding into the power set, which ensures enough injectives both in every topos and in IZF. We further show that it is consistent with CZF to assume that the only injective sets are the singletons. In particular, assuming the consistency of CZF one cannot prove in CZF that there are enough injective sets. As a complement we revisit the duality between injective and projective sets from the point of view of intuitionistic type theory.

The aim of this paper is to formulate and study two weak axiom systems for the conceptual framework of constructive set theory (CST). Arithmetical CST is just strong enough to represent the class of von Neumann natural numbers and its arithmetic so as to interpret Heyting Arithmetic. Rudimentary CST is a very weak subsystem that is just strong enough to represent a constructive version of Jensenʼs rudimentary set theoretic functions and their theory. The paper is a contribution to the study of formal systems for CST that capture significant stages in the development of constructive mathematics in CST.

In a recent note (Palmgren, 2005) Erik Palmgren has shown that, in a sufficiently strong version of Martin-Löf’s type theory (Martin-Löf, 1984) the category of set-presented formal topologies has coequalisers. We refer the reader to (Palmgren, 2005) for the background motivation for this result.

Local Constructive Set Theory (LCST) is intended to be a local version of constructive set theory (CST). Constructive Set Theory is an open-ended set theoretical setting for constructive mathematics that is not committed to any particular brand of constructive mathematics and, by avoiding any built-in choice principles, is also acceptable in topos mathematics, the mathematics that can be carried out in an arbitrary topos with a natural numbers object.

In this paper we analyze the proposals of John Mayberry in his book "The Foundations of Mathematics in the Theory of Sets", especially his idea of solving a problem of more than 200 years: to explain the Foundations of Mathematics.

In this note a T1 formal space (T1 set-generated locale) is a formal space whose points are closed as subspaces. Any regular formal space is T1. We introduce the more general notion of a T1∗ formal space, and prove that the class of points of a weakly set-presentable T1∗ formal space is a set in the constructive set theory CZF. The same also holds in constructive type theory. We then formulate separation properties Ti∗ for constructive topological spaces (ct-spaces), strengthening separation properties discussed elsewhere. Finally we relate the Ti∗ properties for ct-spaces with corresponding properties of formal spaces.

En este trabajo se hace un análisis a las propuestas de John Mayberry en su libro “The Foundations of Mathematics in the Theory of Sets”, especialmente a su idea de resolver un problema de más de 200 años: explicar los fundamentos de las matemáticas.

I state and prove a constructive version of the Lusin Separation Theorem. The classical statement of the theorem is that disjoint analytic sets are Borel separable. The definitions and results are carried out in the axiom system CZF for constructive set theory.

Peter Aczel: Predicate logic over a type setup There are a variety of closely related notions aimed at capturing the abstract structure of type dependency in the syntax and semantics of dependent type theories. Examples of such notions are category with attributes, category with families, category with display maps, contextual category, comprehension category, and there are more. The notion of a type setup is yet one more such notion, which differs from the others in taking a more syntactic approach in its explicit use of contexts, as finite lists of typed variable declarations. This makes it closer to the syntax of dependent type theories, while still abstracting away from the usual inductive structure of syntax and the corresponding recursive definition of substitution. Predicate logic over a type setup is simply defined as a sorted predicate logic where the sorts are the types of the type setup and the sorted terms and substitution are also given by the type setup. Logic over a type setup generalises logic-enriched type theory which, in turn generalises dependently sorted logic, a dependent generalisation of many-sorted logic. Many results of predicate logic generalise to predicate logic over a type setup. I will consider the disjunction and existence properties of intuitionistic predicate logic and end with a characterisation of the logic of the propositions-as-types interpretation of intuitionistic predicate logic. Mark van Atten: Different times: Kant and Brouwer on real numbers Kant held that under the concept of the square root of 2 falls only a geometrical magnitude, but not a number. In particular, he explicitly distinguished the square root of 2 from infinite converging sequences of rationals. Like Kant, Brouwer based his foundations of mathematics on the a priori intuition of time, and indeed he presented his position as fundamentally Kantian. Yet, unlike Kant, Brouwer did identify the square root of 2 with an infinite sequence. The question arises where this difference comes from. I will suggest that it has its origin in the difference in their views on the relation of time to intuition. Steve Awodey: Type theory and homotopy theory In recent research it has become clear that there are deep and fascinating connections between the intensional type theory of Per Martin-Löf and homotopy theory, via the modern approach to the latter in terms of Quillen model categories, as well as the theory of higher dimensional categories. This talk will survey some of these developments. Thierry Coquand: Forcing and type theory Forcing is an important tool in constructive mathematics since it is a general technique to give constructive meaning to some ideal elements. A typical example, that I will recall, is Joyal’s constructive explanation of the algebraic closure of a field. (Even the construction of a splitting field of a polynomial requires this technique.) I will then explain how to adapt this technique to type theory, giving for instance a way to extend type theory with a decidable algebraic closure of a (decidable) field. Peter Dybjer: Program testing and constructive validity In this talk I will discuss the connection between program testing and Martin-Löf's meaning explanations for intuitionistic type theory. First I give a short overview of the historical development of the ideas behind the meaning explanations. Then I explain the connection with program testing. Finally, I will mention the possibility of pursuing the testing point of view for some other logical systems including impredicative ones. Juliet Floyd: Wittgenstein, Gödel and Turing In 1946, recalling his discussions with Turing in Cambridge before the war, Wittgenstein stressed that Turing’s ‘machines’ are really “humans who calculate” (RPP I 1096). Was this intended to embrace or to reject Turing’s model of human calculative activity? What form of anthropomorphism was (and is) at stake in regarding humans as machines, and in playing imitation games? The question becomes even more intriguing when we reflect that while Gödel held that it was Turing’s “precise and unquestionably adequate” definition of the notion of a formal system that allowed his own incompleteness theorems to be proved rigorously for the first time, Gödel also held that Turing made a “philosophical error” in holding that human mental procedures cannot go beyond mechanical procedures. We shall contrast the viewpoints of Wittgenstein, Gödel and Turing, emphasizing the evolution of the logical systems of notation that each one of them provided, and discussing how each viewed the philosophical significance of logic and mathematics. Jean-Yves Girard: Towards non-commutative foundations Quantum physics, operator algebra and the non-commutative geometry of Connes deeply challenge old style foundations. Roughly speaking, the object is entangled, since non-commutative, whereas the subject appears as a commutative window, hence a settheoretic reduction. Issues, partial results, working hypotheses, will be discussed in the talk. Sten Lindström, Church-Fitch’s knowability paradox revisited According to a non-realist conception, the notion of truth is epistemically constrained: the anti-realist accepts one version or another of Dummett’s Knowability Principle: (K) If a statement is true, then it must in principle be possible to know that it is true. There is, however, a well-known argument, due to Alonzo Church and Frederic Fitch, which seems to threaten the anti-realist position. Starting out from seemingly innocuous assumptions, Fitch (JSL 1963) claims to prove: if there is some true proposition which nobody knows to be true, then there is a true proposition which nobody can know to be true. The Church-Fitch argument is simple. Suppose that q is a true proposition that is not known to be true. Consider then the proposition (p): q and it is not known that q. This is obviously a true proposition. And it cannot be known. For suppose that p were known to be true. Then the following proposition would be true: It is known that (q and it is not known that q). Since knowledge distributes over conjunction, it would then also be true that: it is known that q and it is known that it is not known that q. Since knowledge implies truth, it would then follow that it is known that q and it is not known that q. That is, the proposition (p) could not be known to be true. Roughly speaking, we can envisage the following reactions to this argument: • The argument is valid and constitutes a refutation of the anti-realist position. • The argument is valid, but it does not constitute a threat to the anti-realist position. • A detailed analysis of the argument shows it to be invalid. In the talk I plan to discuss these three kinds of reactions to the Knowability argument of Church and Fitch. Per Martin-Löf: Logic: epistemological or ontological? What is logic? Is it the study of the process of inference or reasoning, called demonstration in mathematics, by means of which we justify our judgements? Or is it the study of the logical and set-theoretical concepts, like proposition, truth and consequence on the one hand, and set, element and function on the other, that make their appearance in the contents of our judgements? This is the fundamental question whether logic is in its essence epistemological or ontological. The answer is presumably that it is both, which is to say that, within logic, one can distinguish between two parts, or two layers, the one epistemological and the other ontological. But there remains the question of the order of priority between these two layers: Which comes first? Is epistemology prior to ontology, or is it the other way round? Bolzano, whose logic in four volumes, called Wissenschaftslehre, has the most clear architectonic structure of all logics that have so far been written, treated of the ontological notions of proposition, truth and logical consequence (Ableitbarkeit) in the first two volumes of his Wissenschaftslehre, relegating the epistemology to the third volume. Thus he let ontology take priority over epistemology. Although the line of demarcation between the two was drawn in exactly the right place by Bolzano, my own work on constructive type theory has forced me to the conclusion that the order of priority between ontology and epistemology is nevertheless the reverse of the order in which they are treated in the Wissenschaftslehre. The epistemological notions of judgement and inference have to be in place already when you begin to deal with propositions, truth and consequence, as well as with other purely ontological notions, like the set-theoretical ones. Colin McLarty: What are the things of mathematics? –Identity and existence in categorical foundations Philosophical treatments of identity and existence in mathematics most often take the Zermelo-Frankel conception of extensionality as the norm for individuating objects, which a structuralist account must elude in some way. We will look at the issues with an axiomatic foundation in the category of categories where that kind of individuation is the exception from the start. Peter Pagin: Assertion, truth, and judgment There is an interesting connection between Martin-Löf’s proposition/judgment distinction and a certain puzzle about speech acts. When a speaker asserts (1) The moon reflects light from the sun her assertion is in a sense about its own possible world, even though the proposition she asserts can be evaluated at many worlds. If we treat the world of utterance as an index, we get the content of (2) In w, the moon reflects light from the sun where w gets the world of utterance as value. As a result, the content is either the necessary proposition, if true, or the impossible proposition, if false. This reduces content to truth value. An alternative is to separate the world parameter from the proposition asserted, so that the assertoric content is a distinct entity: (3) w: The moon reflects light from the sun Th

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)

Working in constructive set theory we formulate notions of constructive topological space and set-generated locale so as to get a good constructive general version of the classical Galois adjunction between topological spaces and locales. Our notion of constructive topological space allows for the space to have a class of points that need not be a set. Also our notion of locale allows the locale to have a class of elements that need not be a set. Class sized mathematical structures need to be allowed for in constructive set theory because the powerset axiom and the full separation scheme are necessarily missing from constructive set theory.We also consider the notion of a formal topology, usually treated in Intuitionistic type theory, and show that the category of set-generated locales is equivalent to the category of formal topologies. We exploit ideas of Palmgren and Curi to obtain versions of their results about when the class of formal points of a set-presentable formal topology form a set. (c) 2005 Elsevier B.V. All rights reserved.

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.

Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary re.nement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary re.nement implies that the class of detachable subsets of a set form a set. Binary re.nement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was su.cient to prove that the Dedekind reals form a set. Here we show that the Cauchy reals also form a set. More generally, binary refinement ensures that one remains in the realm of sets when one starts from discrete sets and one applies the operations of exponentiation and binary product a finite number of times.

We describe the final universe approach to the characterisation of semantic universes and illustrate it by giving characterisations of the universes of CCS and CSP processes.

We formulate the notion of a constructive topological space in the constructive set theory CZF. For each i = 0, 1, 2, 3 we formulate three classically equivalent constructive versions of the T-i separation properties; some implications between these are proved, and counterexamples are given to the converse implications. Using a notion of upper real we introduce a variant notion of metric space and examine its relationship with the various separation axioms. Motivated by ideas of Bridges and Vita we also consider some separation properties relative to an inequality.The point-free notion of a formal topology has been developed in the setting of constructive type theory. We introduce this notion in our constructive set theory setting along with a notion of sober constructive topological space and observe that the formal points of a formal topology form a sober constructive topological space. We also introduce a new, constructively weaker, notion of sobriety based on the work of Sambin et al. on the basic picture. In contrast to the standard definition of sobriety, it can be shown constructively that every T-2 space is weakly sober.

Infinite trees form a free completely iterative theory over any given signature--this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(-) + X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees.This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H ⊗ _ + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.

We introduce logic-enriched intuitionistic type theories, that extend intuitionistic dependent type theories with primitive judgements to express logic. By adding type theoretic rules that correspond to the collection axiom schemes of the constructive set theory CZF we obtain a generalisation of the type theoretic interpretation of CZF. Suitable logic-enriched type theories allow also the study of reinterpretations of logic. We end the paper with an application to the double-negation interpretation.