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 effort in providing constructive and predicative meaning to non-constructive modes of reasoning has almost without exception been applied to theories with full classical logic [4]. In this paper we show how to combine unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in constructively given models. These models are sheaf models over a $\sigma$ -complete Boolean algebra, whose topologies are generated by finite or countable covering relations. By a judicious choice of the Boolean algebra we (...) can directly extract effective content from $\Pi_2^0$ -statements true in the model. All the arguments of the present paper can be formalised in Martin-Löf's constructive type theory with generalised inductive definitions. (shrink)

The general framework of this paper is a reformulation of Hilbert’s program using the theory of locales, also known as formal or point-free topology [P.T. Johnstone, Stone Spaces, in: Cambridge Studies in Advanced Mathematics, vol. 3, 1982; Th. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 71–106; G. Sambin, Intuitionistic formal spaces–a first communication, in: D. Skordev , Mathematical Logic and its Applications, Plenum, New York, 1987, pp. 187–204]. Formal topology presents (...) a topological space, not as a set of points, but as a logical theory which describes the lattice of open sets. The application to Hilbert’s program is then the following. Hilbert’s ideal objects are represented by points of such a formal space. There are general methods to “eliminate” the use of points, close to the notion of forcing and to the “elimination of choice sequences” in intuitionist mathematics, which correspond to Hilbert’s required elimination of ideal objects. This paper illustrates further this general program on the notion of valuations. They were introduced by Dedekind and Weber [R. Dedekind, H. Weber, Theorie des algebraischen Funktionen einer Veränderlichen, J. de Crelle t. XCII 181–290] to give a rigorous presentation of Riemann surfaces. It can be argued that it is one of the first example in mathematics of point-free representation of spaces [N. Bourbaki, Eléments de Mathématique. Algèbre commutative, Hermann, Paris, 1965, Chapitre 7]. It is thus of historical and conceptual interest to be able to represent this notion in formal topology. (shrink)

Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are (...) a slight variation of ordinary first-order models, where truth values are now regular ideals of a given Boolean algebra. Two examples are presented: a simple conservativity result and Herbrand's theorem. (shrink)

We present a proof of Goodmanʼs Theorem, which is a variation of the proof of Renaldel de Lavalette [9]. This proof uses in an essential way possibly divergent computations for proving a result which mentions systems involving only terminating computations. Our proof is carried out in a constructive metalanguage. This involves implicitly a covering relation over arbitrary posets in formal topology, which occurs in forcing in set theory in a classical framework, but can also be defined constructively.

We introduce the notion of Boolean measure algebra. It can be described shortly using some standard notations and terminology. If B is any Boolean algebra, let BN denote the algebra of sequences , xn B. Let us write pk BN the sequence such that pk = 1 if i K and Pk = 0 if k < i. If x B, denote by x* BN the constant sequence x* = . We define a Boolean measure algebra to be a Boolean (...) algebra B with an operation μ:BN → B such that μ = 0 and μ = x. Any Boolean measure algebra can be used to model non-principal ultrafilters in a suitable sense. Also, we can build effectively the initial Boolean measure algebra. This construction is related to the closed open Ramsey Theorem 193–198.). (shrink)

We present a new and constructive proof of the Peter-Weyl theorem on the representations of compact groups. We use the Gelfand representation theorem for commutative C*-algebras to give a proof which may be seen as a direct generalization of Burnside's algorithm [3]. This algorithm computes the characters of a finite group. We use this proof as a basis for a constructive proof in the style of Bishop. In fact, the present theory of compact groups may be seen as a natural (...) continuation in the line of Bishop's work on locally compact, but Abelian, groups [2]. (shrink)

We present a manuscript of Paul Lorenzen that provides a proof of consistency for elementary number theory as an application of the construction of the free countably complete pseudocomplemented semilattice over a preordered set. This manuscript rests in the Oskar-Becker-Nachlass at the Philosophisches Archiv of Universität Konstanz, file OB 5-3b-5. It has probably been written between March and May 1944. We also compare this proof to Gentzen's and Novikov's, and provide a translation of the manuscript.

This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive way by (...) an initiality condition. We then use our work to define in a purely inductive way the measure of Borel subsets. (shrink)

We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop-compact. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.

We associate with any game G another game, which is a variant of it, and which we call . Winning strategies for have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over , and vice versa. Through we can express in algorithmic form, as a recursive winning strategy, many common proofs of non-constructive Mathematics, namely exactly the theorems of the (...) sub-classical logic Limit Computable Mathematics [6], Hayashi and Nakata [7]). (shrink)

A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajn’s theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of proof-search.

Le temps suspendu comme moment heureux est à juste titre considéré comme extrêmement précieux. Mais on peut se demander : par quoi donc peut-il bien être suspendu? L'hypothèse que l'auteur examine consiste dans l'idée que le temps est suspendu par le désir s'assouvissant. Ou que le temps suspendu n'est rien d'autre que du désir-temps : ni désir de temps, ni temps du désir ; il relève de leur unité profonde. Il s'agira d'élucider cette hypothèse notamment avec Rousseau, les épicuriens et (...) les stoïciens. (shrink)

Informed consent is the legal instrument that purports to protect an individual's autonomy and defends against medical arbitrariness. Informed Consent and Health highlights that possession of complete information about all relevant aspects of a proposed treatment is integral to the ability of a patient to make an informed choice. With patient choice at both legislative and judicial levels rising to greater levels of prominence, this timely book examines how the tensions between the rights of patients to make choices and the (...) duties of doctors to provide health care are managed.This illuminating book investigates our evolving understanding of informed consent from a range of comparative and international perspectives, demonstrating the diversity of its interpretations around the world. Chapters offer a nuanced analysis of the problems that impede the understanding and implementation of the concept of informed consent and explore the contemporary challenges that continue to hinder both the patient and the medical community.Containing an in-depth discussion on this fundamental right, this thought-provoking book will be of value to academics and practitioners alike. Providing fascinating insight into new solutions and interpretations, this book will also prove a key resource for clinicians and health care workers. (shrink)

Valorising the biocultural heritage of common goods could enable peasant farmers to achieve socially and economically inclusive sustainability. Increasingly appreciated by consumers, peasant heritage products offer small farmers promising opportunities for economic, social and territorial development. Identifying the obstacles and levers of this complex, multi-scale and multi-stakeholder objective requires an integrative framework. We applied the panarchy conceptual framework to two cases of participatory research with small quinoa producers: a local fair in Chile and quinoa export production in Bolivia. In both (...) cases, the “commoning” process was crucial both to bring stakeholders together inside their communities and to gain outside recognition for their production and thus achieve social and economic inclusion. Despite the differences in scale, the local fair and the export market shared a similar marketing strategy based on short value chains promoting quality products with high identity value. In these dynamics of biocultural heritage valorisation, the panarchical approach revealed the central place as well as the vulnerability of the community territory. As a place of both anchoring and opening, the community territory is the privileged space where autonomous and consensual control over the governance of common biocultural resources can be exercised. (shrink)

Comment Descartes a-t-il pu nier l'évidence de sa dette à l'égard du cogito d'Augustin, et Jacques Hadamard s'accuser, à l'inverse, de ne pas avoir découvert la relativité avant Einstein? Qu'est-ce qui pouvait bien justifier Lacan, lorsqu'il osait affirmer que l'inconscient n'est pas de Freud, mais de lui... De même, côté art : on se demande pourquoi Borges a voulu faire de Ménard l'auteur du Quichotte ou Duchamp devenir celui d'un urinoir. Thierry Marchaisse prouve ici que l'on peut devenir le (...) véritable auteur de l'idée d'un autre, et que ce paradoxe, avancé par Pascal voilà plus de trois siècles, est à la fois le verrou et la clé de la logique de la créativité. (shrink)

This root-and-branch reevaluation of Darwin's concept of sexual selection tackles the subject from historical, epistemological and theoretical perspectives. Contributions from a wealth of disciplines have been marshaled for this volume, with key figures in behavioural ecology, philosophy, and the history of science adding to its wide-ranging relevance. Updating the reader on the debate currently live in behavioural ecology itself on the centrality of sexual selection, and with coverage of developments in the field of animal aesthetics, the book details the current (...) state of play, while other chapters trace the history of sexual selection from Darwin to today and inquire into the neurobiological bases for partner choices and the comparisons between the hedonic brain in human and non-human animals. Welcome space is given to the social aspects of sexual selection, particularly where Darwin drew distinctions between eager males and coy females and rationalized this as evolutionary strategy. Also explored are the current definition of sexual selection (as opposed to natural selection) and its importance in today's biological research, and the impending critique of the theory from the nascent field of animal aesthetics. As a comprehensive assessment of the current health, or otherwise, of Darwin's theory, 140 years after the publication of his Descent of Man, the book offers a uniquely rounded view that asks whether 'sexual selection' is in itself a progressive or reactionary notion, even as it explores its theoretical relevance in the technical biological study of the twenty-first century. (shrink)

Ce livre cherche à montrer comment l'eau, à la fois réalité et symbole, nourrit la pensée de Platon. Quelle est l'origine de cette thématique et quelles en sont les finalités? A travers ces interrogations, il s'agit de mettre en lumière la fonction de cette matière particulière dont les aspects sont déclinés de manière originale dans l'ensemble de son oeuvre. En rassemblant la multiplicité des images de l'eau, l'auteur interroge la nature et la valeur des images en s'efforçant de montrer comment (...) Platon, écrivain et poète, met en oeuvre avec inventivité métaphores, allégories et mythes. De quoi alimenter un questionnement sur le réel, auquel l'eau donne un fil directeur. On y voit aussi se défaire une certaine idée du platonisme. Critique à l'égard de la rhétorique et des arts, Platon vise dans le miroir les effets illusoires de l'image et de l'imitation, mais Socrate utilise lui-même les images et les reflets tout au long des dialogues, et on en découvre avec étonnement toutes les variations. La métaphore hydrique conditionne l'univers de la parole et de la science, reflète le mouvement de la pensée et ses dérives. Dans les images métaphysiques et morales, ce sont les flux, les fleuves et le monde marin qui reflètent la nature et la qualité des âmes ; mythes et allégories déplient les symboles de la corruption, de l'oubli et de l'incontinence, où se jouent une idée de la matière et la valeur de l'existence. Sur le plan ontologique, l'eau dénoue les figures de l'instable qui mettent en oeuvre la réfutation des «liquides» - théoriciens du flux - et l'intelligibilité du devenir. Enfin, dans l'ordre politique, la critique de la thalassocratie, les mythes (l'Atlantide, la mer de la dissemblance) et les images nautiques suivent les lignes fluctuantes de l'histoire athénienne, mais tracent aussi les contours de la Cité juste et le visage du vrai gouvernant. Dans le scintillement des eaux, à la croisée du sensible et de l'intelligible, se construit l'iconologie platonicienne. L'eau figurée, transfigurée dans le fil liquide de la poésie, forme les multiples reflets de ce qu'il faut vraiment voir pour se libérer du spectacle des ombres et penser le chemin d'une sagesse, qui ne renonce jamais au monde. (shrink)

Liang Shuming, considered to be the Last Confucian, was a Buddhist.

Tout récemment, Y. Kalliontzis et Chr. Müller ont publié sept nouveaux catalogues militaires de Chorsiai. Le présent article part du constat que la chronologie des archontes fédéraux béotiens adoptée pour ces nouveaux documents soulève des difficultés. En confrontant la série de textes de Chorsiai aux autres séries documentaires existantes, notamment celle d’Aigosthènes, il est possible de proposer de nouvelles hypothèses chronologiques qui font disparaître ces difficultés. Sur la base de la série d’archontes fédéraux attestés dans les nouveaux textes de Chorsiai, (...) une séquence chronologique alternative est proposée pour le dernier quart du iiie siècle av. J.‑C., et sa plausibilité est testée à partir des données prosopographiques d’Akraiphia et de Hyettos. (shrink)

'The Matrix Project' comprises two contexts, namely photographic work of architect Thierry Lagrange and the self-reflective trajectory that he developed during his doctorate at KULeuven. Lagrange's practice-based research developed to an autonomous artistic project, in which he studied the signification and nature of observation within a creative process. Through his multifaceted practice as an architect, photographer and researcher, Lagrange developed 'The Matrix Method'; a method that stimulates creativity within different contexts and can be implemented for example in art education. (...) For the Matrix Project, 25 years' worth of photographs was entered into a context of research and presents a new perspective on different ways of seeing in our present visual culture. (shrink)

Le 7 novembre 2015, avait lieu à la BNF un colloque confrontant les pensées de René Girard et Michel Henry, intitulé "Le désir de l'Autre". Cette rencontre eut lieu trois jours après le décès de René Girard. Elle fut ainsi pour tous les participants l'occasion de lui rendre hommage. A la suite des confrontations déjà organisées par l'Association Recherches Mimétiques entre René Girard et des penseurs français du XXe siècle (Bourdieu, Levinas, Lévi-Strauss, Derrida, Sartre, etc.), il apparaissait nécessaire de mettre (...) la théorie mimétique en présence, cette fois, de la phénoménologie de Michel Henry, chez qui la question de l'Autre est cruciale. Nos travaux nous ont permis de manifester, peut-être contre toute attente chez des penseurs aux méthodes si différentes, une convergence, voire une complémentarité, dans la définition du désir, dans celle de la nature de la violence qu'il suscite, et aussi dans celle de la possibilité de son dépassement."--Page 4 of cover. (shrink)

The aim of this essay is to understand the relationship between knowledge and society and to reflect on the links between science and political decision making. The text evolved from a number of reflections the author made while president of the European Astronomical Society, president of the Swiss Academy of Sciences and vice-president of the European Academies Science Advisory Council (EASAC). The book starts by using astronomy as a showcase for what science brings to society in terms of intellectual enrichment, (...) of practical tools and of societal inputs. It then turns to looking generally at science as a human endeavour for which pleasure is a prime motivation and it describes the efforts made by researchers to rationalise their findings, thus making them universally acceptable. The author also describes the role of science in shaping our environment and discusses resulting responsibility of the scientists with respect to the evolution of the world. As part of an analysis of the relationship between science and policy the author describes the way in which scientists can (and must) bring knowledge in the political decision making process. The argument is closed with considerations on global governance, while the conclusion puts evidence based decision making processes in relation with the more emotional aspects of our behaviour. The readership of the book is intended to be all scientists involved in "science for policy" activities, as well as those who should become more active in this domain. This includes, but is not limited to, all members of science academies. Astronomers will find specific elements to help them think about their science. The intended readers of the book also include civil servants and policy makers who develop legislation and societal action in domains in which a solid knowledge base is important. The book should furthermore be of interest to citizens following public life and all those worried by the "post evidence" trends in policy. (shrink)

The meaning of material artifacts that remain unchanged in form can change through spatial references and through changes in context. In this volume, spatial, historical, topographical, and discursive contextual changes are analyzed in case studies, and their meanings and intersections are critically reflected upon.

L’Introduction à l’analyse des lignes courbes algébriques de Gabriel Cramer, paru en 1750, a tout de suite bénéficié du soutien de D’Alembert qui l’a inclus dans les références bibliographiques de ses articles de mathématiques de l’Encyclopédie portant sur les courbes. Ainsi choisi et légitimé par l’entreprise encyclopédique et ses reprises, l’ouvrage de Cramer devient objet patrimonial au tournant du xixe siècle pour les mathématiciens, amateurs, professionnels ou enseignants qui travaillent sur les courbes algébriques. Le suivi sur le temps long des (...) mentions de l’Introduction dans les encyclopédies, dictionnaires ou histoires des mathématiques en langue française, ainsi que dans quelques textes d’enseignement, nous permettra de comprendre que ce processus de patrimonialisation n’induit pas sa conservation, sa protection, sa valorisation à de seules fins mémorielles, en figeant l’ouvrage dans un passé immuable. Au contraire, il permet une historicisation critique de la part des acteurs qui les met en position d’interroger et de réactualiser les connaissances et les pratiques que l’œuvre contient, au gré des mouvements d’émergence, de réorganisation et des spécialisations des savoirs mathématiques, quitte à en oublier certains aspects pour en mettre de nouveaux en valeur. (shrink)