by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Mathematics, Calculus, Geometry, Entry Directory]
[Logic and Semantics, entry directory]
[Heyting’s Les fondements des mathématiques, entry directory]
[The following is summary. I am not a mathematician, so please consult the original text instead of trusting my summarizations, which are possibly mistaken and probably inelegantly articulated. Also, my abilities with French are insufficient to translate reliably, so please again rely upon the quotations rather than my summarizations. Bracketed comments and subsection divisions are my own. Proofreading is incomplete, so please forgive my mistakes.]
Summary of
Arend Heyting
Les fondements des mathématiques.
Intuitionnisme.
Théorie de la démonstration.
Première section:
Intuitionnisme
5.
L'intuitionnisme brouwérien
5.1
L'intuition mathématique
5.1.1
Mathématique sans négation de Griss
Brief summary:
(5.1.1.1) Griss devised a negationless intuitionistic mathematics. He thought there should be nothing like negation in it, because intuitive methods will not allow us to make a demonstration based on the falsity of an assumption, as we cannot clearly conceive a falsity in the first place. And we can only clearly conceive a property after constructing a mathematical entity that possesses that property, so we cannot introduce an empty species. For real numbers, Griss needs to avoid the negational (and exclusionary) notion of inequality, but he still needs to be able to say that one natural number is not identical to the other ones (and that two numbers are identical when they cannot be unequal). Instead of conceiving this in terms of not being equal (which cannot enter into intuitionistic thinking, because we can only conceive of positive properties), Griss (according to Heyting) recasts this inequality relation (≠) as a distance relation (⧣). On this basis, we can understand two (initially unidentified) numbers as being equal when they share the same distances to the same other numbers. (2 for instance is one away from 1 and one away from 3, and two away from 4, etc. If both a and b each likewise are one away from 1, one away from 3, etc., then they are equal. Here we are avoiding the non-intuitionistic notion of them not being unequal to one another by having them both positively sharing the same relational properties to all the other numbers in the set.) Heyting writes, in rough translation: In the theory of real numbers, the relation ≠, being negative, does not intervene. There is only the relation a = b and the distance relation a ⧣ b (see “numerical calculation” below). The theorem “if a ≠ b is impossible, then a = b” is replaced by the following: “if a is distant from every number c which is distant from b, a = b”. (Heyting p.14). (5.1.1.2) But if we completely eliminate negation, then we cannot have a propositional logic in the normal sense. Nonetheless, both Griss and Destouches-Février attempt to construct such a propositional logic. But instead of being a logic of predicates, Griss here constructs a logic of classes that is unlike the intuitionistic logic of classes in that for Griss, two classes can intersect only if they have at least one element in common. (5.1.1.4) Van Dantzig outlined a formal system of affirmative mathematics. (5.1.1.5) Brouwer supports the role of negation by constructing theories that require it, and he articulated his ideas about the relationship of mathematics to experience, language, and wisdom.
[Griss’ Negationless Mathematics; His Elimination of Negational Structures, in Particular His Use of Distance (⧣) in Place of Inequality (≠)]
[Griss’ and Destouches-Février’s Negationless Intuitionistic Logic]
[Destouches-Février devises a logic of constructions, on the basis of which she defines a logic of problems and a propositional logic.]
[Van Dantzig’s Affirmative Mathematics]
[Brouwer and Negation]
Summary
[Griss’ Negationless Mathematics; His Elimination of Negational Structures, in Particular His Use of Distance (⧣) in Place of Inequality (≠)]
[Griss devised a negationless intuitionistic mathematics. He thought there should be nothing like negation in it, because intuitive methods will not allow us to make a demonstration based on the falsity of an assumption, as we cannot clearly conceive a falsity in the first place. And we can only clearly conceive a property after constructing a mathematical entity that possesses that property, so we cannot introduce an empty species. For real numbers, Griss needs to avoid the negational (and exclusionary) notion of inequality, but he still needs to be able to say that one natural number is not identical to the other ones (and that two numbers are identical when they cannot be unequal). Instead of conceiving this in terms of not being equal (which cannot enter into intuitionistic thinking, because we can only conceive of positive properties), Griss (according to Heyting) recasts this inequality relation (≠) as a distance relation (⧣). On this basis, we can understand two (initially unidentified) numbers as being equal when they share the same distances to the same other numbers. (2 for instance is one away from 1 and one away from 3, and two away from 4, etc. If both a and b each likewise are one away from 1, one away from 3, etc., then they are equal. Here we are avoiding the non-intuitionistic notion of them not being unequal to one another by having them both positively sharing the same relational properties to all the other numbers in the set.) Heyting writes, in rough translation: In the theory of real numbers, the relation ≠, being negative, does not intervene. There is only the relation a = b and the distance relation a ⧣ b (see “numerical calculation” below). The theorem “if a ≠ b is impossible, then a = b” is replaced by the following: “if a is distant from every number c which is distant from b, a = b”. (Heyting p.14).]
[In rough form: Griss’ Negationless Mathematics. Griss [1,2] expressed expressed doubts about the legitimacy of the use of negation in intuitionistic mathematics. According to him, one can never demonstrate by intuitive methods the falsity of an assumption, because if it is false one cannot conceive it clearly. Likewise, one can have a clear idea of a property only after the construction of a mathematical entity that possesses this property. Thus we cannot introduce an empty species. GRISS began the construction of a negationless intuitionistic mathematics. In the theory of real numbers, the relation ≠, being negative, does not intervene. There is only the relation a = b and the distance relation a ⧣ b (see “numerical calculation” below). The theorem “if a ≠ b is impossible, then a = b” is replaced by the following: “if a is distant from every number c which is distant from b, a = b”. The demonstration of this theorem for real numbers creates difficulties; GRISS only succeeds by using BROUWER’s theorem on bounded expansions [déploiements bornés] (see “Bon ordre” below). Mme. DEQUOY studied projective geometry as understood without negation [1,2].] [With explanation: G.F.C. Griss formulated a negationless mathematics based on L.E.J. Brouwer’s intuitionism. Van Stigt explains in “Brouwer’s Intuitionist Programme” section 1.5.1.1 that “In the generation of the fundamental “mathematical entities,” such as the natural numbers and the Brouwer set or spread and its elements, there is no place nor immediate need for negation” (Van Stigt, section 1.5.1.1, p.14, boldface mine). But, negation does factor in when dividing a set into subsets, where to be in a set means it is impossible to be in the complementary set (Van Stigt, section 1.5.1.1, p.14; Griss “Negationless Intuitionistic Mathematics, II” section 1.0.2, p.457). Griss, we saw, was seeking a way to make such a designation without using logical negation or the law of excluded middle. Brouwer’s formulation uses the idea that an item is either in a particular subset or it is not. Such a move normally is founded in classical logic using excluded middle, and it need not be further proved. Griss’ formulation instead says that something is either in one subset or in its complement, and he needed to formulate a proof for this disjunction, which runs parallel to Brouwer’s formulation (see Griss’s “Negationless Intuitionistic Mathematics, I” sections 0 and 1.2 (and especially section 1.2.3 for the parallelism between his and Brouwer’s formulations); and see “Negationless Intuitionistic Mathematics, II” section 1.0). Heyting then writes, roughly, that according to Griss, one can never demonstrate by intuitive methods the falsity of an assumption, because if it is false one cannot conceive it clearly. As Griss writes in “Negationless Intuitionistic Mathematics, I,” section 0.2:
On philosophic grounds I think the use of the negation in intuitionistic mathematics has to be rejected. Proving that something is not right, i.e. proving the incorrectness of a supposition, is no intuitive method. For one cannot have a clear conception of a supposition that eventually proves to be a mistake. Only construction without the use of negation has some sense in intuitionistic mathematics.
(Griss, “Negationless Intuitionistic Mathematics, I,” section 0.2, p.1127)
Heyting next says, roughly: “Likewise, one can have a clear idea of a property only after the construction of a mathematical entity that possesses this property. Thus we cannot introduce an empty species.” Griss notes and emphasizes this in section 1.0.3 of “Negationless Intuitionistic Mathematics, II”
In 1947 Prof. L. E. J. BROUWER gave a formulation of the directives of intuitionistic mathematics 2). It is remarkable that negation does not occur in an explicit way, so one might be inclined to believe negationless mathematics to be a consequence of this formulation. The notion of species, however, is introduced in this way (translated from the Dutch text): “Finally in this construction of mathematics at any stage properties that can be supposed to hold for mathematical conceivabilities already obtained are allowed to be added as new mathematical conceivabilities under the name of species”. By this formulation it is possible that there are properties that can be supposed to hold for mathematical conceivabilities already obtained but that are not known to be true. With it negation and null-species are introduced simultaneously but at the cost of evidence. Whatever are the properties that can be supposed? What other criterion could there be than ‘to hold for mathematical conceivabilities already obtained’? In the definition of the notion of species the words “can be supposed” should be replaced by “are known”. One should restrict oneself in intuitionistic mathematics to mathematical conceivabilities and properties of those mathematical conceivabilities and one should not make suppositions of which one does not know whether it is possible to fulfil them. (The well-known turn in mathematics: “Suppose ABC to be rectangular” seems to be a supposition, but mostly means: “Consider a rectangular triangle ABC”).
(457)
2) L. E. J. BROUWER, Richtlijnen der intuïtionistische wiskunde. Proc. Kon. Ned. Akad. v. Wetensch., 50, (1947).
(Griss, “Negationless Intuitionistic Mathematics, II,” section 1.0.3, p.457, italics in the original)
(Also see Griss “Negationless Intuitionistic Mathematics, I,” section 0.10). The next idea is a bit harder to gather from the Griss texts we have examined. Roughly, Heyting says: In the theory of real numbers, the relation ≠, being negative, does not intervene. There is only the relation a = b and the distance relation a ⧣ b (see “numerical calculation” below). The theorem “if a ≠ b is impossible, then a = b” is replaced by the following: “if a is distant from every number c which is distant from b, a = b”. (Heyting, p.14) But as we know from our sources, one of which Heyting cites in this paragraph, Griss does in fact use unequals (≠) for this formulation. Where in Griss is this notion of distance? I have not found it yet. My best current guess is the following. In section 1.3 of Griss’ “Negationless Intuitionistic Mathematics, I,” he discusses the ordering relation of the numbers in the set. Perhaps the notion of distance comes from the fact that if a and b in a set are identically the same number, then they share all the same numerical “distances” to the other numbers in the ordered sequence. But Heyting also notes that this presented difficulties for real numbers. Also, Dequoy worked on a negationless projective geometry.]
Mathématique sans négation de Griss.- ** GRISS [1,2] a exprimé des doutes sur la légitimité de l’emploi de la négation en mathématiques intuitionnistes. Selon lui on ne peut jamais démontrer par des méthodes intuitives la fausseté d’une supposition, car si celle-ci est fausse on ne saurait la concevoir clairement. Egalement on ne peut avoir une idée nette d’une propriété qu’après la construction d’un être mathématique qui possède cette propriété. On ne peut donc par introduire d’espèce vide. GRISS a commencé la construction des mathématiques intuitionnistes sans négation. Dans la théorie des nombres réels la relation ≠, étant négative, n’intervient pas. Il n’y a que la relation a = b et la relation de distance a ⧣ b (voir ci-dessous “calcul numérique”). Le théorème “si a ≠ b est impossible, on a a = b” est remplacé par le suivant : “si a est distant de tout nombre c qui est distant de b, on a a = b”. La démonstration de | ce théorème pour les nombres réels fait des difficultés ; GRISS n’y parvient qu’en utilisant le théorème de BROUWER sur les déploiements bornés (voir ci-dessous, “Bon ordre”). Mlle DEQUOY a étudié la géométrie projective traitée sans négation [1,2].
(14-15)
GRISS, G.F.C.
[1] : Negatieloze intuitionistische wiskunde. Verslagen Akad. Wet. Amsterdam 53 (1944), p. 261–268. (Résumé dans Proc. Akad. Wet. Amsterdam 46, 47, 48, p. 128) ;
[2] Negationless mathematics. I Proc. Akad. Wet. Amsterdam 49 (1946), p. 1127–1133 = Indag. math. 8 (1946), p. 675-681, II ibidem 53 (1950), p. 456–463 = Indag. math. 12 (1950), p. 108–115 ;
(85)
DEQUOY, Mlle N.
[1] : La géométrie projective plane en mathématique intuitionniste sans négation. C.r. Acad. Sc. Paris 228 (1949) p. 1098–1100 ;
2 : Exposé d’un type de raisonnement en mathématique intuitionniste sans négation et résultats obtenus pour la géométrie projective plane. C.r. Acad. Sc. Paris 230 (1950), p. 357–359.
(84)
[Griss’ and Destouches-Février’s Negationless Intuitionistic Logic]
[But if we completely eliminate negation, then we cannot have a propositional logic in the normal sense. Nonetheless, both Griss and Destouches-Février attempt to construct such a propositional logic. But instead of being a logic of predicates, Griss here constructs a logic of classes that is unlike the intuitionistic logic of classes in that for Griss, two classes can intersect only if they have at least one element in common.]
[In rough form: The suppression of negation has important consequences for logic. If only verified assumptions can be considered, such that any logical variable must represent a true proposition, a logic of propositions in the usual sense becomes manifestly impossible. However, attempts to construct a logic that allows for an interpretation that conforms to the requirements of GRISS have been made by Mrs. DESTOUCHES-FÉVRIER [4] and by GRISS [3,4]. Instead of the logic of predicates, Griss constructs a logic of classes that differs from the intuitionist logic of classes by the fact that the intersection of two classes can only be formed if they have at least one element in common.]
La suppression de la négation a des conséquences importantes pour la logique. Si l’on ne peut considérer que des suppositions vérifiées, de sorte que toute variable logique doit représenter une proposition vraie, une logique des propositions dans le sens usuel devient manifestement impossible. Cependant des tentatives pour construire une logique qui admet une interprétation conforme aux exigences de GRISS ont été faites par Mme. DESTOUCHES-FÉVRIER [4] et par GRISS [3,4]. Au lieu de la logique de prédicats GRISS construit une logique des classes qui diffère de la logique intuitionniste des classes par le fait que l’intersection de deux classes ne peut être formée que si elles ont au moins un élément en commun.
(15)
DESTOUCHES-FEVRIER, Mme P.
[4] : Logique de l'intuitionnisme sans négation et logique de l'intuitionnisme positif. C.r. Acad. Sc. Paris 226 (1948), p. 38–39 ;
(84)
GRISS, G.F.C.
[3] : Logique des mathématiques intuitionnistes. C.r. Acad. Sc. 227 (1948) p. 946–948 ;
[4] : Logic of negationless intuitionistic mathematics. Proc. Akad. Wet. Amsterdam 54 (1951), p. 41–49 = Indag, math. 13, p.41–49.
(85)
[Destouches-Février’s Logic of Constructions, of Problems, and of Propositions]
[Destouches-Février devises a logic of constructions, on the basis of which she defines a logic of problems and a propositional logic.]
[In rough form: Mme. DESTOUCHES [3,5,6,7] defines the conception of a constructible mathematics in the strict sense, similar to GRISS. She outlines a logic of constructions, by means of which she defines a logic of problems and a logic of propositions. The notion of the realization of a construction is fundamental. In propositional logic, the conjunction p(a) ∧ q(a) can only be formed if the construction of an element a that satisfies p(x) and q(x) is feasible. DE BENGY-PUYVALLÉE [1] notes that this propositional logic is analogous to the logic to which we are led in wave mechanics.]
Mme. DESTOUCHES [3,5,6,7] définit la conception des mathématiques du constructible au sens strict, voisine de celle de GRISS. Elle esquisse une logique des constructions, au moyen de laquelle elle définit une logique des problèmes et une logique des propositions. La notion de la réalisation d’une construction est fondamentale. Dans la logique des propositions la conjonction p(a) ∧ q(a) ne peut être formée que si la construction d’un élément a qui satisfait à p(x) et à q(x) est réalisable. DE BENGY-PUYVALLÉE [1] remarque que cette logique des propositions est analogue à la logique à laquelle on est conduit en mécanique ondulatoire.
(15)
DESTOUCHES-FEVRIER, Mme P.
[3] : Esquisse d'une mathématique intuitionniste positive. C.r. Acad. Sc. Paris 225 (1947) p.1241–1243;
[5] : Le calcul des constructions. C.r. Acad. Sc. Paris 227 (1948), p.1192–1193 ;
[6] : Connexions entre le calcul des constructions, des problèmes, des propositions. C.r. Acad. Sc. Paris 228 (1948), p.31–33 ;
[7] : Sur l’intuitionnisme et la conception strictement constructive. Proc. Akad. Wet. Amsterdam 51 (1951), p,80–86 = Indag. math. 13 p, 80–86.
(84)
BENGY-PUYVALLÉE, R.DE
[1] : Sur la relation de composabilité dans les logiques de complémentarité. C.r. Acad. Sc. Paris 228 (1949) p. 324–626.
(83)
[Van Dantzig’s Affirmative Mathematics]
[Van Dantzig outlined a formal system of affirmative mathematics.]
[In rough form: VAN DANTZIG [3] has outlined a formal system of affirmative mathematics. He proposes to explicitly indicate in each proposition the construction that leads to it and shows by some examples how this can be done, but he does not indicate how one could execute his program in more complicated cases.]
VAN DANTZIG [3] a ébauché un système formel de mathématiques affirmatives. Il propose d’indiquer explicitement dans chaque énoncé la construction qui y conduit et montre par quelques exemples comment on peut faire cela, mais il n’indique pas comment on pourrait exécuter son programme en des cas plus compliqués.
(15)
DANTZIG, D. Van
[3] : On the principles of intuitionistic and affirmative mathematics. Proc. Akad. Wet. Amsterdam 50 (1947), I p. 918–929, II p. 1092–1103 = Indag. math. 4 (1947), p. 429–440 et p. 506–517 ;
(84)
[Brouwer and Negation]
[Brouwer supports the role of negation by constructing theories that require it, and he articulated his ideas about the relationship of mathematics to experience, language, and wisdom.]
[In rough form: With regard to GRISS and VAN DANTZIG, BROUWER supports the essential role of negation; by broadening the notion of a series of choices, he constructs theories that cannot be formulated without negation (see the end of this chapter). In the conference [34] BROUWER made clear his fundamental ideas about the relationship of mathematics to experience, language, and wisdom.]
Vis-à-vis de GRISS et de VAN DANTZIG, BROUWER soutient le rôle essentiel de la négation ; en élargissant la notion de suite de choix il construit des théories qu’on ne peut pas formuler sans la négation (voir la fin de ce chapitre). Dans la conférence [34] BROUWER a exposé clairement ses idées fondamentales sur les relations des mathématiques avec l’expérience, avec le langage et avec la sagesse.**
(15)
BROUWER, L.E.J.
[34] Consciousness, Philosophy and Mathematics. Proc. 10th Congr. of Philosophy, Amsterdam 1948, p. 1235–1249.
(83)
Heyting, Arend. Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration. Paris / Louven: Gauthier-Villars / E. Nauwelaerts, 1955.
.
