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 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.

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)

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 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)

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.

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.

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

Etudier le probleme de la personne, c'est s'interesser a un probleme qui traverse a peu pres tous les domaines de la philosophie, depuis la psychologie jusqu'a la theologie en passant par l'ethique et par le droit, mais dont le denominateur commun est la definition du soi-meme. Etudier ce probleme chez Maimonide, c'est voir comment un philosophe juif du Moyen-Age pouvait elaborer une representation coherente de l'homme en s'appuyant a la fois sur la pensee greco-arabe et sur la tradition hebraique. Ce (...) livre espere contribuer a une meilleure comprehension d'un philosophe dont on a trop souvent fragmente la pensee, apparemment dechiree entre des sources contradictoires. En fait, Maimonide a su developper un dialogue critique entre deux heritages qui demeurent aux fondements de la civilisation occidentale. C'est ce qui donne a sa pensee son caractere eminemment actuel. (shrink)

Le droit court derrière la "révolution numérique". Les algorithmes nous espionnent et restreignent les libertés publiques, ils calculent les indemnités au service des compagnies d'assurance. La diminution lente et continue des services chargés de veiller à l'application du droit affaiblit et parfois anéantit l'efficacité de ces lois. L'échec de la loi Hadopi est significatif à cet égard. Le mal est en fait bien plus profond et ne date pas d'hier. Nous vivons une époque de démolition des codes établis. Si le (...) droit est partout, en définitive il n'est nulle part... (shrink)

Cet ouvrage porte sur l'auto-comprehension de l'homme moderne dans son rapport a la dimension de l'animalite. L'auteur part du statut paradoxal des discours philosophiques de la Renaissance et de l'Age Classique sur la nature des animaux. Ce caractere paradoxal a ete bien caracterise par Pierre Bayle qui, dans l'article Pereira de son Dictionnaire, place son lecteur devant une alternative inconfortable entre les deux positions extremes que sont l'opinion tres dangereuse de Montaigne (qui affirme la superiorite des animaux sur les hommes) (...) et l'opinion absurde de Descartes (celle des animaux-machines). L'auteur propose une analyse minutieuse des deux textes seminaux que sont l'Apologie de Raimond Sebond de Montaigne et la cinquieme partie du Discours de la methode de Descartes, en s'attachant tout particulierement aux deplacements operes dans ces textes sur le fonds legue par la litterature zoologique antique, d'Aristote a Pline, Plutarque et Elien. Il montre ainsi le lien des paradoxes du discours zoologique des Modernes a un paradoxe philosophique plus fondamental par lequel l'anthropologie moderne se trouve degagee des ontologies scalaires traditionnelles pour constituer une champ autonome d'investigation. Cette liberation a une consequence importante pour les temps modernes: l'unite de l'homme n'est plus donnee dans un ordre predefini de l'etre, mais constitue une tache que l'homme doit accomplir, a la fois sur le plan ethique et sur le plan technique, en affrontant, dans une perspective d'immanence, le dualisme de la vie et de la pensee, du biologique et du noetique. (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)

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)

Le premier chapitre de la Métaphysique allemande ne comprend que neuf paragraphes et semble ne représenter qu' une sorte de préambule. De ce fait, on peut avoir le sentiment que la métaphysique ne commence à proprement parler qu'avec le § 10, lequel ouvre, avec l'énoncé du principe de contradiction, la partie ontologique de l'ouvrage. Pourtant, Wolff fait figurer dans cette première partie des considérations qui concernent de très près le commencement de sa philosophie: il présente tout d'abord quelque chose comme (...) un cogito. De plus, les acquis de ce premier chapitre sont repris à l'ouverture des cinq autres chapitres qui suivent : y aurait-il là matière à affirmer que la métaphysique wolffienne est fondée dans une expérience psychologique? Cette hypothèse est donc ici testée par l'examen successif des statuts de l' Ontologie, de la Logique et de la Psychologie empirique au travers d'une lecture conjointe de la Métaphysique allemande et de la Logique allemande. The first chapter of the German Metaphysics gathers only nine paragraphs and seems to represent but some kind of a preamble. Hence one may feel that metaphysics begins only with paragraph 10 opening the ontological part of the text with the contradiction principle. Yet Wolff already mentions a few considerations in this first part that are extremely close to the beginning of his philosophy : he presents from the start something very similar to a cogito. Moreover the assets of this first chapter are recaptured whenever every one of the five following chapters opens. Would there be therein sufficient matter at stake to evidence that the Wolffian Metaphysics is grounded in a psychological experience? Hence the author tests here such a hypothesis through the successive analysis of the status of Ontology, of Logics and of empirical Psychology, through a joint reading of the German Metaphysics and of the German Logics. (shrink)

In recent years, neurophysiological evidence has accumulated in favor of a common coding between perception and execution of action. We review findings from recent neuroimaging experiments in the action domain with three complementary perspectives: perception of action, covert action triggered by perception, and reproduction of perceived action (imitation). All studies point to the parietal cortex as a key region for body movement representation, both observed and performed.

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)

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)

Objective: Body dissatisfaction is a major risk factor underlying vulnerability to eating disorders. Laboratory settings suggest that body dissatisfaction could be improved by using evaluative conditioning (EC). The present study evaluates the feasibility of using an EC app in everyday life and the effects of its use on body dissatisfaction. Method: We designed a game-like app inspired by the Therapeutic Evaluative Conditioning app. 60 participants were randomly assigned to two conditions. Participants in the EC condition had to pair photographs of (...) their own body with positive photographs, while participants in the neutral condition had to pair photographs of their own body with neutral photographs. We tested the effect of use of the app on body dissatisfaction, drive for thinness, self-esteem, mood and eating behaviors. Results: Analysis revealed that participants in all conditions presented a significant decrease in body dissatisfaction and drive for thinness. However, contrary to our hypothesis, these reductions were not greater in the EC condition than in the neutral condition. Conclusions: This is the first study to evaluate the effects of an app-based EC intervention targeting body image. Results appear to be promising and the app could easily be implemented in an ecological setting as it is a low effort, attractive and accessible intervention. However, these findings do not support the idea that evaluative conditioning is responsible for the effects. Results are discussed. (shrink)