We develop a constructive version of nonstandard analysis, extending Bishop's constructive analysis with infinitesimal methods. A full transfer principle and a strong idealisation principle are obtained by using a sheaf-theoretic construction due to I. Moerdijk. The construction is, in a precise sense, a reduced power with variable filter structure. We avoid the nonconstructive standard part map by the use of nonstandard hulls. This leads to an infinitesimal analysis which includes nonconstructive theorems such as the Heine-Borel theorem, the Cauchy-Peano existence theorem (...) for ordinary differential equations and the exact intermediate-value theorem, while it at the same time provides constructive results for concrete statements. A nonstandard measure theory which is considerably simpler than that of Bishop and Cheng is developed within this context. (shrink)

Stakeholder theory has become an influential framework for addressing organizational challenges, including those related to sustainability. Yet, the inclusion of nonhuman stakeholders in stakeholder theory is complicated by ontological and epistemological obstacles. To overcome these, we turn to art and posthumanist practice theory and examine artist-led practices by focusing on the projects of two pioneering eco-artists, Helen Mayer Harrison and Newton Harrison. In this way we identify the ontological and epistemological challenges that impede the inclusion of nonhumans into stakeholder theory, (...) showing that artist-led practices allow for the inclusion of nonhuman stakeholders in two ways: (1) by specifying the temporal, spatial, and outcome distinctions that ontologically hinder their inclusion; and (2) by explicating the reframing of knowing and the emotional and imaginative dimensions of knowing that epistemologically enable their inclusion. We expand on the theorizing of nonhuman stakeholder inclusion by understanding the inclusion of nonhumans, first, not as a fixed state that is to be achieved but rather as one that materializes and gains meaning through specific practices of knowing; and, second, not as merely the absence of exclusion but rather as a dynamic interplay, where inclusion and exclusion mutually constitute one another. By advancing stakeholder theory’s theorizing and understandings of inclusion and exclusion, we also respond to urgent and contemporary environmental challenges. (shrink)

Mobile health devices pose novel questions at the intersection of philosophy and technology. Many such applications not only collect sensitive data, but also aim at persuading users to change their lifestyle for the better. A major concern is that persuasion is paternalistic as it intentionally aims at changing the agent’s actions, chipping away at their autonomy. This worry roots in the philosophical conviction that perhaps the most salient feature of living autonomous lives is displayed via agency as opposed to patiency—our (...) lives go well in virtue of what we do, rather than what happens to us. Being persuaded by a device telling us how to conduct our lives seemingly renders the agent passive, an inert recipient of technological commands. This agential bias, however, has led to a marginalization of patiential characteristics that are just as much part of our lives as are agential characteristics. To appreciate the inherent interlocking of acting and being acted upon, it is vital to acknowledge that agency and patiency are correlates, not mutually exclusive opposites. Furthermore, it is unclear whether an action can only count as agential so long as its causes are internal. Drawing on the extended mind and extended will framework, I argue that mHealth applications merely serve as volitional aids to the agent’s internal cognition. Autonomously set goals can be achieved more effectively via technology. To be persuaded by an mHealth device does not mainly—let alone exclusively—emphasize patiency; on the contrary, it can be an effective tool for technologically enhancing agency. (shrink)

In our lives, we aim to achieve welfare for ourselves, that is, to live good lives. But we also have another, more impartial perspective, where we aim to balance our concern for our own welfare against a concern for the welfare of others. This is a perspective of justice. Nils Holtug examines these two perspectives and the relations between them.

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this (...) article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos. (shrink)

In this paper, we consider a few actual cases of mnemonic strategies among older subjects (older than 65). The cases are taken from an ethnographic study, examining how elderly adults cope with cognitive decline. We believe that these cases illustrate that the process of remembering in many cases involve a complex distributed web of processes involving both internal or intracranial and external sources. Our cases illustrate that the nature of distributed remembering is shaped by and subordinated to the dynamic characteristics (...) of the on-going activity and to our minds suggest that research on memory and distributed cognition should focus on the process of remembering through detailed descriptions and analysis of naturally occurring situations. (shrink)

The present paper unravels ontological and normative conditions of personhood for the purpose of critiquing ‘Cognitivist Views’. Such views have attracted much attention and affirmation by presenting the ontology of personhood in terms of higher-order cognition on the basis of which normative practices are explained and justified. However, these normative conditions are invoked to establish the alleged ontology in the first place. When we want to know what kind of entity has full moral status, it is tempting to establish an (...) ontology that fits our moral intuitions about who should qualify for such unique normative standing. But this approach conflates personhood’s ontology and normativity insofar as it stresses the primacy of the former while implicitly presupposing the latter; it thereby suffers from a ‘Normative Fallacy’ by inferring from ‘ought’ to ‘is’. Following my critique of Cognitivism, I sketch an alternative conception, contending that, whereas the Cognitivist ontology of personhood presupposes the normative, a social ontology is constituted by it. In due consideration of evidence from developmental psychology, the social embeddedness of persons—manifested in the ability of taking a ‘second-person stance’—is identified as a key feature of personhood that precedes higher-order cognition, and is directly linked to basic normative concerns. (shrink)

This text is intended to show that in Hannah Arendt’s reflections on the possibilities of political judgment there is an idea of subjectivity that seeks to combine sociality and individuality. In Hannah Arendt’s case, the development of individual judgment becomes the precondition for allowing individuals to be given independent judgment. Arendt derives this concept of judgment from Kant’s reflections on the aesthetic power of judgment which she broadens and makes fruitful for political space. Using the example of aesthetic judgment, Arendt (...) develops an idea of political subjectivity that is intended to respond to the destruction of the subject through totalitarian politics. (shrink)

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved (...) for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle. (shrink)

We prove that a nonstandard extension of arithmetic is effectively conservative over Peano arithmetic by using an internal version of a definable ultrapower. By the same method we show that a certain extension of the nonstandard theory with a saturation principle has the same proof-theoretic strength as second order arithmetic, where comprehension is restricted to arithmetical formulas.

We give an intuitionistic axiomatisation of real closed fields which has the constructive reals as a model. The main result is that this axiomatisation together with just the decidability of the order relation gives the classical theory of real closed fields. To establish this we rely on the quantifier elimination theorem for real closed fields due to Tarski, and a conservation theorem of classical logic over intuitionistic logic for geometric theories.

The contributors to the volume are: Richard Arneson, Linda Barclay, Thomas Christiano, Nils Holtug, Susan Hurley, Kasper Lippert-Rasmussen, Dennis McKerlie, ...

We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to occur only (...) strictly positively. The modelling is done by constructivizing continuity notions for set operators at higher number classes and proving that strictly positive set operators are continuous in this sense. The existence of least fixed points, or more accurately, least sets closed under the operator, then easily follows. (shrink)

We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers.

Berichte zur Wissenschaftsgeschichte, EarlyView.

This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas additional to those familiar from standard intuitionist and classical logic. When $\invertediota$ is added it must be ensured that reduction procedures involving replacements of parameters by terms do not introduce new maximal formulas of higher degree than the ones removed. The problem is solved by a rule (...) that permits restricting these terms in the rules for $\forall$, $\exists$ and $\invertediota$ to parameters or constants. A restricted subformula property for deductions in systems without $\invertediota$ is considered. It is improved upon by an alternative formalisation of free logic building on an idea of Ja\'skowski's. In the classical system the rules for $\invertediota$ require treatment known from normalisation for classical logic with $\lor$ or $\exists$. The philosophical significance of the results is also indicated. (shrink)

The strength of a slippery slope argument is a matter of some dispute. Some see it as a reasonable argument pointing out what probably or inevitably follows from adopting some practice, others see it as essentially a fallacious argument. However, there seems to be a tendency emerging to say that in many cases, the argument is not actually fallacious, although it may be unsubstantiated. I shall not try to settle this general discussion, but merely seek to assess the strength of (...) the slippery slope argument applied to human gene therapy. The structure of my argument will be the following. First, I shall distinguish between three different versions of the slippery slope argument; two logical versions and an empirical one. Next, I will address human gene therapy in terms of each of the three versions, partly relying on slippery slope arguments against this practice that have already surfaced in the literature. I shall argue that neither version pulls through. The logical versions fail primarily because relevant distinctions can be made between different uses of gene therapy, contrary to what the proponents of the arguments claim. The empirical version fails because there seems to be no evidence supporting the claim that we shall in fact slide down the slope if we engage in gene therapy, and because if we accepted the conclusion that we should not allow gene therapy on the basis of the empirical argument, we should have to make very far-reaching and undesirable modifications in health care in general, in order to be consistent. Or at least so I shall argue. (shrink)

The class of points in a set-presented formal topology is a set, if all points are maximal. To prove this constructively a strengthening of the dependent choice principle to infinite well-founded trees is used.

ABSTRACTIn light of the large recent inflow of refugees to the EU and the Commission’s efforts to relocate them, I raise the question of what a fair distribution of refugees between EU countries would look like. More specifically, I consider what concerns such a distributive scheme should be sensitive to. First, I put forward some arguments for why states are obligated to admit refugees and outline how I believe the EU should respond to the refugee crisis. This involves, among other (...) things, resettling a proportion of refugees from countries neighbouring Syria in the EU. Second, I consider how the intake into the EU should be distributed between member states, that is, the shares different countries can be expected to admit. I discuss the relevance of a number of different factors that may be claimed to affect such shares, including population size, GDP, number of refugees admitted so far, unemployment rate, country-specific costs and cultural ‘closeness’. Third, I consider whether the distributive scheme should be restricted to reflect specific states’ responsibility for creating refugees in the first place, levels of racism and xenophobia, and whether other states are required to pick up the slack if some refuse to admit their fair share. (shrink)

Need-based justice is an important ingredient for a pluralistic theory of justice. But how can need-based justice be measured? I will argue that need-based justice cannot be measured by measuring need-satisfaction. This is because need-based justice does not only depend on need-satisfaction, but also on opportunities to avoid or at least mitigate undersupply. Depending on these opportunities, one and the same degree of undersupply can be unjust to different degrees. In this article, I establish a number of desiderata that a (...) measure of need-based justice has to comply with. Resulting measures treat avoidable undersupply as the main source of injustice. (shrink)

The localic completion of a metric space induces a canonical notion of continuous map between metric spaces. It is shown that these maps are continuous in the sense of Bishop constructive mathematics, i.e., uniformly continuous near every compact image.

Dahlbäck, Forsblad and Hydén argue that conversational remembering in the real‐world must be acknowledged as an interactional practice grounded in and bound to the communicative actions produced by the interlocutors. They illustrate the complexity of those processes by referring to their own fieldwork examining older adults’ prospective memory within their homes (Dahlbäck, Kristiansson, & Stjernberg, 2013) and propose alternative methodologies (e.g., scenarios design) to increase collaborations between ethnographic and experimental memory researchers.

This paper is a discussion of efforts to manage real and potential conflicts of interest in university research in the United States. The focus is on the report by an Association of American Universities (AAU) task force that addresses both individual and institutional conflict of interest issues.

Justus Raphelengius, a Leiden printer and orientalist scholar, translated into Latin a sixteenth-century manuscript compilation of Turkish folk tales associated with the famous Anatolian comic figure Nasreddin Hoca. This article considers the role of Raphelengius’s translation within the framework of the manuscript circulation and print production of Nasreddin Hoca tales in Europe from the first dated manuscript to twentieth-century printed editions Raphelengius’s editorial choices for his intended publication, the style of his Latin translation, and his excision of bawdy or sacrilegious (...) passages from the original text come under scrutiny. (shrink)

The case in favor of gene therapy is quite simple. Gene therapy is likely to improve the health and well-being of some people that are among the worst off in society, namely patients with painful and life-threatening diseases. However, two types of objection have been raised.

Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is shown for (...) fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed. (shrink)

The right to health is enshrined in the constitution of the World Health Organization and numerous other international agreements. Yet today, an estimated 5.7 million people die each year from treatable infectious diseases, most of which are susceptible to existing antimicrobials if they were accessible. These deaths occur predominantly among populations living in poverty in low- and middle-income countries, and they greatly exceed the estimated 700,000 annual deaths worldwide currently attributed to antimicrobial resistance. Ensuring universal appropriate access to antimicrobials is (...) not only a critical part of realizing the right to health, it is necessary for mobilizing effective collective action against the development and spread of AMR. (shrink)