A class of toposes is introduced and studied, suitable for semantical analysis of an extension of the Heyting predicate calculus admitting Gödel's provability interpretation.

The purpose of this paper is to justify the claim that Topos theory and Logic (the latter interpreted in a wide enough sense to include Model theory and Set theory) may interact to the advantage of both fields. Once the necessity of utilizing toposes (other than the topos of Sets) becomes apparent, workers in Topos theory try to make this task as easy as possible by employing a variety of methods which, in the last instance, find their justification in (...) metatheorems from Logic. Some concrete instances of this assertion will be given in the form of simple proofs that certain theorems of Algebra hold in any (Grothendieck) topos, in order to illustrate the various techniques that are used. In the other direction, Topos theory can also be a useful tool in Logic. Examples of this are independence proofs in (classical as well as intuitionistic) Set theory, as well as transfer methods in the presence of a sheaf representation theorem, the latter applied, in particular, to model theoretic properties of certain theories. (shrink)

For 20th century mathematicians, the role of Cantor's sets has been that of the ideally featureless canvases on which all needed algebraic and geometrical structures can be painted. (Certain passages in Cantor's writings refer to this role.) Clearly, the resulting contradication, 'the points of such sets are distinc yet indistinguishable', should not lead to inconsistency. Indeed, the productive nature of this dialectic is made explicit by a method fruitful in other parts of mathematics (see 'Adjointness in Foundations', Dialectia 1969). This (...) role of Cantor's theory is compared with the role of Galois theory in algebraic geometry. (shrink)

Steve Awodey and Audrej Bauer. Sheaf Toposes for Realizability.

This book introduces a set of methods and techniques for studying mathematical theories and relating them to each other through the use of Grothendieck toposes.

By a classifying topos for a first-order theory , we mean a topos such that, for any topos models of in correspond exactly to open geometric morphisms → . We show that not every first-order theory has a classifying topos in this sense, but we characterize those which do by an appropriate ‘smallness condition’, and we show that every Grothendieck topos arises as the classifying topos of such a theory. We also show that every first-order theory has a conservative extension (...) to one which possesses a classifying topos, and we obtain a Heyting-valued completeness theorem for infinitary first-order logic. (shrink)

This paper is an introduction to topos theory which assumes no prior knowledge of category theory. It includes a discussion of internal logic in a topos, A characterization of the category of sets, And an investigation of the notions of topology and sheaf in a topos.

The aim of this paper is to introduce a new approach to the modal operators of necessity and possibility. This approach is based on the existence of two negations in certain lattices that we call bi-Heyting algebras. Modal operators are obtained by iterating certain combinations of these negations and going to the limit. Examples of these operators are given by means of graphs.

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. (...) The resulting framework is intended as a setting for the logical and categorical study of relative computability. (shrink)

We introduce a predicative version of topos 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.

Now available in paperback, this acclaimed book introduces categories and elementary toposes in a manner requiring little mathematical background. It defines the key concepts and gives complete elementary proofs of theorems, including the fundamental theorem of toposes and the sheafification theorem. It ends with topos theoretic descriptions of sets, of basic differential geometry, and of recursive analysis.

ABSTRACT We present a new method for proving theorems in the equational theory of partial maps over toposes introduced in the papers [C'089] and [086], The method is given by a system of rules of formation of proofs. The proofs of f is defined' and the proofs of correctness ‘φ)' formed by application of the rules of the system are such that they contain a computation of the value f, where f is a partial function valued in natural numbers (...) and is a vector of natural numbers. We show that the system is complete, i.e. if an equation holds in every model then it has a proof formed by application of the rules of the system. The system is equipped with a method of visual presentation of proofs by nested commutative triangles, i.e. commutative triangles which contain in their interiors other commutative triangles which may be also nested. To provide formal foundations for the method of visual presentation of proofs we give a mathematical description of nested commutative triangles in terms of directed graphs and graph homomorphisms. AMS Subject Classification 1995: Primary: 68. Secondary: 18. (shrink)

This book is written for those who are in sympathy with its spirit. This spirit is different from the one which informs the vast stream of European and American civilization in which all of us stand. That spirit expresses itself in an onwards movement, in building ever larger and more complicated structures; the other in striving in clarity and perspicuity in no matter what structure. The first tries to grasp the world by way of its periphery—in its variety; the second (...) at its centre—in its essence. And so the first adds one construction to another, moving on and up, as it were, from one thing to the next, while the other remains where it is and what it tries to grasp is always the same. (shrink)

We describe a method for presenting (a topos closely related to) either of Freyd’s topos-theoretic models for the independence of the axiom of choice as the classifying topos for a geometric theory. As an application, we show that no such topos can admit a geometric morphism from a two-valued topos satisfying countable dependent choice.

In 1996, W. Veldman and F. Waaldijk present a constructive (intuitionistic) proof for the homogeneity of the ordered structure of the Cauchy real numbers, and so this result holds in any topos with natural number object. However, it is well known that the real numbers objects obtained by the traditional constructions of Cauchy sequences and Dedekind cuts are not necessarily isomorphic in an arbitrary topos with natural numbers object. Consequently, Veldman and Waaldijk's result does not apply to the ordered structure (...) of Dedekind real numbers in toposes. The main result to be proved in the present paper is that the ordered structure of the Dedekind real numbers object is homogeneous, in any topos with natural numbers object. This result is obtained within the framework of local set theory. (shrink)

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions . As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the (...) full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo-Fraenkel set theory. (shrink)

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the (...) full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo—Fraenkel set theory (IZF). (shrink)

The topos theory gives tools for unified proofs of theorems for model theory for various semantics and logics. We introduce the notion of power and the notion of generalized quantifier in topos and we formulate sufficient condition for such quantifiers in order that they fulfil downward Skolem-Löwenheim theorem when added to the language. In the next paper, in print, we will show that this sufficient condition is fulfilled in a vast class of Grothendieck toposes for the general and the (...) existential quantifiers. (shrink)

We present a complete elementary axiomatization of local maps of toposes.

This paper is a continuation of the investigation from [13]. The main theorem states that the general and the existential quantifiers are (, -reducible in some Grothendieck toposes. Using this result and Theorems 4.1, 4.2 [13] we get the downward Skolem-Löwenheim theorem for semantics in these toposes.

A topos version of Cantor’s back and forth theorem is established and used to prove that the ordered structure of the rational numbers (Q, <) is homogeneous in any topos with natural numbers object. The notion of effective homogeneity is introduced, and it is shown that (Q, <) is a minimal effectively homogeneous structure, that is, it can be embedded in every other effectively homogeneous ordered structure.

Assuming some extra structure we simplify the characterization of the categories with finite limits whose exact completions are toposes given in Menni . This simplification allows us to obtain new examples and non-examples and also to provide a new perspective and an alternative proof of recent results on the inevitability of untypedness for realizability toposes.

We give an explicit construction of the dependent product in an elementary topos, and a site‐theoretic description for it in the case of a Grothendieck topos. Along the way, we obtain a number of results of independent interest, including an expression for the operation of universal quantification on subobjects in terms of finite limits and power objects.

Categorical-theoretic semantics for the relevance logic is proposed which is based on the construction of the topos of functors from a relevant algebra (considered as a preorder category endowed with the special endofunctors) in the category of sets Set. The completeness of the relevant system R of entailment is proved in respect to the semantic considered.

The view that toposes originated as generalized set theory is a figment of set theoretically educated common sense. This false history obstructs understanding of category theory and especially of categorical foundations for mathematics. Problems in geometry, topology, and related algebra led to categories and toposes. Elementary toposes arose when Lawvere's interest in the foundations of physics and Tierney's in the foundations of topology led both to study Grothendieck's foundations for algebraic geometry. I end with remarks on a (...) categorical view of the history of set theory, including a false history plausible from that point of view that would make it helpful to introduce toposes as a generalization from set theory. (shrink)

Newton's Principia introduced conceptions of space and time that launched one of themost famous and sustained debates in the history of physics, a controversy that involves fundamentalconcerns in the foundations of physics, metaphysics, and scientific epistemology.This bookintroduces and clarifies the historical and philosophical development of the clash between Newton'sabsolute conception of space and Leibniz's relational one. It separates the issues and provides newperspectives on absolute relational accounts of motion and relational-substantival accounts of theontology of space time.Earman's sustained treatment and imaginative (...) insights raise to a new levelthe debate on these important issues at the boundary of philosophy and physics. He surveys thehistory of the controversy from Newton to Einstein develops the mathematics and physics needed topose the issues in sharp form and provides a persuasive assessment of the philosophical problemsinvolved.Most importantly, Earman revitalizes the connection of the debate to contemporary science.He shows, for example, how concerns raised by Leibniz form the core of ongoing debate on thefoundations of general theory of relativity, moving the discussion into a new and vital arena andintroducing arguments that will be discussed for years to come.John Earman is Professor of Historyand Philosophy of Science at the University of Pittsburgh. A Bradford Book. (shrink)

The classical forms of both modified realizability and relative realizability are naturally described in terms of the Sierpinski topos. The paper puts these two observations together and explains abstractly the existence of the geometric morphisms and logical functors connecting the various toposes at issue. This is done by advancing the theory of triposes over internal partial combinatory algebras and by employing a novel notion of elementary map.

Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality. We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals (...) grow very rapidly. Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it. We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank. The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area. Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy. Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result. (shrink)

Purpose. The article highlights the demand for critical thinking in everyday life at the present stage of development of globalized culture and emphasizes the role of philosophy as a source of rationality. Philosophizing, which is determined by the psychosociocultural matrix, sets the toposes, vocabulary and rhythms of meaning making, their preservation and transformation. The purpose of the article is to concretize the practices of socio-cultural communication, primarily through the social institute of education, where individuals interact with the psychosociocultural matrix (...) of philosophizing, which mediate the general and individual level in philosophical culture. Theoretical basis of the study are cultural anthropology and phenomenological methods. Originality of the study: based on the philosophy of intersubjectivity, we actualized the rational grounds for formation of adequate judgments in modern culture at the level of everyday life. This justifies the inevitability of the spread of various forms and types of philosophical education, philosophical thinking, ideas and values developed in philosophical communities beyond the narrow circle of professional philosophers. This implies the systemic involvement of philosophers as professionals of meaning-making in solving problems in various non-academic fields – politics, economics, law, etc. The formation of skills of philosophical critical thinking in the process of preparing young people for active civil life is no less important aspect of this. Conclusions lead to an understanding of the existential importance of philosophy and philosophizing and the need for organized forms of knowledge transfer such as the Faculty of Philosophy of the Classical University. There is a mutual interest and interaction of the general culture of society and philosophy as a special kind of culture. Because philosophy actively configures other forms of culture, contributes to the creation of sociocultural identities precisely because of its ability to conceptually reproduce the core of the psychosociocultural matrix that underlies the existence of all these different forms within one society. The sociocultural macro level of philosophical spiritual practices is formed by the psychosociocultural matrix of the philosophical tradition, which retains its longevity from the emergence of philosophy and goes through its history, demonstrating the features of the national reception of philosophy as a national-specific embodiment of sociocultural macro level of the psychosociocultural matrix. (shrink)