We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...) a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

Within the technical frame supplied by the algebraic variety of diagonalizable algebras, defined by R. Magari in [2], we prove the following: Let T be any first-order theory with a predicate Pr satisfying the canonical derivability conditions, including Löb's property. Then any formula in T built up from the propositional variables $q,p_{1},...,p_{n}$ , using logical connectives and the predicate Pr, has the same "fixed-points" relative to q (that is, formulas $\psi (p_{1},...,p_{n})$ for which for all $p_{1},...,p_{n}\vdash _{T}\phi (\psi (p_{1},...,p_{n}),p_{1},...,p_{n})\leftrightarrow \psi (...) (p_{1},...,p_{n})$ ) of a formula $\phi ^{\ast}$ of the same kind, obtained from φ in an effective way. Moreover, such $\phi ^{\ast}$ is provably equivalent to the formula obtained from φ substituting with $\phi ^{\ast}$ itself all the occurrences of q which are under Pr. In the particular case where q is always under Pr in φ, $\phi ^{\ast}$ is the unique (up to provable equivalence) "fixed-point" of φ. Since this result is proved only assuming Pr to be canonical, it can be deduced that Löb's property is, in a sense, equivalent to Gödel's diagonalization lemma. All the results are proved more generally in the intuitionistic case. (shrink)

We introduce a sequent calculusBfor a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterizeBpositively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, (...) and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules,ex falso quodlibetor double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, (...) including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward. (shrink)

Martin-Löf Type Theory is both an important and practical formalization and a focus for a charismatic view of the foundations of mathematics. Per Martin-Löf's work has been of huge significance in the fields of logic and the foundations of mathematics, and has important applications in areas such as computing science and linguistics. This volume celebrates the twenty-fifth anniversary of the birth of the subject, and is an invaluable record both of areas of currentactivity and of the early development of the (...) subject. Also published for the first time is one of Per Martin-Löf's earliest papers. (shrink)

We introduce the notion of infinitary preorder and use it to obtain a predicative presentation of sup-lattices by generators and relations. The method is uniform in that it extends in a modular way to obtain a presentation of quantales, as “sup-lattices on monoids”, by using the notion of pretopology.Our presentation is then applied to frames, the link with Johnstone’s presentation of frames is spelled out, and his theorem on freely generated frames becomes a special case of our results on quantales.The (...) main motivation of this paper is to contribute to the development of formal topology. That is why all our definitions and proofs can be expressed within an intuitionistic and predicative foundation, like constructive type theory. (shrink)

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined. (shrink)

The search for a synthesis between formalism and constructivism, and meditation on Gödel incompleteness, leads in a natural way to conceive mathematics as dynamic and plural, that is the result of a human achievement, rather than static and unique, that is given truth. This foundational attitude, called dynamic constructivism, has been adopted in the actual development of topology and revealed some deep structures that had remained hidden under other views. After motivations for and a brief introduction to dynamic constructivism, an (...) overview is given of the changes it induces in the practice of mathematics and in its foundation, and of the new results it allows to obtain. (shrink)

This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.

We construct a Galois connection between closure and interior operators on a given set. All arguments are intuitionistically valid. Our construction is an intuitionistic version of the classical correspondence between closure and interior operators via complement.

A positive topology is a set equipped with two particular relations between elements and subsets of that set: a convergent cover relation and a positivity relation. A set equipped with a convergent cover relation is a predicative counterpart of a locale, where the given set plays the role of a set of generators, typically a base, and the cover encodes the relations between generators. A positivity relation enriches the structure of a locale; among other things, it is a tool to (...) study some particular subobjects, namely the overt weakly closed sublocales. We relate the category of locales to that of positive topologies and we show that the former is a reflective subcategory of the latter. We then generalize such a result to the category of suplattices, which we present by means of cover relations. Finally, we show that the category of positive topologies also generalizes that of formal topologies, that is, overt locales. (shrink)

We give arguments explaining why, when adopting a minimalist approach to constructive mathematics as that formalized in our two-level minimalist foundation, the choice for a pointfree approach to topology is not just a matter of convenience or mathematical elegance, but becomes compulsory. The main reason is that in our foundation real numbers, either as Dedekind cuts or as Cauchy sequences, do not form a set.

The duality between general frames and modal algebras allows to transfer a problem about the relational (Kripke) semantics into algebraic terms, and conversely. We here deal with the conjecture: the modal algebra A is subdirectly irreducible (s.i.) if and only if the dual frame A* is generated. We show that it is false in general, and that it becomes true under some mild assumptions, which include the finite case and the case of K4. We also prove that a Kripke frame (...) F is generated if and only if the dual algebra F* is s.i. The technical result is that A is s.i. when the set of points which generate the dual frame A* is not of zero measure. (shrink)

Global properties of canonical derivability predicates in Peano Arithmetic) are studied here by means of a suitable propositional modal logic GL. A whole book [1] has appeared on GL and we refer to it for more information and a bibliography on GL. Here we propose a sequent calculus for GL and, by exhibiting a good proof procedure, prove that such calculus admits the elimination of cuts. Most of standard results on GL are then easy consequences: completeness, decidability, finite model property, (...) interpolation and the fixed point theorem. (shrink)

Humanity’s self-ordained mandate to subdue and dominate nature is part of the cognitive foundation of the modern world—a perspective that remains deeply ingrained in science and technology. Marine biology has not been immune to this anthropocentric bias. But this needs to change, and the gaps between basic scientific disciplines and the global conservation imperatives of our time need to be bridged. In the face of a looming ecological and climate crisis, marine biologists must upgrade their values and professional standards and (...) help foster the radical transformation needed to avert a climate and ecological breakdown. To prevent some of the damage, they must cross the imaginary line that separates science from science-based activism and consciously pursue the health and durability of human and natural communities. To this end, they can (1) develop compelling narratives that engage human society, with emphasis on care for the wild living world; (2) move beyond marine conservation on paper and avoid self-serving complaisance; (3) advocate constructive changes in market and human behaviour, not only by documenting damage but also by clarifying how the extraction, production and consumption system can be steered away from practices that harm nature; (4) push for systemic change in politics through individual and collective efforts, supporting environmental activism and those who demand biosphere-saving policies; and (5) endorse a more ecocentric and holistic world vision, relinquishing contempt for spiritual wisdom and liaising with (or at least not dismissing) spiritual traditions that encourage equality, self-restraint and environmental sustainability. (shrink)

This handbook is currently in development, with individual articles publishing online in advance of print publication. At this time, we cannot add information about unpublished articles in this handbook, however the table of contents will continue to grow as additional articles pass through the review process and are added to the site. Please note that the online publication date for this handbook is the date that the first article in the title was published online.

In the paper, after clarifying terms such as ‘identity’, ‘self’ and ‘personhood’, I propose an empirical account of identity based on the notion of “whole phenotype”. This move allows one to claim the persistence of the individuals before and after their being affected by dementia. Furthermore, I show how this account permits us to address significant questions related to demented individuals’ loss of the capacity of moral decisions.

Emotions and personhood are important notions within the field of mental health care. How they are related is less evident. This book provides a framework for understanding the important and complex relationship between our emotional wellbeing and our sense of self, drawing on psychopathology, philosophy, and phenomenology.

How can we better understand and treat those suffering from schizophrenia and manic-depressive illnesses? This important new book takes us into the world of those suffering from such disorders. Using self descriptions, its emphasis is not on how mental health professionals view sufferers, but on how the patients themselves experience their disorder. A new volume in the International Perspectives in Philosophy and Psychiatry series, this book will be of great interest to all those working with sufferers from such disorders - (...) helping them to better understand their mental lives, and providing important insights into how best to treat them. (shrink)

Much of the recent philosophical debate on causation and causal explanation in the biological and biomedical sciences has focused on the notion of mechanism. Mechanisms, their nature and epistemic roles have been tackled by a range of so-called neo-mechanistic theories, and widely discussed. Without denying the merits of this approach, our paper aims to show how lately it has failed to give proper credit to processes, which are central to the field, especially of contemporary molecular biology. Processes can be summed (...) up in the notion of ‘pathway’, which is far from being just equivalent to that of ‘mechanism’ and has a profound epistemological and explanatory relevance. It is argued that an adequate consideration of pathways impels some rethinking of scientific explanation in molecular biology, namely its functional and contextual features. A number of examples are given to suggest that the focus of philosophical attention in this disciplinary field should shift from the notion of mechanism to the notion of pathway. (shrink)

Two problems related to the biological identity of living beings are faced: the who-problem (which are the biological properties making that living being unique and different from the others?); the persistence-problem (what does it take for a living being to persist from a time to another?). They are discussed inside a molecular biology framework, which shows how epigenetics can be a good ground to provide plausible answers. That is, we propose an empirical solution to the who-problem and to the persistence-problem (...) on the basis of the new perspectives opened by a molecular understanding of epigenetic processes. In particular, concerning the former, we argue that any living being is the result of the epigenetic processes that have regulated the expression of its genome; concerning the latter, we defend the idea that the criterion for the persistence of its identity is to be indicated in the continuity of those epigenetic processes. We also counteract possible objections, in particular (1) whether our approach has something to say at a metaphysical level; (2) how it could account for the passage from the two phenotypes of the parental gametes to the single phenotype of the zygote; (3) how it could account for the identity of derivatives of one living being that continue to live disjoined from that original living being; (4) how it could account for higher mental functions. (shrink)