1907-2007 : cent ans d'intuitionnisme (2007)

RÉSUMÉS :

Mohammad ARDESHIR: L'intuition chez Brouwer et Sührawardi
La notion d’"intuition" chez Brouwer est demeurée opaque pendant un siècle, 1907-2007. Dans ses écrits, Brouwer emploie deux versions de la notion, "ur- [originaire, primordiale] intuition" et "intuition". Il me semble que chez Brouwer la notion d’"ur-intuition" est fondamentale (voir, e.g., [1], page 97), tandis que la notion d’"intuition" est globale (voir, e.g., [1], page 52). Le trait commun aux deux versions est l’idée de construction. Cela signifie que la notion épistémologique de l'intuition est liée à la notion ontologique de construction. Dans sa critique du péripatéticien d’Ibn Sina (Avicenne), Sührawardi (1155-1191), un philosophe perse, a fondé sa philosophie "illuminationiste" (Ḥekmāt al-ishraq). Cette philosophie provient du mot arabe ishraq, signifiant "lever", notamment "lever du soleil". Le mot est également lié, en arabe, à l’"orient", ce qui représente une forme spécifiquement orientale de pensée philosophique, une forme de pensée qui, contrairement à la raison discursive, est intuitive et immédiate. Nous montrerons que la notion brouwerienne d'intuition peut être interprétée dans la théorie de la "connaissance par la présence" présentée d'abord par Sührawardï.

Références Bibliographiques :

[1] Brouwer, L. E. J., "On the foundation of Mathematics", 1907, in [2], pp. 11-101.
[2] Brouwer, L. E. J., Collected works, vol. 1, edited by A. Heyting, North-Holland, 1975.
[3] Sührawardi, Sh., Collected works, edited by H. Corbin and S. H. Nasr, vols., 1-4, (Farsi and Arabic), Institute for humanities and cultural studies, 2002, Tehran.

Henk BARENDREGT: Brouwer et le mysticisme
On peut distinguer dans la conscience instantanée, qu'on a tout le temps pendant sa vie, un contenu et un type. Quand on voit une couleur, par exemple, vert ou rouge peuvent être des éléments de contenu, tandis que la joie ou la tristesse peuvent être des types. Dans la vie quotidienne généralement on optimise les contenus. Pour cette raison l'on désire souvant avoir une femme belle, une grande maison et un voiture neuve, même si ces trois choses n'apportent pas toujours le bonheur. Dans le mysticisme on n'optimise pas le contenu, mais le type de la conscience. On se dirige directement vers le bonheur. Or, il y a deux espèces de mysticisme: celui de la concentration (sammatha), dirigé vers l'augmentation des types positifs, et celui de l'intuition (vipassana), dirigé vers la diminution et finalement l'élimination des types négatifs. Dans cette conférence on donne une description de ces deux voies du mysticisme et on essaie de décrire le niveau où L.E.J. Brouwer est arrivé avec le développement de son mysticisme.

Douglas BRIDGES: Les "Reverse Mathematics" constructives (Constructive Reverse Mathematics)
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Constructive reverse mathematics is reverse mathematics carried out in Bishop-style constructive math (BISH) — that is, using intuitionistic logic (and, where necessary, constructive ZF set theory). There are two primary foci of constructive reverse mathematics:
- first, investigating which constructive principles are necessary to prove a given constructive theorem;
- secondly, investigating what non-constructive principles are necessary additions to BISH in order to prove a given non-constructive theorem.
I will present recent work on constructive reverse mathematics, carried out with Josef Berger and Hannes Diener. The main theme of the talk is the connection between the antithesis of Specker's theorem, the uniform continuity theorem, versions of the fan theorem, and Ishihara's principle BD-N.

AMS Classification : 03F60 Constructive and recursive analysis ; 03F55 Intuitionistic mathematics.
Keywords : constructive, reverse mathematics, uniform continuity, Specker's theorem.

Références Bibliographiques :

Josef Berger and Douglas Bridges, A fan-theoretic equivalent of the antithesis of Specker's theorem, Proc. Koninklijke Nederlandse Akad. Wetenschappen (Indag. Math.), to appear.
Douglas Bridges, Uniform continuity theorems and the antithesis of Specker's theorem, preprint, University of Canterbury, 2006.
Douglas Bridges and Hannes Diener, The pseudocompactness of [0 ; 1] is equivalent to the uniform continuity theorem, preprint, University of Canterbury, 2006.
Douglas Bridges and Luminita Simona, Techniques of Constructive Analysis, Universitext, Springer-New-York, September 2006.

Bernd BULDT: Que nous dit le temps dans les mathématiques (intuitionnistes)?
Recently, various author have made claims as to the importance of internal or phenomenological time in the foundations of (intuitionistic) mathematics. The paper starts out with a survey andcritical assessment of these claims. It then investigates whether the professed insights and theapproaches based on them are still viable options in the philosophy of mathematics.

Jean FICHOT: L'interprétation fonctionnnelle de Gödel: constructivité et calculabilité
De 1933 à 1972, un des buts de Gödel a été de donner une interprétation constructive et prédicative de l'arithmétique classique (AP) permettant de se convaincre de sa non-contradiction. Une traduction de AP dans l'arithmétique intuitionnisme (AH), à elle seule, ne pouvait satisfaire Gödel car la justification de cette dernière, telle qu'elle était donnée par Heyting, reposait sur une notion de preuve imprédicative. Gödel proposa alors de traduire AH dans une extension de l'arithmétique récursive primitive permettant de définir des fonctionnelles de type fini (T) dont la non-contradiction dépendait à son tour d'un concept de fonction calculable de type fini. Cette notion était supposée ne pas dépendre du concept de preuve constructive et, de plus, ne pas souffrir de ses défauts. Gödel lui-même ne s'est jamais satisfait de ses tentatives visant à formuler cette proposition de façon convaincante. Malgré tout, le sentiment qu'une certaine réduction a été obtenue demeure. Nous essayons de montrer la portée et quelques-unes des limites de cette réduction.

Marcel GUILLAUME: De quelques contributions de mathématiciens du début du XIXe siècle au débat sur les fondements
Nous rappellerons les contributions de Schoenflies à la théorie des ensembles, qui suscita les objections et donc la réflexion de Brouwer, ainsi que celles de Julius König, qui rejette hors des lois de la logique aussi bien le principe de contradiction que celui du tiers exclu, dans son testament scientifique sur les Nouveaux fondements de la logique, de l’arithmétique et de la théorie des ensembles, dont Bernays reconnaît le caractère précurseur de la théorie hibertienne de la démonstration, et auquel Von Neumann, qui doit en partie sa formation à sa lecture, rend hommage, dans un article sur la théorie de la démonstration.

Références Bibliographiques :

P. Bernays, Hilberts Untersuchungen über die Grundlagen der Arithmetic, in D. Hilbert, Gesammelte Abhandlungen III (Berlin: Springer, 1935), 196-216.
L.E.J. Brouwer, L.E.J. Brouwer collected works 1 (Amsterdam-Oxford: North Holland; New-York: American Elsevier, 1975).
J. König, Neue Grundlagen der Logik, Arithmetik und Mengenlehre (Leipzig: Veit, 1914).
A. Schoenflies, Entwickelung der Mengenlehre und ihrer Anwendungen, Erst Hälfte : Allgemeine Theorie der unendlichen Mengen und theorie der Punktmengen (Leipzig & Berlin: Teubner, 1913).
J. Von Neumann, Zur Hilbertschen Beweistheorie, Mathematische Zeitschrift 26 (1927), 1-46.

Per MARTIN-LÖF: La controverse Hilbert Brouwer résolue?
Developments in proof theory (Hilbert) on the one hand and constructive mathematics (Brouwer) on the other during the last decade or two have led to such a remarkable convergence of the two at the outset opposed foundational schemes that it might not be inappropriate to speak of a resolution of the Hilbert-Brouwer controversy that reached its peak in the 1920's. The purpose of my talk will be to report on these developments.

Charles McCARTY: Le nouvel intuitionnisme (The New Intuitionisn)
Antirealism, loosely based on proof-theoretic semantics, has been proven inconsistent, in its most prominent formulation, with intuitionistic mathematics. The philosophies of Brouwer and Heyting retain a certain antiquarian appeal. Mathematical logic appears to be fading as an intellectual force. The foundational questions surrounding intuitionism can, it seems, only be approached on the basis of a new philosophical outlook, one that takes seriously the idea that the only suitable foundation for a mathematics consists not of logic, but of more mathematics. We will endeavor to describe, in general terms, such an outlook foundational with respect to intuitionism and to compare it critically with existing alternatives.

Philippe NABONNAND & Gerhard HEINZMANN: L'intuition chez Poincaré et Brouwer
Brouwer discute à plusieurs reprises de la relation entre l’intuitionnisme et les positions de Poincaré. Le diagnostic de Brouwer reflète bien les similitudes et les différences entre ses positions et celles de Poincaré. Ils partagent la conviction que l’intuition est un des garants de la certitude inhérente aux mathématiques et que l’induction complète est le "raisonnement mathématique par excellence". Par contre, Poincaré considère l’intuition comme l’unique base de la construction mathématique et leurs positions diffèrent en ce qui concerne les relations entre intuition et langage. Nous discuterons dans cette conférence des positions de Poincaré au sujet de ces questions et analyserons dans quelle mesure les points de vue différents de Brouwer et Poincaré au sujet de l’intuition impliquent une conception différente de l’induction complète.

Carl POSY: L'infini brouwerien (Brouwerian Infinity)
Infinity is a defining notion for any mathematical constructivist. In this talk I will explore the development of Brouwer's views about mathematical infinity from his dissertation through his late work in the 1950's. I will suggest that his views about infinity — and about our intuitive grasp of infinite objects — developed through three distinct stages, and will argue that Brouwer's moves from one stage to the next were driven by both mathematical and philosophical concerns. I hope also to show how this focus on infinity and intuition can shed new light on the connection and contrast between Brouwer's intuitionism on the one hand and other constructivist mathematical views (including those of Kant, the French pre-intuitionists and Bernays) on the other.

Giovanni SAMBIN: Deux applications du constructivisme dynamique: le principe de continuité de Brouwer et les suites de choix dans la topologie formelle (Two applications of dynamic constructivism: Brouwer's continuity principle and choice sequences in formal topology)
In dynamic constructivism* the origin of concepts is seen to be a dialectical process between two requirements: convenience of abstractions and faithfulness to reality. The essence of constructivism is then shifted and becomes awareness of the level of abstraction and its uses, rather than a static self-limitation to certain principles. This is perfectly consonant with a minimalist foundation** of mathematics, which in particular is based on two different levels, one for computational (intensional) and one for geometrical (extensional) aspects of mathematics.
After a short general introduction, dynamic constructivism is illustrated by two specific applications, which exploit formal topology over a minimalist foundation. I will show under which assumptions Brouwer's principle, saying that all functions on the real numbers are continuous, can be proved and generalized. And I will argue for a rigorous and simple definition of choice sequences, and will confront them with lawlike sequences. If time permits, I will also report on work in progress (with M. E. Maietti) aiming to find topological equivalents of the axiom of choice.

* G. Sambin, Steps towards a dynamic constructivism, in: In the scope of Logic, Methodology and Philosophy of Science, vol. 1, P. Gärdenfors, J. Wolenski, K. Kijania-Placek eds., Synthese Library 315, Kluwer 2002, pp. 263-286.
** M. E. Maietti - G. Sambin, Toward a minimalist foundation for constructive mathematics, in: From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, L. Crosilla, P. Schuster, eds., Oxford Logic Guides 48, Oxford U. P. 2005, pp. 91--114.

Peter SCHRÖDER HEISTER: La justification opérative de la logique intuitionniste selon Lorenzen
Je souhaite démontrer que le fondement opérationnel de la logique intuitionniste établi par Lorenzen mérite davantage d’attention que celle qu'on lui porte actuellement. L’approche de Lorenzen anticipe de nombreuses idées de la théorie sémantique de la démonstration dans le sens de Dummett et Prawitz. Sa théorie de l’admissibilité de règles peut être interprétée en tant que définition de la validité d’énoncés d’implication. Pour la justification de règles logiques, l’approche opérationnelle me paraît être plus fondamentale que la justification de la logique par des dialogues ou en termes de jeux établis plus tard par Lorenzen.

Anton SETZER: Théorie de la démonstration et théorie des types de Martin-Löf (Proof Theory and Martin-Löf Type Theory)
La théorie ordinale de la démonstration a pour but de réduire la consistance des théories mathématiques formelles à la bonne fondation de systèmes de notation ordinale. Afin d’obtenir une solution satisfaisante au problème de la consistance, cette réduction doit être complétée par une seconde étape, à savoir, la preuve du caractère bien fondé des systèmes de notation ordinale pour les théories pour lesquelles on dispose d’un argument montrant que tout ce qui est établi dans ces théories est correct. En vertu du théorème d’incomplétude de Gödel, un tel argument ne peut être que de nature philosophique. Les théories pour lesquelles de tels arguments ont été le mieux élaborés sont des extensions de la théorie des types de Martin-Löf. Dans cet exposé, nous étudierons la façon dont une telle réduction peut être menée à bien pour la théorie des ensemble de Kripke Platek avec un ordinal récursivement inaccessible. Nous analyserons les limitations rencontrées dans ce cas par un argument philosophique de consistance. Enfin, nous regarderons la théorie des ensembles de Kripke Platek étendue par un nouvel ordinal, et les résultats obtenus dans ce cas quant à la réduction.

Göran SUNDHOLM & Mark VAN ATTEN: L'interprétation correcte de la logique intuitionniste (The Proper Interpretation of Intuitionistic Logic)
A plausible reading of Brouwer's 1927 proof of the bar theorem suggests that for him the principle of Bar Induction amounts to nothing but closure of all of mathematics under the Bar Rule. In the light of this, a likely difference between the constructive and specifically intuitionistic renderings of implication will be discussed.

Richard TIESZEN: A l'intersection de l'intuitionnisme et de la phénoménologie (The Intersection of intuitionism and phenomenology)
In the nineteen twenties and early nineteen thirties Brouwerian intuitionism was brought into association with Husserlian phenomenology in the work of Hermann Weyl, Oskar Becker, and Arend Heyting. It is not surprising that this happened, since human subjectivity and consciousness were taken seriously in both intuitionism and phenomenology. Although there are some significant differences between their views, neither Brouwer nor Husserl wished to objectify mathematical consciousness, to reduce it to something else, or to ignore it. In my lecture I want to show why it would be held, on the grounds of a particular subset of phenomenological ideas about the mind (and without a detour through the philosophy of language), that classical logic and mathematics should be rejected in favor of intuitionistic logic and mathematics.

Wim VELDMAN: Quelques applications du théorème de la barre de Brouwer
Brouwer a introduit son théorème de la barre qu’on peut plus ou moins identifier avec la thèse philosophique sur laquelle il a fondé ce théorème, au moment qu’il voudrait établir le théorème de l'éventail et la continuité uniforme de toute fonction de l’intervalle [0, 1] dans R. Il n’a jamais fait autre usage de sa thèse surprenante. Néanmoins, cette thèse a des conséquences beaucoup plus profondes que le théorème de l'éventail. On va mentionner quelques applications de la thèse de Brouwer, notamment dans la théorie déscriptive des ensembles et le programme des mathématiques renversées. Après, on va voir comment un ancien résultat de Cantor est sauvé par la thèse de Brouwer. C’est le théorème disant que tout sous-ensemble fermé de R qui est énumerable est réductible. Il faut introduire la notion d’un ensemble provisoirement énumerable. Une suite x₀, x₁, ... d'éléments d’un sous-ensemble X de R est une énumeration provisoire de X quand, pour toute suite e₀, e₁, ... de nombres rationnels positives, pour tout élément x de X, on peut déterminer n tel que |x - x_n| < e_n. Ça veut dire que toute tentative de prouver que la suite x₀, x₁, ... n’est pas une énumeration de X est en vain. Il se trouve qu’un sous-ensemble fermé et localisé de R est provisoirement énumérable si et seulement si l’ensemble est réductible au sens de Cantor.