Les logiques : notes en vrac

I’ve written before about “structural” foundations for mathematics, which can also be thought of as “typed” foundations, in the sense that every object comes with a type, and typing restrictions prevent us from even asking certain nonsensical questions. For instance, whether the cyclic group of order 17 is equal to the square root of 2 is such a nonsensical question, since the first is a group while the second is a real number, and only things of the same type can be compared for equality.

J’ai précédemment écrit à propos de fondations « structurelles » pour les mathématiques, qui peuvent aussi être comprises comme des fondations « typées », dans le sens ou chaque objet a son type, et que les règles de typage nous gardent de poser des questions insensées. Par exemple, se demander si le groupe cyclique d’ordre 17 est égale à la racine carrée de 2, est un exemple de question sans aucun sens, vu que le premier est un groupe tandis que le second est un nombre réel, et que seulement des choses du même type peuvent être dites égales.

Dependent types are also everywhere in natural language. One standard example is that for any month m, there is a type (or set) D(m) of the days in that month. Since different months have different numbers of days, the cardinality of D(m) is different for different m. Of course, because of leap years, D actually depends not only on m but also on a year y. David gave a couple of nice examples here of the need for dependent types in expressing quantifiers in everyday language.

Les types dépendants sont aussi présents partout dans le langage naturel. Un exemple standard est celui est que à tous mois m, est associé un type (ou ensemble) D(m) des jours dans le mois. Comme les différents mois ont différents nombres de jours, le cardinal de D(m) est différent pour les différents m. Bien sûr, en conséquence des années bissextile, D ne dépend pas seulement de m, mais aussi de l’année y. David a donné un ensemble de beaux exemples ici, de l’utilité des types dépendants pour exprimer les quantificateurs du langage de tous les jours.

It is well-known, due to the work of Girard and Coquand, that adding polymorphic domains to higher order logic, HOL, or its type theoretic variant λHOL, renders the logic inconsistent. This is known as Girard’s paradox. But there is also a another presentation of higher order logic, in its type theoretic variant called λPREDω, to which polymorphic domains can be added safely. Both λHOL and λPREDω are well-known type systems and in this paper we study why λHOL with polymorphic domains is inconsistent and why and λPREDω with polymorphic domains remains consistent. We do this by describing a simple model for the latter and we show why this can not be a model of the first.

Il est connu, depuis les travaux de Girard et Coquand, qu’étendre aux domaines du polymorphisme, la logique d’ordre supérieur, HOL, ou sa variante de la théorie des types, λHOL, rend cette logique incohérente. Ce phénomène est connu comme paradoxe de Girard. Mais il existe une autre forme de logique d’ordre supérieur, dans sa variante de la théorie des types, nommée λPREDω, à laquelle les domaines du polymorphisme peuvent être ajoutés de manière fiable. Autant λHOL que λPREDω sont des systèmes de types bien connus et dans ce document nous étudions la raison pour laquelle λHOL avec les domaines du polymorphisme est incohérente et pourquoi λPREDω avec les domaines du polymorphisme, reste cohérente. Nous le faisons en décrivant un modèle simple pour cette dernière et nous montrons pourquoi il ne peut pas être un modèle de cette première.

Computational type theory, like all type theories, is related to a foundational theory for mathematics originating with Bertrand Russell (Russell, 1908 a,b) as an attempt to deal with certain contradictions such as Russell's Paradox about the set R of all sets that are not members of themselves, denoted {x | x ∉ x} , a circular definition. The paradox arises from asking whether R belongs to R . Russell's theory of logical types was designed to prevent so called vicious circles in definitions which led to contradictions in mathematical reasoning.

La Théorie des Types Algorithmiques, comme toutes les théories des types, est liée à une théorie des fondements des mathématiques, prenant naissance avec Bertrand Russel (Russel, 1908 a,b) comme tentative de travailler certaines contradictions, telle que le Paradoxe de Russel, à propos de l’ensemble R de tous les ensembles qui ne sont pas membres d’eux‑mêmes, noté {x | x ∉ x}, une définition circulaire. Le paradoxe apparait quand on veut savoir si l’ensemble R appartient à R. La théorie des types logique, de Russel, fût conçu de manière à prévenir les dits cercles vicieux dans des définitions qui aboutissent à des contradictions dans les raisonnements mathématiques.

In PM and STT, types are used to render the notions of class and propositional function free from vicious circles. A type is the domain of significance of a propositional function, i.e. those objects that the proposition is about, and that domain can not include the proposition itself. What Russell believed is that there can't be a single universal type of all meaningful objects on which propositions are defined because that type would include the propositions being defined, creating a vicious circle. Instead, the universe must be divided into categories, Aristotle's terminology, or types.

Dans PM et la STT, les types sont utilisés pour exprimer les notions de classes de fonctions propositionnelles, exemptes de tout cercle vicieux. Un type est le domaine de pertinence de la signification d’une fonction propositionnelle, c‑à‑d. les éléments sur lesquels porte la proposition, et ce domaine ne peut inclure la proposition elle‑même. Ce que Russel a crut, c’est qu’il ne peut pas exister un unique type universel de tous les objets ayant un sens, à propos desquels des propositions sont définies, car ce type devrait inclure la proposition ainsi définie, aboutissant à un cercle vicieux. Au lieu de ça, l’univers doit être divisé en catégories, une terminologie d’Aristote, ou des types.

Principia Mathematica was also designed to demonstrate that mathematics could be reduced to logic, say to truth values and higher-order functions over them – specifically to predicative logic which avoids the concept of all functions or all propositions. This is one reason that PM did not start with a primitive notion of natural numbers nor with a notion of individuals as in HOL, namely, Russell and Whitehead wanted to derive mathematical concepts such as natural numbers and real numbers from more basic logical concepts. Unfortunately, the core PM foundation is inadequate for classical mathematics, even for natural numbers, without an axiom of reducibility in the typing rules, which is a way to introduce so called impredicative notions, those whose definition quantifies over a collection including the concept being defined.

Principia Mathematica a aussi été conçu pour démontrer que les mathématiques pouvaient se ramener à la logique, c’est‑à‑dire à des valeurs de vérité et des fonctions d’ordre supérieur sur ces premières — spécifiquement à la logique prédicative qui permet d’éviter le concept du tout‑fonction ou du tout‑proposition. C’est une raison pour laquelle PM ne démarrât pas avec une notion primitive des nombres naturels, ni avec une notion d’individuels comme en HOL; nommément, Russel et Whitehead voulurent dériver des concepts mathématiques comme les nombres naturels et les nombres réels, à partir de concepts logiques plus basiques. Malencontreusement, le cœur de fondation de PM, est inapproprié aux mathématiques classiques, même aux nombres naturels, sans un axiome de réductibilité dans les règles de typage, une manière d’introduire les notions dites imprédicatives, celles dont la définition quantifie dans une collection incluant le concept ainsi défini.

Axiom introduced by Russell and Whitehead in Principia Mathematica. In that system propositional functions are sorted into levels, as part of the ramified theory of types. The axiom says that for any function at any level there exists a formally equivalent function at the first level. The axiom is needed to allow the construction of elementary mathematics, in particular to certify the principle of mathematical induction. Its effect, as Ramsey pointed out, was largely to nullify the point of introducing different orders of functions.

Axiome introduit par Russel et Whitehead dans Principia Mathematica. Dans ce système, les fonctions propositionnelles sont rangées en niveaux, selon la théorie ramifiée des types. Cet axiome dit que pour toute fonction à n’importe quel niveau, il existe une fonction strictement équivalente au premier niveau. Cet axiome est nécessaire pour rendre possible la construction des mathématiques élémentaires, en particulier pour certifier le principe de l’induction mathématique. Elle eût, comme l’a fait remarquer Ramsey, pour effet de largement rendre caduque l’idée d’introduire différents degrés pour les fonctions.

Russell and Whitehead tried unsuccessfully to base mathematics on a predicative type theory; but, though reluctant, they had to introduce an additional axiom, the axiom of reducibility, which rendered their enterprise impredicative after all.

Russel et Whitehead tentèrent en vain de baser les mathématique sur une théorie prédicative des types; mais, bien que réticents, ils ont dut introduire un axiome additionnel, l’axiome de réductibilité, qui rendît leur ouvrage imprédicatif, finalement.

Intuitionnisme et constructivisme, semble bien être synonymes.

Constructive Type Theory and Interactive Theorem Proving (jaist.ac.jp) [PDF]. 2005.

Citation : 

Now it is the contention of the intuitionists (or the constructivists, I shall use these terms synonymously) […]