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

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

The critique of the dogmatism of a-priorism from the Popperians suffered from the fact that Popper, too, was moving towards a certain dogmatic derivation. According to the a-priorists, in wanting to protect himself from any would-be-critics who would argue against the dogmatism of his approach, Popper left his philosophical foundation free to the critics. In fighting against German essentialism, he found himself in a position that necessitated the abandonment of either his presupposed anti-essentialism, or his critique of the positivists. Popper's (...) success stems less from his ability to rally the anti-historicist positivists towards the search for scientific foundations, than the fact that he was one of the greatest, if not the greatest, theoreticians of the scientific method, and critic of ideological simplicity. (shrink)

En Occident, à partir de 1520, l’Ecclesia una se fragmente en confessions chrétiennes rivales. Cette réalité religieuse nouvelle ne peut être pensée sans mots; mais les néologismes lexicaux nécessaires sont lents à s’imposer. La situation paroxystique de ceux qui changent effectivement d’Église dans les années 1520-1650 est pourtant favorable à de telles créations. Elle permet de trouver les mots pour dire, et donc pour admettre, l’existence de l’Autre Église.

Plusieurs de ceux qui présentent des problèmes de santé mentale se retrouvent dans le système judiciaire. Leur profil clinique se caractérise par une problématique complexe où se juxtaposent divers troubles ou déficits. Il n’est pas toujours facile de dépister ces personnes et d’intervenir auprès d’elles dans le cadre du processus judiciaire et pénal, qui n’est pas conçu pour répondre à leurs besoins cliniques. De son côté, le réseau de la santé et des services sociaux semble lui aussi peu adapté pour (...) intervenir auprès de cette clientèle marginale, souvent réfractaire à l’aide et parfois intimidante. Ces deux réseaux fonctionnent en parallèle, très peu familiers l’un de l’autre. Ils ont tendance à se renvoyer cette clientèle problématique. L’État doit s’assurer de soutenir et de coordonner des services qui peuvent rejoindre et aider ces personnes. (shrink)

The present paper examines how discursive representations and emotive constructions underpin an argumentative dynamic that emerges from apparently non-argumentative statements, like those found in newspaper headlines. Our data comes from Greek broadsheet newspapers in the polarized context of the Greek crisis. First, we outline an analytic synergy that scrutinizes representational meaning and the semiotization of emotions in headlines. We then move towards the reconstruction of the inferential passage, contained in the headlines, that unites the implicit standpoint with its supporting argument.

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

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)

This paper assesses the problem of the possible tension between development and environmental protection, especially for developing countries. Some leaders of these countries like Jacob Zuma claim for example that poor countries should only join the fight against climate change if it does not compromise their economic development, thus suggesting that environmental protection is more often than not an obstacle to economic development. I argue that this argument is if not misleading, at least incomplete because it does not take the (...) diversity of environmental protection seriously and reduces development to economic development. In fact, some aspects of environmental protection may clearly clash with some kinds of economic development. In that line, when countries are still very poor, their economic development should take priority over some ecological-friendly policies. But this is only one side of the truth. The other side of the truth is that some ecologically-friendly policies can also make poor countries richer, more democratic and fairer. (shrink)

Devenir borgne! Difficile de ne pas vivre ce handicap comme un drame. Sans la vision binoculaire et stéréoscopique, le réel semble n'avoir plus d'épaisseur. L'auteur rapporte ce qu'il a éprouvé au cours de sa prise en charge ophtalmologique et interroge en même temps les peintres malvoyants et les philosophes : qu'est-ce que voir? Le handicap visuel permettrait-il de dépasser l'ordinaire de la vision? Pour répondre à ces questions, Monet, Degas, Victor Brauner sont interpellés dans leurs oeuvres ou encore Bruegel et (...) Rembrandt, en même temps que sont convoqués Platon, Descartes, Alain, Merleau-Ponty ou encore James Joyce et William Blake, sans oublier les Évangiles. Les bien-voyants ne se rendent pas compte qu'ils sont condamnés à vivre la tyrannie du réel. Et si les yeux empêchaient de voir en vrai? Le genre humain n'a peut-être pas vocation à voir mais à entrevoir. Dans ces conditions, ne devrait-on pas considérer la malvoyance comme un atout? Ne serait-il pas temps de voir autrement qu'avec les yeux? Peut-être, alors, sentira-t-on la présence de l'Être émerger de la pénombre"--Page 4 of cover. (shrink)

The classical experimental methodology is ill-suited for the investigation of the behavioral and physiological correlates of natural social interactions. A new experimental approach combining a natural conversation between two persons with control conditions is proposed in this paper. Behavior, including gaze direction and speech, and physiology, including electrodermal activity, are recorded during a discussion between two participants through videoconferencing. Control for the social aspect of the interaction is provided by the use of an artificial agent and of videoed conditions. A (...) cover story provides spurious explanations for the purpose of the experiment and for the recordings, as well as a controlled and engaging topic of discussion. Preprocessing entails transforming raw measurements into boxcar and delta functions time series indicating when a certain behaviour or physiological event is present. The preliminary analysis presented here consists in finding statistically significant differences between experimental conditions in the temporal associations between behavioral and physiological time series. Significant results validate the experimental approach and further developments including more elaborate analysis and adaptation of the paradigm to functional MRI are discussed. (shrink)