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. (shrink)

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

We introduce a new axiom scheme for constructive set theory, the Relation Reflection Scheme . 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 , the result is equivalent to the scheme of Relative Dependent Choices . 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. (shrink)

Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary refinement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary refinement implies that the class of detachable subsets of a set form a set. Binary refinement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was sufficient 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. (shrink)

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. (shrink)

The aim of this paper is to formulate and study two weak axiom systems for the conceptual framework of constructive set theory . 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. (shrink)

Situation Theory and Its Applications, Vol. 1 . Robin Cooper, Kuniaki Mukai, and John Perry (Eds.). Lecture Notes No. 22. ...

This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.

Situation theory is the result of an interdisciplinary effort to create a full-fledged theory of information. Created by scholars and scientists from cognitive science, computer science and AI, linguistics, logic, philosophy, and mathematics, it aims to provide a common set of tools for the analysis of phenomena from all these fields. Unlike Shannon-Weaver type theories of information, which are purely quantitative theories, situation theory aims at providing tools for the analysis of the specific content of a situation. The question addressed (...) is not how much information is carried, but what information is carried. (shrink)

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.

The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe á la Tarski. A set U 0 of codes for small sets is generated inductively at the same time as a function T 0 , which maps a code to the corresponding small set, is defined by recursion on the way the elements of U 0 are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is (...) implicit in Martin-Löf's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous induction-recursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen. (shrink)

Some propositions add more information to bodies of propositions than do others. We start with intuitive considerations on qualitative comparisons of information added . Central to these are considerations bearing on conjunctions and on negations. We find that we can discern two distinct, incompatible, notions of information added. From the comparative notions we pass to quantitative measurement of information added. In this we borrow heavily from the literature on quantitative representations of qualitative, comparative conditional probability. We look at two ways (...) to obtain a quantitative conception of information added. One, the most direct, mirrors Bernard Koopman’s construction of conditional probability: by making a strong structural assumption, it leads to a measure that is, transparently, some function of a function P which is, formally, an assignment of conditional probability (in fact, a Popper function). P reverses the information added order and mislocates the natural zero of the scale so some transformation of this scale is needed but the derivation of P falls out so readily that no particular transformation suggests itself. The Cox–Good–Aczél method assumes the existence of a quantitative measure matching the qualitative relation, and builds on the structural constraints to obtain a measure of information that can be rescaled as, formally, an assignment of conditional probability. A classical result of Cantor’s, subsequently strengthened by Debreu, goes some way towards justifying the assumption of the existence of a quantitative scale. What the two approaches give us is a pointer towards a novel interpretation of probability as a rescaling of a measure of information added. (shrink)

In this groundbreaking editorial and curatorial project, more than 100 writers, artists, and philosophers rethink what politics is about. In a time of political turmoil and anticlimax, this book redefines politics as operating in the realm of things. Politics is not just an arena, a profession, or a system, but a concern for things brought to the attention of the fluid and expansive constituency of the public. But how are things made public? What, we might ask, is a republic, a (...) res publica, a public thing, if we do not know how to make things public? There are many other kinds of assemblies, which are not political in the usual sense, that gather a public around things—scientific laboratories, supermarkets, churches, and disputes involving natural resources like rivers, landscapes, and air. The authors of Making Things Public—and the ZKM show that the book accompanies—ask what would happen if politics revolved around disputed things. Instead of looking for democracy only in the official sphere of professional politics, they examine the new atmospheric conditions—technologies, interfaces, platforms, networks, and mediations that allow things to be made public. They show us that the old definition of politics is too narrow; there are many techniques of representation—in politics, science, and art—of which Parliaments and Congresses are only a part. The authors include such prominent thinkers as Richard Rorty, Simon Schaffer, Peter Galison, Richard Powers, Lorraine Daston, Richard Aczel, and Donna Haraway; their writings are accompanied by excerpts from John Dewey, Shakespeare, Swift, La Fontaine, and Melville. More than 500 color images document the new idea of what Bruno Latour and Peter Weibel call an "object-oriented democracy.". (shrink)

The Dedekind cuts in an ordered set form a set in the sense of constructive Zermelo—Fraenkel set theory. We deduce this statement from the principle of refinement, which we distill before from the axiom of fullness. Together with exponentiation, refinement is equivalent to fullness. None of the defining properties of an ordering is needed, and only refinement for two—element coverings is used. In particular, the Dedekind reals form a set; whence we have also refined an earlier result by Aczel (...) and Rathjen, who invoked the full form of fullness. To further generalise this, we look at Richman's method to complete an arbitrary metric space without sequences, which he designed to avoid countable choice. The completion of a separable metric space turns out to be a set even if the original space is a proper class; in particular, every complete separable metric space automatically is a set. (shrink)

As I write this, in November 1971, people are dying in East Bengal from lack of food, shelter, and medical caxc. The suffering and death that are occurring there now axe not inevitable, 1101; unavoidable in any fatalistic sense of the term. Constant poverty, a cyclone, and a civil war have turned at least nine million people into destitute refugees; nevertheless, it is not beyond Lhe capacity of the richer nations to give enough assistance to reduce any further suffering to (...) very small proportions. The decisions arid actions of human beings can prevent this kind of suffering. Unfortunately, human beings have not made the necessary decisions. At the individual level, people have, with very few exceptions, not responded to the situation in any signihczmt way. Generally speaking, people have not given large sums to relief funds; they have not written t0 their parliamentaxy representatives demanding increased government assistance; they have not demonstrated in the streets, held symbolic fasts, or done anything else directed toward providing thc refugees with the means to satisfy their essential needs. At thc government level, no govcrmmcnt has given the sort of massive aid that would enable the refugees to survive fm: more than a few days. Britain, for instance, has given rather more than most countries. It has, to date, given £14,750,000. For comparative purposes, B1~itain’s share of thc nonreccverabla development costs of the Anglo-French Concorde project is already in excess of £275,000,000, and on present estimates will reach £440,000,¤00. The implication is that the British government values a supersonic transport more than thirty times as.. (shrink)

ABSTRACTThe general assumption that people fail to notice discrepancy between their answer and the normative answer in the conjunction fallacy task has been challenged by the theory of Logical Intuition. This theory suggests that people can detect the conflict between the heuristic and normative answers even if they do not always manage to inhibit their intuitive choice. This theory gained support from the finding that people report lower levels of confidence in their choice after they commit the conjunction fallacy compared (...) to when their answer is not in conflict with logic. In four experiments we asked the participants to give probability estimations to the options of the conflict and no-conflict versions of the tasks in the original set-up of the experiment or in a three-option design. We found that participants perceive probabilities for the options of the conflict version less similar than for the no-conflict version. As people are less confident when choosing between more similar options, this simil.. (shrink)

This paper argues that a set of questioning attitudes are among the foundations of human and animal minds. While both verbal questioning and states of curiosity are generally explained in terms of metacognitive desires for knowledge or true belief, I argue that each is better explained by a prelinguistic sui generis type of mental attitude of questioning. I review a range of considerations in support of such a proposal and improve on previous characterizations of the nature of these attitudes. I (...) then broaden their explanatory scope to include a number of forms of exploratory search. The paper has three main goals: to characterize the nature of the questioning attitudes, outlining their causal role and type of content; to argue that they are fundamental components of the mind, being widespread among animals and not constructed during ontogeny out of other attitudes; and to suggest that they explain a great deal more behavior than one might think. (shrink)

Since its original publication in 1975, this groundbreaking work has awakened millions of people to the existence of "speciesism"—our systematic disregard of nonhuman animals—inspiring a worldwide movement to transform our attitudes to animals and eliminate the cruelty we inflict on them. In Animal Liberation, author Peter Singer exposes the chilling realities of today’s "factory farms" and product-testing procedures—destroying the spurious justifications behind them, and offering alternatives to what has become a profound environmental and social as well as moral issue. (...) An important and persuasive appeal to conscience, fairness, decency, and justice, it is essential reading for the supporter and the skeptic alike. (shrink)

We propose a solution to the problem of logical omniscience in what we take to be its fundamental version: as concerning arbitrary agents and the knowledge attitude per se. Our logic of knowledge is a spin-off from a general theory of thick content, whereby the content of a sentence has two components: an intension, taking care of truth conditions; and a topic, taking care of subject matter. We present a list of plausible logical validities and invalidities for the logic of (...) knowledge per se for arbitrary agents, and isolate three explanatory factors for them: the topic-sensitivity of content; the fragmentation of knowledge states; the defeasibility of knowledge acquisition. We then present a novel dynamic epistemic logic that yields precisely the desired validities and invalidities, for which we provide expressivity and completeness results. We contrast this with related systems and address possible objections. (shrink)

Single-premise epistemic closure is the principle that: if one is in an evidential position to know that P where P entails Q, then one is in an evidential position to know that Q. In this paper, I defend the viability of opposition to closure. A key task for such an opponent is to precisely formulate a restricted closure principle that remains true to the motivations for abandoning unrestricted closure but does not endorse particularly egregious instances of closure violation. I focus (...) on two brands of epistemic theory that naturally incorporate closure restrictions. The first type holds that the truth value of a knowledge ascription is relative to a relevant question. The second holds that the truth value of a knowledge ascription is relative to a relevant topic. For each approach, I offer a formalization of a leading theory from the literature and use this formalization to evaluate the theory’s adequacy in terms of a precise set of desiderata. I conclude that neither theory succeeds in meeting these desiderata, casting doubt on the viability of the underlying approaches. Finally, I offer a novel variant of the topic-sensitive approach that fares better. (shrink)

From the end of the 19th century until his death, one of history's most brilliant mathematicians languished in an asylum. The Mystery of the Aleph tells the story of Georg Cantor (1845-1918), a Russian-born German who created set theory, the concept of infinite numbers, and the "continuum hypothesis," which challenged the very foundations of mathematics. His ideas brought expected denunciation from established corners - he was called a "corruptor of youth" not only for his work in mathematics, but for his (...) larger attempts to meld spirituality and science. (shrink)

Introduction These essays have been written over a period of about ten years and have already been published separately in various places. ...

I lay out the framework for my theory of sensory imagination in “Imagining as a guide to possibility.” Sensory imagining involves mental imagery , and crucially, in describing the content of imagining, I distinguish between qualitative content and assigned content. Qualitative content derives from the mental image itself; for visual imaginings, it is what is “pictured.” For example, visually imagine the Philadelphia Eagles defeating the Pittsburgh Steelers to win their first Super Bowl. You picture the greenness of the field and (...) the football’s brown oblong shape. Some of what you imagine isn’t explicitly pictured, however. That it is Sunday, that it is the Super Bowl: these facts are assigned. (shrink)

Political decisions have the potential to greatly impact our lives. Think of decisions in relation to abortion or climate change, for example. This makes political legitimacy an important normative concern. But what makes political decisions legitimate? Are they legitimate in virtue of having support from the citizens? Democratic conceptions of political legitimacy answer in the affirmative. Such conceptions righly highlight that legitimate political decision-making must be sensitive to disagreements among the citizens. But what if democratic decisions fail to track what (...) there is most reason to do? What if a democratically elected government fails to take measures necessary to protect its population from threats related to climate change? Peter argues that the legitimacy of political decisions doesn't just depend on respect for the citizens' will; and defends a novel hybrid conception of political legitimacy, called the Epistemic Accountability conception. According to this conception, political legitimacy also depends on how political decision-making responds to evidence for what there is most reason to do. Grounds for Political Legitmacy starts with an overview of the main ways in which philosophers have thought about political legitimacy, and identifies the epistemic accountability conception as an overlooked alternative. It then develops the epistemic accountability conception of political legitimacy and discusses its implications for legitimate political decision-making. Considering the norms that should govern political debate, it examines the role of experts in politics, and probes the responsibilities of democratically elected political leaders and as well as of citizens. (shrink)

In this study, we investigated whether control of the conflict between incongruent heuristic and analytical answer options in a reasoning task is modulated by the presence of conflict on previous trials. In two experiments, we found that the incongruency of the previous trial has a significant effect on the control exhibited on the current trial. Our data also showed that this adaptation effect is modulated by the incongruency of the previous series of trials. These results demonstrate the same control adaptation (...) effects for a reasoning task as observed for standard response interference tasks. Coinciding control effects in the two research areas suggest that cognitive control might be an important mechanism underlying performance on reasoning tasks. Based on these results we argue that the study of cognitive control in reasoning could potentially facilitate the refinement of empirical predictions and provide a new tool to explore the exertion of top-down control in human thinking. (shrink)

In at least some cases of justified perceptual belief, our perceptual experience itself, as opposed to beliefs about it, evidences and thereby justifies our belief. While the phenomenon is common, it is also mysterious. There are good reasons to think that perceptions cannot justify beliefs directly, and there is a significant challenge in explaining how they do. After explaining just how direct perceptual justification is mysterious, I considerMichael Huemers (Skepticism and the Veil of Perception, 2001) and Bill Brewers (Perception and (...) Reason, 1999) recent, but radically different, attempts to eliminate it. I argue that both are unsuccessful, though a consideration of their mistakes deepens our appreciation of the mystery. (shrink)