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

This article introduces and defends the “pathological complexity thesis” as a hypothesis about the evolutionary origins of minimal consciousness, or sentience, that connects the study of animal consciousness closely with work in behavioral ecology and evolutionary biology. I argue that consciousness is an adaptive solution to a design problem that led to the extinction of complex multicellular animal life following the Avalon explosion and that was subsequently solved during the Cambrian explosion. This is the economic trade-off problem of having to (...) deal with a complex body with high degrees of freedom, what I call “pathological complexity.” By modeling the explosion of this computational complexity using the resources of state-based behavioral and life history theory we will be able to provide an evolutionary bottom-up framework to make sense of subjective experience and its function in nature by paying close attention to the ecological lifestyles of different animals. (shrink)

The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, (...) we prove in this paper that the statement “if X is well-ordered then εX is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a fragment of. (shrink)

The article shows a simple way of calibrating the strength of the theory of positive induction, ${{\rm ID}^{*}_{1}}$ . Crucially the proof exploits the equivalence of ${\Sigma^{1}_{1}}$ dependent choice and ω-model reflection for ${\Pi^{1}_{2}}$ formulae over ACA 0. Unbeknown to the authors, D. Probst had already determined the proof-theoretic strength of ${{\rm ID}^{*}_{1}}$ in Probst, J Symb Log, 71, 721–746, 2006.

In this article we characterize a countable ordinal known as the big Veblen number in terms of natural well-partially ordered tree-like structures. To this end, we consider generalized trees where the immediate subtrees are grouped in pairs with address-like objects. Motivated by natural ordering properties, extracted from the standard notations for the big Veblen number, we investigate different choices for embeddability relations on the generalized trees. We observe that for addresses using one finite sequence only, the embeddability coincides with the (...) classical tree-embeddability, but in this article we are interested in more general situations. We prove that the maximal order type of some of these new embeddability relations hit precisely the big Veblen ordinal ϑΩΩ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vartheta \Omega^{\Omega}}$$\end{document}. Somewhat surprisingly, changing a little bit the well-partially ordered addresses, the maximal order type hits an ordinal which exceeds the big Veblen number by far, namely ϑΩΩΩ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vartheta \Omega^{\Omega^\Omega}}$$\end{document}. Our results contribute to the research program on classifying properties of natural well-orderings in terms of order-theoretic properties of the functions generating the orderings. (shrink)

There has been much criticism of the idea that Friston's free-energy principle can unite the life and mind sciences. Here, we argue that perhaps the greatest problem for the totalizing ambitions of its proponents is a failure to recognize the importance of evolutionary dynamics and to provide a convincing adaptive story relating free-energy minimization to organismal fitness.

The regular extension axiom, REA, was first considered by Peter Aczel in the context of Constructive Zermelo-Fraenkel Set Theory as an axiom that ensures the existence of many inductively defined sets. REA has several natural variants. In this note we gather together metamathematical results about these variants from the point of view of both classical and constructive set theory.

This paper constitutes a radical departure from the existing philosophical literature on models, modeling-practices, and model-based science. I argue that the various entities and practices called 'models' and 'modeling-practices' are too diverse, too context-sensitive, and serve too many scientific purposes and roles, as to allow for a general philosophical analysis. From this recognition an alternative view emerges that I shall dub model anarchism.

An alarming number of philosophers and cognitive scientists have argued that mind extends beyond the brain and body. This book evaluates these arguments and suggests that, typically, it does not. A timely and relevant study that exposes the need to develop a more sophisticated theory of cognition, while pointing to a bold new direction in exploring the nature of cognition Articulates and defends the “mark of the cognitive”, a common sense theory used to distinguish between cognitive and non-cognitive processes Challenges (...) the current popularity of extended cognition theory through critical analysis and by pointing out fallacies and shortcoming in the literature Stimulates discussions that will advance debate about the nature of cognition in the cognitive sciences. (shrink)

This paper presents the outlines of a phenomenological theory of foundational or non-inferential knowledge according to which the facts or states of affairs towards which our beliefs are intentionally directed can sometimes serve as reasons or evidence for what we believe. This occurs in acts of fulfillment, in which an object or state of affairs is given as it is thought to be. Hopp further argues that the sorts of empirical facts that can serve as reasons for noninferentially justified beliefs (...) are not confined to facts about one’s own occurrent mental states, but include facts about the physical world as well. In the course of defending the view against objections, Hopp argues that we should be internalists about the reasons in virtue of which what we believe is justified but externalists about the factors in virtue of which our states of believing have the status of being justified. He also argues against the claim that mental states, such as perceptual experiences, constitute our evidence for empirical beliefs. (shrink)

Introduction: the advance of governmentality -- Foucault, power, and governmentality: introduction; what is governmentality?; beyond the microphysics of power?; from theory of the state to genealogy of the state; history of the art of government; pastoral power; raison d'état; liberal governmentality; five propositions on foucault and governmentality -- Governmentality 3.4.7.: introduction; governmentality after Foucault; governmentality and the political sciences; some problems in governmentality -- Foucault effect redux? some notes on international governmentality studies: constellation; a few preliminary observations; problems and debates (...) in international governmentality studies -- Reconnecting governmentality and genealogy: introduction; genealogy and governmentality; pluralizing genealogy; practicing genealogy; lines of descent: the family tree of power?; counter-memory and re-serialization; the retrieval of forgotten struggles and subjugated knowledges -- Conclusion: encountering governmentality: governmentality as a new cartography of power; from mapping to encountering; governmentality and politics. (shrink)

A variant of realizability for Heyting arithmetic which validates Church’s thesis with uniqueness condition, but not the general form of Church’s thesis, was introduced by Lifschitz (Proc Am Math Soc 73:101–106, 1979). A Lifschitz counterpart to Kleene’s realizability for functions (in Baire space) was developed by van Oosten (J Symb Log 55:805–821, 1990). In that paper he also extended Lifschitz’ realizability to second order arithmetic. The objective here is to extend it to full intuitionistic Zermelo–Fraenkel set theory, IZF. The machinery (...) would also work for extensions of IZF with large set axioms. In addition to separating Church’s thesis with uniqueness condition from its general form in intuitionistic set theory, we also obtain several interesting corollaries. The interpretation repudiates a weak form of countable choice, ACω,ω, asserting that a countable family of inhabited sets of natural numbers has a choice function. ACω,ω is validated by ordinary Kleene realizability and is of course provable in ZF. On the other hand, a pivotal consequence of ACω,ω, namely that the sets of Cauchy reals and Dedekind reals are isomorphic, remains valid in this interpretation. Another interesting aspect of this realizability is that it validates the lesser limited principle of omniscience. (shrink)

One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency proof of a (...) strong classical theory. Also the proof-theoretic strength of other inductive types like Aczel's type of iterative sets is investigated in various contexts.Further, we study metamathematical relations between type theories and other frameworks for formalizing constructive mathematics, e.g. Aczel's set theories and theories of operations and classes as developed by Feferman. (shrink)

The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκ where κ is a strongly inaccessible cardinal and Vκ denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the context in (...) which they are embedded. The context here will be the theory CZF− of constructive Zermelo–Fraenkel set theory but without -Induction . Let INAC be the statement that for every set there is an inaccessible set containing it. CZF−+INAC is a mathematically rich theory in which one can easily formalize Bishop style constructive mathematics and a great deal of category theory. CZF−+INAC also has a realizability interpretation in type theory which gives its theorems a direct computational meaning. The main result presented here is that the proof theoretic ordinal of CZF−+INAC is a small ordinal known as the Feferman–Schütte ordinal Γ0. (shrink)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical (...) point of view. (shrink)

This article canvases the main areas of controversy: the nature of Lockean signification and his position on propositions and particles.

Especially nice models of intuitionistic set theories are realizability models $V$, where $\mathcal A$ is an applicative structure or partial combinatory algebra. This paper is concerned with the preservation of various choice principles in $V$ if assumed in the underlying universe $V$, adopting Constructive Zermelo–Fraenkel as background theory for all of these investigations. Examples of choice principles are the axiom schemes of countable choice, dependent choice, relativized dependent choice and the presentation axiom. It is shown that any of these axioms (...) holds in $V$ for every applicative structure $\mathcal A$ if it holds in the background universe.1 It is also shown that a weak form of the countable axiom of choice, $\textbf{AC}^{\boldsymbol{\omega, \omega }}$, is rendered true in any $V$ regardless of whether it holds in the background universe. The paper extends work by McCarty and Rathjen. (shrink)

The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of these new cut (...) elimination techniques to attain an ordinal analysis of П12 comprehension by approaching П12 comprehension through transfinite levels of reflection. (shrink)

On a currently popular reading of Locke, an idea represents its cause, or what God intended to be its cause. Against Martha Bolton and my former self (among others), I argue that Locke cannot hold such a view, since it sins against his epistemology and theory of abstraction. I argue that Locke is committed to a resemblance theory of representation, with the result that ideas of secondary qualities are not representations.

Teachers in many countries complain that their pedagogic work is impeded by unreasonable bureaucratic demands by government agencies. This paper suggests that historical, institutional and cultural perspectives are needed to understand the processes at work. It draws on Weber’s classic study of bureaucracy, but also makes reference to claims that traditional bureaucracies have been modified in ways that ameliorate their authoritarian character. The central part of the paper examines the attempts of one country (Scotland) to address complaints about excessive bureaucracy: (...) it is argued that they show a limited understanding of the nature of institutional power. In the discussion that follows, a number of critical interpretations are considered: that bureaucracies are, by their very nature, anti-educational; that they undermine ethical consciousness and cause psychological damage; and that enhanced professionalism can serve as a counterweight to bureaucratic tendencies. The paper ends by suggesting that the powerful pragmatic argument that mass, state-run educational systems cannot function without complex administrative structures, should not be used to disguise the fact that they have unintended consequences, some of which tend to subvert their stated aims. (shrink)

In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.

Gerhard Gentzen has been described as logic’s lost genius, whom Gödel called a better logician than himself. This work comprises articles by leading proof theorists, attesting to Gentzen’s enduring legacy to mathematical logic and beyond. The contributions range from philosophical reflections and re-evaluations of Gentzen’s original consistency proofs to the most recent developments in proof theory. Gentzen founded modern proof theory. His sequent calculus and natural deduction system beautifully explain the deep symmetries of logic. They underlie modern developments in computer (...) science such as automated theorem proving and type theory. (shrink)

Identification of the molecular mechanisms underlying axonal branching in vivo has begun in several neuronal systems, notably the projections formed by dorsal root ganglion (DRG) neurons or retinal ganglion cells (RGC). cGMP signalling is essential for sensory axon bifurcation at the spinal cord, whereas brain‐derived neurotrophic factor (BDNF) and ephrinA signalling establish position‐dependent branching of RGC axons. In the latter system, the degradation of specific signalling components, via the ubiquitin‐proteasome system, may provide an additional mechanism involved in axon branching of (...) RGC. The process of arborisation is essential for neurons to innervate multiple targets and to build topographic maps. The various forms of branching found in different types of neurons are regulated by distinct signalling pathways activated by multiple extracellular cues in addition to axonal guidance factors. These signalling cascades, together with transcriptional programs, most likely interact and trigger the polymerisation or depolymerisation of the actin and tubulin cytoskeleton to regulate branching. (shrink)

Like their contemporary counterparts, early modern philosophers find themselves in a predicament. On one hand, there are strong reasons to deny that sensations are representations. For there seems to be nothing in the world for them to represent. On the other hand, some sensory representations seem to be required for us to experience bodies. How else could one perceive the boundaries of a body, except by means of different shadings of color? I argue that Nicolas Malebranche offers an extreme -- (...) and ultimately unworkable -- attempt to solve this riddle. Most commentators claim that Malebranche defends an adverbial theory of sensation, according to which a sensation is merely a way in which an act of sensing happens. The adverbial reading is wrong, or so I argue. Once we arrive at a more accurate reading, we shall see that his position is much more strange than is currently thought. Nevertheless, Malebranche’s view is similar to the adverbial theory in one respect, albeit it at a very high level of generality. His view thus inherits two of the main problems that afflict adverbial theories. Although Malebranche fails to solve them, his ingenious attempts to do so are instructive. (shrink)

The conditions animals experience during the early developmental stages of their lives can have critical ongoing effects on their future health, welfare, and proper development. In this paper we draw on evolutionary theory to improve our understanding of the processes of developmental programming, particularly Predictive Adaptive Responses (PAR) that serve to match offspring phenotype with predicted future environmental conditions. When these predictions fail, a mismatch occurs between offspring phenotype and the environment, which can have long-lasting health and welfare effects. Examples (...) include metabolic diseases resulting from maternal nutrition and behavioral changes from maternal stress. An understanding of these processes and their evolutionary origins will help in identifying and providing appropriate developmental conditions to optimize offspring welfare. This serves as an example of the benefits of using evolutionary thinking within veterinary science and we suggest that in the same way that evolutionary medicine has helped our understanding of human health, the implementation of evolutionary veterinary science (EvoVetSci) could be a useful way forward for research in animal health and welfare. (shrink)

The first attempt at a systematic approach to axiomatic theories of truth was undertaken by Friedman and Sheard (Ann Pure Appl Log 33:1–21, 1987). There twelve principles consisting of axioms, axiom schemata and rules of inference, each embodying a reasonable property of truth were isolated for study. Working with a base theory of truth conservative over PA, Friedman and Sheard raised the following questions. Which subsets of the Optional Axioms are consistent over the base theory? What are the proof-theoretic strengths (...) of the consistent theories? The first question was answered completely by Friedman and Sheard; all subsets of the Optional Axioms were classified as either consistent or inconsistent giving rise to nine maximal consistent theories of truth.They also determined the proof-theoretic strength of two subsets of the Optional Axioms. The aim of this paper is to continue the work begun by Friedman and Sheard. We will establish the proof-theoretic strength of all the remaining seven theories and relate their arithmetic part to well-known theories ranging from PA to the theory of ${\Sigma^1_1}$ dependent choice. (shrink)

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of-analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated-comprehension, e.g.,-comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory came into existence in (...) 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2is still something to be sought. However, for reasons that cannot be explained here,-comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2in the foreseeable future.Roughly speaking,ordinally informativeproof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

Abstract.This paper is the second in a series of three culminating in an ordinal analysis of Π12-comprehension. Its objective is to present an ordinal analysis for the subsystem of second order arithmetic with Δ12-comprehension, bar induction and Π12-comprehension for formulae without set parameters. Couched in terms of Kripke-Platek set theory, KP, the latter system corresponds to KPi augmented by the assertion that there exists a stable ordinal, where KPi is KP with an additional axiom stating that every set is contained (...) in an admissible set. (shrink)

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory (...) came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2 is still something to be sought. However, for reasons that cannot be explained here, -comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2 in the foreseeable future.Roughly speaking, ordinally informative proof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

Alongside the rapid global advances in neuroscientific research, neuroethics has been one of the fastest growing sub-fields within bioethics. With this rapid expansion, bioethicists struggle to kee...

Are demands for equality motivated by envy? Nietzsche, Freud, Hayek, and Nozick all thought so. Call this the Envy Objection. For egalitarians, the Envy Objection is meant to sting. Many egalitarians have tried to evade the Envy Objection.. But should egalitarians be worried about envy? In this paper, I argue that egalitarians should stop worrying and learn to love envy. I argue that the persistent unwillingness to embrace the Envy Objection is rooted in a common misunderstanding of the nature of (...) the charge, what it reveals, and what can be said in response to it. I develop what Bernard Williams might call a vindicatory genealogy of envy, thereby allowing us to see that envy, rather than undermining egalitarian intuitions, can in fact play a distinct justificatory role (when it is fitting), which undermines the Envy Objection. (shrink)

Provides philosophical definitions which help scholars and students to understand Plotinus’ notions of eternity and time; presents a way in which to understand the relationship between eternity, time, and the hypostases; conveys the practical and experiential aspect of Ennead III.7.

In this article we provide an intrinsic characterization of the famous Howard–Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees with respect to a homeomorphic embeddability relation. We use our calculations to draw some conclusions about some corresponding subsystems of second order arithmetic. All these subsystems deal with versions of light-face Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\varPi ^1_1$$\end{document}-comprehension.