Showing posts with label Brouwer. L.E.J. Brouwer. Show all posts
Showing posts with label Brouwer. L.E.J. Brouwer. Show all posts

6 Jun 2019

van Stigt & Mancosu (CBS) From Brouwer to Hilbert, collected brief summaries

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[Mathematics, Calculus, Geometry, Entry Directory]

[Logic and Semantics, entry directory]

[Walter P. van Stigt, entry directory]

[Paolo Mancosu, entry directory]

 

[The following collects brief summaries of select texts. The entry directories without the brief summaries are located here:

Mancosu and van Stigt, “Intuitionistic Logic,” entry directory

van Stigt, “Brouwer’s Intuitionist Programme,” entry directory

]

 

 

 

Collected Brief Summaries of

 

Walter P. van Stigt and Paolo Mancosu

 

From Brouwer to Hilbert:

The Debate on the Foundations of Mathematics in the 1920’s

 

Part I.

L.E.J. Brouwer

 

Ch1.:

“Brouwer’s Intuitionist Programme”

by Walter P. van Stigt

 

[1.0]

[Introductory material]

 

(1.0.1) Luitzen Egbertus Jan Brouwer (1881-1966) “main contributions are in the field of topology and the foundations of mathematics,” but “It is Brouwer’s contribution to the foundations of mathematics, the intuitionist programme, that has made him known to the wider scientific and philosophical community” (1). His influence is still great today. van Stigt will give an overview of Brouwer’s intuitionistic program.

 

1.1

The Intuitionist-Formalist Controversy

 

(1.1.1) Brouwer’s text “Foundations of Set Theory Independent of the Principle of Excluded Middle” diagnosed a crisis in the foundations of mathematics. This was noted by and had strong influence on Hermann Weyl. In his “Intuitionist Set Theory,” “Brouwer set out the consequences for established mathematics of his Intuitionist theses, in particular, his rejection of the logical Principle of the Excluded Middle: ‘the use of the Principle of the Excluded Middle is not permissible as part of a mathematical proof ... [it] has only scholastic and heuristic value, so that theorems which in their proof cannot avoid the use of this principle lack all mathematical content.’” (1.1.2) Hilbert saw Brouwer’s program as posing a threat to Cantorian set theory and to his own program, so he launched a counterattack in 1922. This begins the Intuitionist-Formalist debate of the 1920s. (1.1.3) The Intuitionist-Formalist debate revolved around two issues: {1} “The nature of mathematics: either human thought-construction or theory of formal structures” and {2} “The role of the Principle of the Excluded Middle in mathematics and Brouwer’s restrictive alternative logic” (2). (1.1.4) “Brouwer’s main concern was the nature of mathematics as pure, ‘languageless’ thought-construction” (2). His program aimed to convince the mathematical world of this view. His “Intuitionist Splitting of the Fundamental Notions of Mathematics” opened debate among logicians regarding an alternative “Brouwer Logic,” (including contributions by Kolmogorov, Borel, Wavre, Glivenko, and Heyting). But Brouwer was not concerned with logic, because he believed that “logic and formalization were ‘an unproductive, sterile exercise’ with no direct relevance to mathematics and its foundations” (2). (1.1.5) Hilbert’s program retains classical mathematics and bases “its validity on a proof of the consistency of its formalization” (3). Brouwer’s program had a constructive interpretation of mathematics. Both held some interest in the mathematical community, but Brouwer’s program failed to gain traction. (1.1.6) “The Brouwer-Hilbert debate grew increasingly bitter and turned into a personal feud” (3). Hilbert expels Brouwer from the board of the Mathematische Annalen. (1.1.7) Brouwer’s professional rejection led him to stop publicizing his program, even at the same time that Hilbert’s formalist program was shown to be fundamentally flawed.

 

1.2

“Intuitionism and Brouwer’s Intuitionist Philosophy of Mathematics”

 

[1.2.0]

[Introductory Material]

 

(1.2.0.1) Brouwer’s intuitionism is primarily a philosophy of mathematics. (1.2.0.2) “Most of Brouwer’s philosophical views on life in general and on the nature of mathematics were formed during the years of undergraduate and doctoral studies, and they remained virtually the same throughout his life” (4). (1.2.0.3) “This section is a brief introduction to Philosophical Intuitionism and the main aspects of Brouwer’s philosophy as are relevant to his Intuitionist practice” (4).

 

[1.2.1]

Intuitionism

 

(1.2.1.1) “Intuitionism is a philosophical trend that places the emphasis on the individual consciousness as the source and seat of all knowledge” (4). Intuitionism holds that the mind has not only a faculty and activity of reasoning but as well “a definite faculty and act of direct apprehension, intuition, as the necessary foundation of all knowledge, both in the grasping of first principles on which a system of deductive reasoning is built and as the critical link in every act of knowing between the knower and the object known” (4). Moreover, “Intuitionism stands in contrast to a more general rationalistic and deterministic trend that denies the possibility of knowing things and facts in themselves and restricts human knowledge to what can be deduced mechanically by analytical reasoning, ultimately from self-evident facts and principles that result from common sense or are based on the authority of collective wisdom” (4). (1.2.1.2) Elements of intuitionism can be found in previous philosophies. Aristotle’s νοῦς, for instance, is something like Brouwerian intuition; for, it is “a special faculty of direct apprehension, an active faculty that is indispensable in the creation of primary concepts and first principles as well as at every step of the thought process” (4). We can also find elements of intuitionism in “the systems of some of the modern German and English philosophers such as Kant, Hamilton, Whewell, and even Russell” (4). (1.2.1.3) Descartes can be considered the father of intuitionism, because for him, “every form of knowing ultimately requires an act of immediate mental apprehension, ‘intuition’” (5). (1.2.1.4) Descartes’ sort of intuitionism saw development in 19th century France by Maine de Biran, Ravaisson, Lachelier, and Boutroux. “It was developed into a full and comprehensive philosophy by Henri Bergson, who raised Intuition to the faculty of grasping the spiritual and changing reality, distinct from Reason, the analytical mind, which probes the material and static reality. Bergson’s living reality, however, did not include the mathematical universe; his concepts of number and the mathematical continuum are spatial, products of the analytical intellect” (5). (1.2.1.5) But the notion of intuition is vague in Descartes as well as with the French “New Intuitionists” Poincaré, Borel, and Lebesgue. It was not made mathematically precise until Brouwer “took Descartes’ intuitionist thesis to its radical subjective and constructive conclusion” (5).

 

[1.2.2]

Brouwer’s Outlook on Life and General Philosophy

 

(1.2.2.1) “Brouwer’s outlook on life and general philosophy can best be described as a blend of romantic pessimism and radical individualism” (5). Brouwer is critical of human industrialization and damage to nature and calls instead for a return to nature “and to mystic and solitary contemplation” (5). (1.2.2.2) In Foundations of Mathematics, Brouwer sees “the application of mathematics in experimental science and logic” as “the source of all evil,” because it superimposes “a mathematical regularity on the physical world” (5). In both Life, Art and Mysticism and Foundations of Mathematics, Brouwer expresses “his conviction of the opposition between mind and matter, the individual consciousness and the exterior world” (5). (1.2.2.3) Brouwer has a notion of personal identity, self, and subject as being a pure spiritual soul. “The life of the Soul is the complex of thought processes in response to its awareness of the world outside” (5). These processes are phases that deteriorate. (1.2.2.4) There is an original preperceptual phase of consciousness that is “stillness.” This is “followed by ‘the naive phase’ of receiving images through physical sensations and reacting spontaneously to them” (5). There is next a momentous event, called “the Primordial Happening” or “the Primordial Intuition of Time,” in which the subject links isolated sensations and becomes aware of time. This on the one hand “brings about a transformation of the Naive Consciousness to the rational ‘Mind’ ” while on the other hand it also “generates the fundamental concepts and tools of mathematics. The Primordial Intuition of Time is the fundamental single act of isolating and linking distinct moments in time, creating mathematical ‘Two-ity’ and the ordinal numbers as well as the continuum.” (6). This thereby gives us the “mathematical power to generate sequences,” which enables us to produce a human-made and mathematical interpretation of nature or the outside world. What we take to be “things,” “including other human beings, are no more than repeated sequences or sequences of sequences, manmade, as is indeed the so-called scientific or ‘causal’ coherence of the world” (6). Now, since these things are somehow fundamentally mathematical sequences that are thought up, “this universe of ‘things’ is wholly private,” and it is called “the Exterior World of the Subject” (6). “The scientific observation of regularity in Nature, linking things and events in time as sequences, is a creative, mathematical process of the individual Mind and is referred to as ‘mathematical viewing’ or ‘causal attention’,” and causality “is an artificial, mind-made structure, not inherent in Nature” (6). In fact, “Brouwer rejects any universal objectivity of things,” and he also rejects the idea that things are bound up by causality. Moreover, Brouwer “denies the existence of a collective or ‘plural’ mind” and instead favors “the essential individuality of thought and mind” (6). (1.2.2.5) The evolutionary movement of consciousness “enters a moral phase when man takes advantage of and acts upon his causal knowl­edge by setting in motion a causal sequence of events, selecting a first element of the sequence in order to achieve a later element, the desired ‘end’ ” (6). Given that there is an assessment of the causal sequence resulting from one’s actions, this is a “mathematical or causal acting” and it is “calculated” and “cunning”. As such, Brouwer condemns it “as ‘sinful’ and ‘not-beautiful’ ” on account of it being morally evil. (1.2.2.6) The next phase of conscious development, taking us even further away from consciousness’ “deepest home” is the “final phase of ‘social acting’ ” (6). Brouwer describes it as “ ‘the enforcement of will’ in social interaction and organization, in particular by the creation of language” (6). Brouwer thinks that we cannot communicate directly “soul-to-soul”. This creates the need for language, which Brouwer sees as the “ ‘imposition of will through sounds,’ forcing an­ other human being to act in pursuance of the end desired by the speaker” (6).  Then, “As social interaction develops and grows more complex, language becomes more sophisticated, but its essence, as of all instruments, is determined by its purpose: the transmission of will” (7). But, since it is “Used as a means of communicating thought to others, language is bound to remain defective, given the essential privacy of thought and the nature of the ‘sign,’  the arbitrary association of a thought with a sound or visual object” (7). (1.2.2.7) But language is not restricted to the imposition of one’s will upon others. It also is implemented strictly within one’s own inner world as an aid to memory, “helping the Subject to recall his past thought” (7). But Brouwer, when discussing the limitations of real life mathematicians and when noting that even with the help of linguistic signs, memory is still fallible, he “introduces his notion of the ‘Idealized Mathematician’ ” (7).

 

1.3

“The Nature of Pure Mathematics”

 

[1.3.0]

[Introductory material]

 

(1.3.0.1) We previously noted (see section 1.2.2.4 and 1.2.2.5) the mathematical nature of causality (for causality is a mental construction resulting from calculating outcomes) and the Primordial Intuition of Time (by which we ascertain Two-ity and thus numerical multiplicity). These are the “central theses of Brouwer’s analysis of science and language” (7). Early on Brouwer takes these two theses as being closely related, and his notion of mathematics is also at this time “somewhat tainted by its association with ‘causal’ or ‘cunning acting’ ” (7). Later Brouwer comes to give pure mathematics “an independent and redeeming role” (7). Part of this line of thinking is Brouwer’s notion of the “Liberation of the Mind,” which, in the mathematical context, “refers to the elimination of all exterior, phenomenal elements and causal influences from the creative mathematical act. It allows the Primordial Intuition as an abstraction of pure time awareness, eliminating also the content of sensations, to be a pure and a priori basis of mathematics and its defining act” (7). The Primordial Intuition of Time {1} is “necessary and sufficient for the creation of two-ity,” {2} it “holds the continuum as ‘its inseparable complement’,” and {3} “contains the fundamental elements and tools from which and with which the whole of mathematics is to be constructed” (7). In fact, “mathematics is identified with the whole of the constructive thought-process on and with the elements of the Primordial Intuition alone. Brouwer’s preferred term is ‘building’ (Dutch: bouwen) rather than ‘construction,’ a building upwards from the ground, a time-bound process, beginning at some moment in the past, existing in the present, and having an open future ahead” (7).

 

[1.3.1]

Mathematical Existence and Truth

 

(1.3.1.1) Mathematical existence means “having been constructed” and “remaining alive in the mind or memory” (8). Thus “The whole of the Subject’s constructive thought-activity, past and present, constitutes mathematical reality and mathematical truth: ‘Truth is only in reality, i.e. in the present and past experiences of consciousness’ ” (8). For Brouwer, we should identify mathematical entities “with the whole of their constructive pedigree, whether they be single concepts, such as, for example, an ordinal number, or more complex, such as a mathematical theorem, which combines various constructions” (8). (1.3.1.2) A (mathematical) construction consists of a sequence of constructive steps. Past, completed constructions would thus be finite sequences. But certain infinite values can have mathematical existence when an algorithm or law by which the number is uniquely determined can completely construct them. In such cases, the free power of the subject allows for the infinite values to be generated indefinitely. We see this sort of procedure for example in the intuition of the continuum, which is not for Brouwer a set of existing points but is rather “abstracted from the time interval, the mathematical ‘between’ that is never exhausted by division into subintervals” (8).

 

1.4

“Mathematics, Language, and Logic”

 

[1.4.0]

[Introductory material]

 

(1.4.0.1) The objective of Brouwer’s first intuitionist campaign was the freeing of “mathematics from its traditional reliance on language and logic” (8). (1.4.0.2) The subject when generating mathematics in their mind may make no use of any aspect of language. At best, the mathematician may record their constructions in symbols to aid their memory. However, this symbolization cannot be a part of the mathematical process itself. (1.4.0.3) In fact, symbolization cannot be relied upon for communicating mathematical constructions, because {a} we cannot be sure that other subjects, who are mere things in our created exterior world, have minds, and {b} even if other minds do exist, we cannot be sure that commonly shared words will “represent the same thought-construction in the private worlds of different individuals” (9). (1.4.0.4) Thus “Brouwer’s ‘mathematical language’ is the report, the record of a completed mathematical construction; its truth and noncontradictority are due solely to the constructions it represents” (9).

 

1.4.1

Logic

 

(1.4.1.1) Brouwer has a notion of “theoretical logic.” It is an application of mathematics in which one uses a “mathematical viewing” of a given mathematical record to see some regularity in that symbolic representation. (1.4.1.2) What we consider classical laws or principles of logic are regularities that we discern secondarily after genuine (intuitive) mathematical constructions are created. (1.4.1.3) But the operation of mathematics in the verbal or symbolic domain in fact is operating outside mathematical reality. And logic itself cannot generate new mathematical truths. In fact, we cannot even apply all the principles of logic to mathematics. Brouwer’s famous example is the invalidity of the Principle of the Excluded Middle (PEM) in mathematical applications. He identifies the Principle of the Excluded Middle with the principle of the solvability of every mathematical problem. Brower takes a strict interpretation of affirmation and negation: “True mathematical statements, affirmative and negative, express the completion of a constructive proof; in particular the negative statement expresses what Brouwer calls ‘absurdity,’ the constructed incompatibility of two mathematical constructions represented, respectively, by the subject and predicate of the sentence” (9-10). But for infinite systems there is no absolute guarantee that a complete constructed affirmative proof or completed absurd construction can be formulated for them. (Thus, it can be that for such an infinite system, neither an affirmative nor a negative construction can be given for it. Now, the Principle of the Excluded Middle says that for any formula, it is either affirmative or negative, or understood another way, it is either true or false. But infinite systems are neither affirmable nor negatable.) Hence, “the Logical Principle of the Excluded Middle is not a reliable principle” (10).

 

1.5

“Brouwer’s New Theory of Sets and the Continuum”

 

1.5.1

The Brouwer Negation

 

(1.5.1.1) When we are constructing fundamental mathematical entities, as for instance the natural numbers, “there is no place nor immediate need for negation” (14). We only require negation when needing to determine elementhood for entities in some species S. “Such attempt may lead to ‘successful fitting in’; that is, a particular mathematical entity is established as an element of S. The alternatives to ‘successful fitting in’ are: (1) the constructed impossibility or ‘absurdity’ of fitting in; and (2) the simple absence of the construction of elementhood or of its absurdity. Only negation in the first sense, of constructed impossibility, meets Brouwer’s strict requirements and can claim to be an act of mathematical construction” (14). (1.5.1.2) By interpreting negation as such, it “immediately calls into question the use of double negation and the logical principle of the excluded ‘third’ or middle” (14). (1.5.1.3) To define Brouwer negation, we need to determine what constitutes “absurdity” or “constructed impossibility” (15). Brouwer’s definitions for negation remain vague, and often important concepts they employ, like “impossibility,” “incompatibility,” “difference,” and “contradiction”, appear to be defined circularly. For instance, he defines “contradiction” or “the impossibility of fitting in” (see section 1.5.1.1 above) in the following way: “I just observe that the construction does not go further [Dutch: gaat niet, that is, it does not work], that in the main edifice there is no room to be found for the posited structure” (15). (In other words, perhaps: something is a contradiction if it does not fit in, and the criterion for determining this is that it does not fit in. So we still need a more precise account for not fitting in, which is what we in fact sought in the first place.) And “impossibility” is defined as an “incompatibility;” but “in­compatibility – latent and inherent in the structures concerned – is not sufficient by itself; he insists that negation is ‘a construction of incompatibility’ (B1954A, p. 3) or ‘the construction of the hitting upon the impossibility of the fitting in’ (B1908C, p. 3)” (15). (1.5.1.4) Post-Brouwer Intuitionism identifies the proof of the “absurdity of” or the incompatibility of two complex systems as a “reduction to a simple contradiction such as 1 = 0 or the logical p & ¬p” (15). But, even these sorts of contradictions and in fact all descriptions of “absurdity” “make use of some notion of negation or difference. Their absurdity can ultimately only be justified by some intuitive, primitive relation of distinctness, an element of the Primordial Intuition, the fundamental recognition of the Subject of distinct moments in time” (15). (So perhaps: negation is grounded in the intuition that one moment in time is not some other; but negation cannot be given a formal definition.) (1.5.1.5) There is a weaker form of negation which is not the proof of the absurdity of a formulation but rather is the fact that neither a proof affirming it nor a proof negating it has currently been found. It is recognized that in the future a proof could be found, so its negative status is not certain.

Brouwer also uses other, weaker forms of negation, in particular, where he moves outside the domain of mathematics proper into the realm of “mathematical language” and mathematical “assertions,” where, for example, he speaks of “un­proven hypotheses,” “the case that α has neither been proved to be true nor to be absurd.” Negation in this case expresses the simple absence of proof, which in the world of mathematics as construction in time may well be reversed: Unsolved problems may one day become proven truth or absurdity. Moreover, “a mathematical entity is not necessarily predeterminate, and may, in its state of free growth, at some time acquire a property it did not possess before” (BMS59, p. 1), leading to further distinctions, in particular, between “cannot now” and “cannot now and ever,” the latter term frequently used by Brouwer in his later work as an alternative description of “absurdity.”

(15, boldface and underlining are mine)

 

 

 

 

Part IV

Intuitionistic Logic

 

Part IV’s Introduction:

“Intuitionistic Logic”

by Paolo Mancosu & Walter P. van Stigt

 

4.0

[Introductory material]

 

(4.0.1) Quoting: “In this fourth part of the book we introduce several texts related to the emergence of intuitionistic logic. The introduction is divided into two sections. The first section, written by W. P. van Stigt, describes Brouwer’s contributions to what soon became called the “Brouwer logic.” The second section, written by P. Mancosu, analyzes several further contributions to the formalization of intuitionistic logic due to Glivenko, Heyting, and Kolmogorov” (275).

 

4.1

Brouwer

 

(4.1.1) Brouwer fought his “foundational battle” of intuitionistic mathematics initially on philosophical grounds: {1} he defends his claim that the true nature of mathematics is constructive thought construction against the “logicist-formalist confusion of mathematics with its symbolic representation;” {2} he takes the “first act of Intuitionism” to be “ ‘the separation of mathematics and language,’ exposing the true nature of logic as no more than a science, a mathematical analysis of the symbolic record of a mathematical thought­-construction” (275) (see section 1.4.1.2); {3} he particularly “condemned the traditional practice of using logical principles – distilled from past mathematical records – as operators on words and sentences to generate new mathematical truths. The Principle of the Excluded Middle was singled out as obviously flawed when applied to the mathematics of the infinite, its use in his reconstruction of mathematics expressly avoided” (275) (See section 1.4.1.3). (4.1.2) But with his text “Intuitionist Splitting of the Fundamental Notions of Mathematics,” Brouwer “now embarks on an investigation in the field of logic proper” (275). Brouwer even came to soften his critique of the use of language in mathematics. He was part of the “Signific movement,” which called for “new words expressing spiritual values for the languages of western nations,” and which “was particularly relevant to Brouwer’s programme of reconstructing mathematics; new words were needed to represent his new notions and distinctions – and communicate his message to the mathematical world” (276). (4.1.3) In his “Intuitionist Splitting of the Fundamental Notions of Mathematics,” Brouwer fashions new words for some of his intuitionistic ideas (see section 4.1.2). He begins with mathematical truth and with absurdity, which is proven impossibility. From this we learn that the Principle of Excluded Middle and Double Negation (here called “The Principle of Reciprocity of Complementary Species”) are not applicable in intuitionistic mathematics. (While Brouwer will keep this rejection of double negation, he holds something similar, namely that) “Truth implies absurdity-of-absurdity, but absurdity-of-absurdity does not imply truth” (276). (It seems that this means, from an affirmed formula you can derive its doubled negation, but from a double negation you cannot derive its unnegated form. Maybe the idea is the following. Negation of negation is somehow like lacking a constructed proof, but that does not prove the affirmative form. For, it could still be shown to simply be absurd later. But, suppose you have constructed a valid proof of something. Nothing in the future could ever then show it to be absurd. So from a proven formula you can derive its double negation or the absurdity of it being absurd.) But, a triple negation, “Absurdity-of-absurdity-of-absurdity is equivalent with absurdity” (276). Brouwer does not want to use the symbolic notation for negation, because he does not want to portray logical operators as mathematical (and thus as intuitive). But we can eliminate enchained absurdities (reduce negations) in the expected way:  “a finite sequence of absurdity predicates can be reduced to either absurdity or absurdity-of-absurdity ... by striking out pairs of absurdity predicates, provided that the last absurdity predicate of the sequence is never included in the cancellation” (276). (4.1.4) Thus in his paper “Intuitionist Splitting of the Fundamental Notions of Mathematics,” Brouwer for the first time makes explicit his rejection of double negation. (4.1.5) Rolin Wavre calls this “Brouwerian Logic” (Logique Brouwerienne), and many others joined the debate about or made contributions to intuitionist logic, including Kolmogorov, Lévy, Avstidisky, Barzin & Errera, Borel, Khinchin, Glivenko, and Heyting. (4.1.6) But Brouwer did not get too much involved in the debate over intuitionistic logic on account of his still negative view of formal logic (see section 1.4.1.2 and section 1.4.1.3). Heyting then takes over the cause of intuitionistic logic.

 

4.2

The Emergence of the Intuitionistic Propositional Calculus

 

(4.2.1) Brouwer says that the intuitionist mathematician rejects excluded middle and double negation but accepts A → ¬¬A (so if something is proven, it cannot be disproven), (A B) → (¬B → ¬A), and ¬A is equivalent to ¬¬¬A, meaning that “one can always strike out an even number of negations from a formula provided the last negation is not cancelled” (277). (4.2.2) After Brower’s reflections on intuitionistic logic in 1923, the next to have reflected on it was Wavre in 1926. He calls classical logic “formal logic” and intuitionistic logic “empiricist” logic. He says that in an empiricist context, to assert a statement A means to assert the provability of A. And the negation of A would be stating that the assertion of A leads to a contradiction. The following are other empiricist principles:

1. (A B) & (B C) → (A C);

2. From A and (A B) one can infer B;

3. ¬(A & ¬A);

4. (A → ⊥) → ¬A.

And as with intuitionism, empiricist logic does not have excluded middle or double negation. Also valid are A → ¬¬A and the equivalence of ¬A and ¬¬¬A. Only some forms of reductio ad absurdum hold in empiricist logic. (4.2.3) Although Wavre’s article does not go beyond Brouwer’s remarks on Intuitionistic logic, it did start a debate on intuitionistic mathematics in the Revue de Metaphysique et de Morale. (4.2.4) In his 1927 book Mathematische Existenz, O. Becker gives a phenomenological interpretation of intuitionistic logic based on Husserl’s theory of judgments in his Logic Investigations. We consider that “p holds,” written as “+p”. Becker says that there are two ways this can be denied: {1} we can say p’s negation holds, “¬p holds”, written as “+(–p),” or {2} we can say p fails to hold, “p does not hold”, written as and “– (+p)”. “He also claimed that the three cases excluded any other possibility so that either +p or +(–p) or –(+p), quartum non datur.” These correspond to the ways an intention can be fulfilled. Suppose that we have the proposition p: “the book is on the table”. {1} Fulfillment [Erfüllung], +p, would be that we perceive the table and see that the book is in fact on it; {2} frustration [Enttäuschung], +(–p), would be that we see the table and the book is not on it. In this case, there would be a conflict [Widerstreit]; and {3} nonfulfillment, –(+p), would be that we see neither the table nor the book. In this case, there is no conflict. (4.2.5) Becker defines truth and falsity in intuitionistic logic in the following way: “intuitionistic logic does not distinguish between ‘true’ and ‘false’ but between ‘true’ and ‘absurd.’ In this context ‘true’ means: actually provable (constructively), and absurd: ‘provably contradictory’ (from the phenomenological point of view one can in principle say: true = there is the synthesis of the fulfillment of the judgment intention, the agreement between what is intended and what is perceived; ‘absurd’: = there is the ‘synthesis’ of the frustration of the judgment intention, the ‘synthesis’ of the conflict.... Clearly there is no complete disjunction, in the sense of the tertium non datur, between fulfillment and frustration, agreement and conflict. (Becker 1927, p. 775)” (278). (Now take the book and table example again. Suppose we do not see that the book is on the table, that is, –(+p). Now suppose instead that we do not see that the book is not on the table, or –(–p). What, phenomenologically speaking, is the difference? There is no difference between the experiences of failing to see that the book is on the table compared with failing to see that the book is not on the table. Becker found this problematic, because the quartum non datur is +p or +(–p) or –(+p) and Wavre says that in intuitionistic logic we cannot have (p ∨ ¬p ∨ ¬¬p), but here Becker thinks that we should have the equivalent of ¬¬p as –(–p).) His solution for this was not satisfactory. (4.2.6) “Becker managed to ground all the principles in Wavre’s list according to his phenomenological interpretation. At the end of the appendix he also stated the problem of finding a calculus for intuitionistic logic” (279). (4.2.7) Regarding the formulation of a calculus for intuitionistic logic, early on there were detractors. In 1927, Barzin and Errera argued that intuitionistic logic has a third value, “tierce,” written as “p′” and that on account of it and the semantics of intuitionism, the system leads to formal contradictions regarding the truth values. But their proofs involve using principles that are classically valid but not intuitionistically valid, so their attempt fails. (4.2.8) In 1928, Church, in his “On the Law of the Excluded Middle”, reviews Barzin & Errera’s criticisms and makes the following three claims: {1} Dropping the law of excluded middle alone will not result in contradictions. {2} Barzin & Errera’s criticisms use reductio ad absurdum argumentation. But reductio arguments use the law of excluded middle, so these criticisms will not work for intuitionists who reject that law. And {3} Church incorrectly says that the “tierce” value being neither true nor false breaks the law of contradiction along with the law of excluded middle. (4.2.9) Church did not see any reason for accepting the quartum non datur. (4.2.10) Glivenko in a 1928 paper shows that Brouwerian intuitionistic logic is not a three-valued logic, so the use of “tierce” propositions are invalid. (4.2.11) Glivenko in a 1929 paper provides “the first seeds of a development that will yield a long series of interpretations of classical logic into intuitionistic logic known as double negation interpretations or negative translations” (280-281). (4.2.12) Around the same time, Heyting was formalizing the principles of intuitionistic logic. (4.2.13) In a letter to Becker from 1933, Heyting explains some of his insights into intuitionistic logic and how he came upon them. (4.2.14) In other papers Heyting gives the interpretations for logical connectives in intuitionistic logic. There we also see elements of Becker’s phenomenological interpretation. (4.2.15) Heyting also says that we cannot simply identify “ ‘p is true’ (in the intuitionistic sense) with ‘p is provable’,” because we need “the observation of an empirical fact, that is, of the realization of the expectation expressed by the proposition p. Here, then, is the Brouwerian assertion of p: It is known how to prove p. (1930a, p. 307)” (282). (4.2.16) For Heyting and Kolmogorov, a proposition p can be interpreted either as an expectation or a problem. (4.2.17) Kolmogorov in 1932 explains the problem interpretation: “If a and b are two problems, then a & b designates the problem ‘to solve both problems a and b,’ while a b designates the problem ‘to solve at least one of the problems a and b.’ Furthermore, a b is the problem ‘to solve b provided that the solution for a is given’ or, equivalently, ‘to reduce the solution of b to the solution of a’ [ ... ] ¬a designates the problem ‘to obtain a contradiction provided that the solution of a is given.’ (1932, p. 329)” (282). (4.2.18) We have thus seen three major events in the history of intuitionistic logic: “Heyting had provided a complete formalization of intuitionistic logic, Glivenko had pointed the way to the negative interpretations to follow, and the combined work of Heyting and Kolmogorov had given an explicit formulation to what is now known as the BHK interpretation of intuitionistic logic” (283).

 

 

 

 

 

 

 

Stigt, Walter P. van. (1989). “Brouwer’s Intuitionist Programme” In: From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920’s, edited by Paolo Mancosu. Oxford: Oxford University.

 

Mancosu, Poalo & Stigt, Walter P. van. (1989). “Intuitionistic Logic” In: From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920’s, edited by Paolo Mancosu. Oxford: Oxford University.

 

 

 

.

5 Jun 2019

Heyting (2.2.2.1,2,9,10) Intuitionism: An Introduction. Selections from section 2.2.2, “[on inequality and negation]”, summary

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[Mathematics, Calculus, Geometry, Entry Directory]

[Logic and Semantics, entry directory]

[Heyting, entry directory]

[Heyting’s Intuitionism: An Introduction, 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. Bracketed comments and subsection divisions are my own. Proofreading is incomplete, so please forgive my mistakes.]

 

 

 

 

Summary of

 

Arend Heyting

 

Intuitionism: An Introduction

 

2.

Arithmetic

 

2.2

“Real Number Generators”

 

2.2.2

Inequality Relation Between Number-Generators

 

2.2.2.1,2,9,10

[Selections on inequality and negation]

 

 

 

 

Brief summary:

(2.2.2.1) “If a = b is contradictory (that means : if the supposition that a = b leads to a contradiction), we write a b.” (2.2.2.2) The first theorem says: “If a b is contradictory, then a = b.” (2.2.2.3-8: skip) (2.2.2.9) In intuitionistic mathematics, “not” always has a strict meaning: “The proposition p is not true” or “the proposition p is false” means “If we suppose the truth of p, we are led to a contradiction” (this is de jure falsity, because it has been proven necessarily the case and will stay that way). Yet we can use “not” in another way, namely, to mean there is not yet a proof for something (this is de facto falsity, because it happens to be the case that a proof is lacking, but one may someday be formulated):

‘if we say that the number-generator ρ which I defined a few moments ago is not rational, this is not meant as a mathematical assertion, but as a statement about a matter of facts; I mean by it that as yet no proof for the rationality of ρ has been given. As it is not always easy to see whether a sentence is meant as a mathematical assertion or as a statement about the present state of our knowledge, it is necessary to be careful about the formulation of such sentences. Where there is some danger of ambiguity, we express the mathematical negation by such expressions as “it is impossible that”, “it is false that”, “it cannot be”, etc., while the factual negation is expressed by “we have no right to assert that”, “nobody knows that”, etc.’

(18)

(2.2.2.10) In intuitionistic mathematics, all mathematical assertions are in the form of constructions. Even a negation of an assertion would have to be an alternate positive construction on the basis of which we effect a reductio of that negated assertion:

‘There is a criterion by which we are able to recognize mathe- | matical assertions as such. Every mathematical assertion can be expressed in the form: “I have effected the construction A in my mind”. The mathematical negation of this assertion can be expressed as “I have effected in my mind a construction B, which deduces a contradiction from the supposition that the construction A were brought to an end”, which is again of the same form.’

(18-19)

However, when we simply lack a proof for something (without also being able to construct a disproof of it), then we have just a factual negation (and a disproof may or may not be devised some day).

‘On the contrary, the factual negation of the first assertion is: “I have not effected the construction A in my mind”; this statement has not the form of a mathematical assertion.’

(19)

 

 

 

 

 

 

 

Contents

 

2.2.2.1

[The Contradiction of Equality as Inequality]

 

2.2.2.2

[The Contradiction of Inequality as Equality]

 

2.2.2.9

[Negation as Disproof and Negation as Lack of Proof]

 

2.2.2.10

[The Difference Between Constructing a Disproof for a Mathematical Assertion and Simply Not Having Constructed a Proof for It]

 

Bibliography

 

 

 

 

 

 

Summary

 

2.2.2.1

[The Contradiction of Equality as Inequality]

 

[“If a = b is contradictory (that means : if the supposition that a = b leads to a contradiction), we write a b.”]

 

[ditto]

If a = b is contradictory (that means : if the supposition that a = b leads to a contradiction), we write a b.

(17)

[contents]

 

 

 

 

 

 

2.2.2.2

[The Contradiction of Inequality as Equality]

 

[The first theorem says: “If a b is contradictory, then a = b.”]

 

[ditto]

Theorem 1.   If a b is contradictory, then a = b [L. E. J. Brouwer 1925, p . 254].

(17)

BROUWER, L. E. J.

1925. Intuitionistische Zerlegung mathematischer Grundbegriffe. Jahresbericht deutsch. Math. Ver. 33, p. 251–256.

 

[contents]

 

 

 

[2.2.2.3-8: skip]

 

 

 

 

 

 

2.2.2.9

[Negation as Disproof and Negation as Lack of Proof]

 

[In intuitionistic mathematics, “not” always has a strict meaning: “The proposition p is not true” or “the proposition p is false” means “If we suppose the truth of p, we are led to a contradiction” (this is de jure falsity, because it has been proven necessarily the case and will stay that way). Yet we can use “not” in another way, namely, to mean there is not yet a proof for something (this is de facto falsity, because it happens to be the case that a proof is lacking, but one may someday be formulated):

‘if we say that the number-generator ρ which I defined a few moments ago is not rational, this is not meant as a mathematical assertion, but as a statement about a matter of facts; I mean by it that as yet no proof for the rationality of ρ has been given. As it is not always easy to see whether a sentence is meant as a mathematical assertion or as a statement about the present state of our knowledge, it is necessary to be careful about the formulation of such sentences. Where there is some danger of ambiguity, we express the mathematical negation by such expressions as “it is impossible that”, “it is false that”, “it cannot be”, etc., while the factual negation is expressed by “we have no right to assert that”, “nobody knows that”, etc.’

(18)]

 

[ditto]

Strictly speaking, we must well distinguish the use of “not” in mathematics from that in explanations which are not mathematical, but are expressed in ordinary language. In mathematical assertions no ambiguity can arise: “not” has always the strict meaning. “The proposition p is not true”, or “the proposition p is false” means “If we suppose the truth of p, we are led to a contradiction”. But if we say that the number-generator ρ which I defined a few moments ago is not rational, this is not meant as a mathematical assertion, but as a statement about a matter of facts; I mean by it that as yet no proof for the rationality of ρ has been given. As it is not always easy to see whether a sentence is meant as a mathematical assertion or as a statement about the present state of our knowledge, it is necessary to be careful about the formulation of such sentences. Where there is some danger of ambiguity, we express the mathematical negation by such expressions as “it is impossible that”, “it is false that”, “it cannot be”, etc., while the factual negation is expressed by “we have no right to assert that”, “nobody knows that”, etc.

(18)

[contents]

 

 

 

 

 

 

2.2.2.10

[The Difference Between Constructing a Disproof for a Mathematical Assertion and Simply Not Having Constructed a Proof for It]

 

[In intuitionistic mathematics, all mathematical assertions are in the form of constructions. Even a negation of an assertion would have to be an alternate positive construction on the basis of which we effect a reductio of that negated assertion:

‘There is a criterion by which we are able to recognize mathe- | matical assertions as such. Every mathematical assertion can be expressed in the form: “I have effected the construction A in my mind”. The mathematical negation of this assertion can be expressed as “I have effected in my mind a construction B, which deduces a contradiction from the supposition that the construction A were brought to an end”, which is again of the same form.’

(18-19)

However, when we simply lack a proof for something (without also being able to construct a disproof of it), then we have just a factual negation (and a disproof may or may not be devised some day).

‘On the contrary, the factual negation of the first assertion is: “I have not effected the construction A in my mind”; this statement has not the form of a mathematical assertion.’

(19)]

 

[ditto]

There is a criterion by which we are able to recognize mathe- | matical assertions as such. Every mathematical assertion can be expressed in the form: “I have effected the construction A in my mind”. The mathematical negation of this assertion can be expressed as “I have effected in my mind a construction B, which deduces a contradiction from the supposition that the construction A were brought to an end”, which is again of the same form. On the contrary, the factual negation of the first assertion is: “I have not effected the construction A in my mind”; this statement has not the form of a mathematical assertion.

(18-19)

[contents]

 

 

 

 

 

 

 

 

 

 

 

 

 

Bibliography:

 

Heyting, Arend. Intuitionism. An Introduction. Amsterdam: North-Holland, 1956.

 

.

2 Jun 2019

Heyting (5.3.1) Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration. Section 5.3.1, “Calcul numérique”, summary

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[Mathematics, Calculus, Geometry, Entry Directory]

[Logic and Semantics, entry directory]

[Heyting, 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.3

Continu. Suite de choix

 

5.3.1

Calcul numérique

 

 

 

 

 

Brief summary:

(5.3.1.1) Coordinated choice sequences can be used to define the operations of calculation. But problems arise when inequalities are used. For Brouwer, a is different from b, (a ≠ b), means that a = b is impossible. But when we are dealing with the continuum, we have an additional relationship of inequality and equality that can hold between variables. Roughly: For the continuum, we additionally have the relationship a is positively different from b or “a is apart from [écarté deb” (a b). This is fulfilled when, in the series of intervals that define a and b, two external intervals are known [to be shared by both]. a b of course results from a ⧣ b ; but the inverse cannot be affirmed. Moreover, as we can easily see, the negation of ab, and also of a b, is equivalent to a = b.

 

 

 

 

 

Contents

 

5.3.1.1

[Inequality and Continua]

 

Bibliography

 

 

 

 

 

 

Summary

 

5.3.1.1

[Inequality and Continua]

 

[Coordinated choice sequences can be used to define the operations of calculation. But problems arise when inequalities are used. For Brouwer, a is different from b, (a ≠ b), means that a = b is impossible. But when we are dealing with the continuum, we have an additional relationship of inequality and equality that can hold between variables. Roughly: For the continuum, we additionally have the relationship a is positively different from b or “a is apart from [écarté deb” (a b). This is fulfilled when, in the series of intervals that define a and b, two external intervals are known [to be shared by both]. a b of course results from a ⧣ b ; but the inverse cannot be affirmed. Moreover, as we can easily see, the negation of ab, and also of a b, is equivalent to a = b.]

 

[In rough form: Numerical calculation.– The use of choice sequences in mathematics is based on the possibility of establishing coordination between choice sequences. The sequence β can be coordinated with the sequence α by the fact that each choice of β can be defined by using a finite initial segment of α. The definitions of the operations of calculation constitute simple examples of such a coordination. Once these have been given, we then easily have the results of a pure calculation of elementary arithmetic and algebra; however, complications can appear as soon as inequalities are used. a is different from b, (a b), means, in BROUWER’s terminology, that a = b is impossible. For the continuum, we additionally have the relationship a is positively different from b or “a is apart from [écarté deb” (a b). This is fulfilled when, in the series of intervals that define a and b, two external intervals are known [to be shared by both]. a b of course results from a ⧣ b ; but the inverse cannot be affirmed. Moreover, as we can easily see, the negation of ab, and also of a b, is equivalent to a = b. BROUWER has shown using examples [26] that there are real numbers for which we do not know if a = 0 or  if a ≠ 0. We will write a b when we know in the series of intervals for a an interval that is external and to the right of an interval of the sequence for.b. From a b it follows either a b, or b a.]

]

Calcul numérique.– L’utilisation des suites de choix en mathématiques est fondée sur la possibilité d’établir des coordinations entre des suites de choix. La suite β peut être coordonnée à la suite α par le fait que chaque choix de β peut être défini au moyen d’un segment initial fini de α. Les définitions des opérations du calcul constituent des exemples simples de telles coordinations. Une fois celles-ci données, on a alors sans difficulté les résultats de pur calcul de l’arithmétique élémentaire et de l’algèbre ; pourtant des complications peuvent apparaître dès qu’on fait emploi d’inégalités. a est différent de b, (a b), signifie, dans la terminologie de BROUWER, que a = b est impossible. Pour le continu, on a en outre la relation a est positivement différent de b ou a est | écarté de b (ab). Celle-ci est remplie quand, dans les suites d’intervalles qui définissent a et b, on connaît deux intervalles extérieurs l’un à l’autre. a b résulte évidemment de ab ; mais l’inverse ne peut pas être affirmé. De plus, on le voit facilement, la négation de a b, et aussi celle de ab, est équivalente à a = b. BROUWER a montré par des exemples [26] qu’il y a des nombres réels pour lesquels on ne sait pas si a = 0 ou a ≠ 0. On écrira ab quand on connaît dans la suite d’intervalles pour a un intervalle qui est extérieur et à droite d’un intervalle de la suite pour.b. De ab il suit soit ab, soit ba.

(24-25)

[26] : Mathematik, Wissenschaft und Sprache. Mh, Math, Phys. 36 (1929), p.153–164 ;

(79) (boldface is mine)

[contents]

 

 

 

 

 

 

 

 

Bibliography:

 

Heyting, Arend. Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration. Paris / Louven: Gauthier-Villars / E. Nauwelaerts, 1955.

 

.

31 May 2019

Heyting (5.1.1) Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration. Section 5.1.1, “Mathématique sans négation de Griss”, summary

 

by Corry Shores

 

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[Mathematics, Calculus, Geometry, Entry Directory]

[Logic and Semantics, entry directory]

[Heyting, 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 ab (see “numerical calculation” below). The theorem “if ab 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.

 

 

 

 

Contents

 

5.1.1.1

[Griss’ Negationless Mathematics; His Elimination of Negational Structures, in Particular His Use of Distance (⧣) in Place of Inequality (≠)]

 

5.1.1.2

[Griss’ and Destouches-Février’s Negationless Intuitionistic Logic]

 

5.1.1.3

[Destouches-Février devises a logic of constructions, on the basis of which she defines a logic of problems and a propositional logic.]

 

5.1.1.4

[Van Dantzig’s Affirmative Mathematics]

 

5.1.1.5

[Brouwer and Negation]

 

Bibliography

 

 

 

 

 

 

Summary

 

5.1.1.1

[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 ab (see “numerical calculation” below). The theorem “if ab 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 ab (see “numerical calculation” below). The theorem “if ab 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 ab (see “numerical calculation” below). The theorem “if ab 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 ab (voir ci-dessous “calcul numérique”). Le théorème “si ab 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)

[contents]

 

 

 

 

 

 

5.1.1.2

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

[contents]

 

 

 

 

 

 

5.1.1.3

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

[contents]

 

 

 

 

 

 

5.1.1.4

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

[contents]

 

 

 

 

 

 

5.1.1.5

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

[contents]

 

 

 

 

 

 

 

Bibliography:

 

Heyting, Arend. Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration. Paris / Louven: Gauthier-Villars / E. Nauwelaerts, 1955.

 

.