|This is the talk page for discussing improvements to the Intuitionism article.|
|WikiProject Mathematics||(Rated Start-class, Mid-importance)|
|WikiProject Philosophy||(Rated Start-class, Mid-importance)|
New article 
This new article by Alexey Dejneka is much better than the nonsense that was here before. Perhaps it would be good to add some examples of intuitionistic theorems, to show how different they are from classical theorems. Unfortunately, I don't know enough about intuitionism to do this myself. I remember reading somewhere that Brouwer proved that every real-valued function defined on the whole of [0,1] is uniformly continuous. If this is correct, it would make a nice example. --Zundark, 2001 Sep 22
Article title 
I moved this to just Intuitionism on the grounds that we don't need parenthetical disambiguation if this is only intuitionism in the 'Pedia. If there is more intutionism, then move this back to Intuitionism (philosophy of mathematics) and make a disambiguation page. -- Toby 02:26 Feb 20, 2003 (UTC)
Yes, there is more to intuitionism that just mathematical, logical, and ethical intuitionism. Philosophers may use "intuition" to denote any immediate apprehension of an object (without mediation by conceptual knowledge), irrespective of its application in any specific field of study. The article on intuition already makes brief mention of this. Kant, for example, used the term in this way when he spoke of space and time as the pure forms of intuition. Philosophers from Plato to the phenomenologists can be understood as intuitionists. Intuitionism, broadly construed, can thus be any theory of knowledge which recognizes intuition as a particularly important way of knowing. But this needs more thought and more careful research before it can be incorporated into this article. I have put it on my list of things to try to do. -- WikiPedant 18:57, 28 November 2005 (UTC)
Lambiam's exposition 
[this originally appeared on the law of excluded middle talk-page.wvbaileyWvbailey 18:22, 27 June 2006 (UTC)]
- What counts as an acceptable proof method to intuitionists will necessarily always remain a bit vague, as these issues precede any attempts at formalization. In fact, not all intuitionists agreed or agree on all aspects; see for example the article on Ultrafinitism. Most would agree, though, that intuitionistic logic faithfully internalizes the propositional aspect of intuitionistically acceptable mathematical reasoning, and so will accept a valid theorem in that logic as being also a valid theorem schema in mathematics itself. In many ways intuitionistic type theory has gone further, extending the scope of the formal-logical approach. In general, the methods of constructive mathematics are also acceptable to intuitionists, and some people even identify intuitionism with constructivism in mathematics.
- Intuitionists accept P V ~P for any specific proposition P whose truth or falsehood has been demonstrated. Furthermore, they accept this for classes of propositions for which an effective method is known for testing whether they hold. For example, consider the class in which P takes the form X = Y in which X and Y are arithmetic formulas involving only numerals and the familiar arithmetic operations. To test the validity of such a P, just evaluate the two sides of the equation and check whether they are the same. If such a test is not (known to be) available, usually the problem involves, so to speak, to test an infinity of cases, and no known reasoning allowing us to reduce this infinity to a finite number of effectively testable cases. A well-known example is Goldbach's conjecture. For many classes of formally infinite problems an effective (and therefore finite) test procedure is known, however, and then intuitionists will gladly assert P V ~P for these classes. What counts as effective to intuitionists, and which effective procedures count as true tests, will necessarily always remain a bit vague; see above.
- Intuitionists can look at PM derivations in two ways. One is that the logician is playing a game with self-invented rules, like peg solitaire but more complicated, and then they can look at the process and verify that the logician is not cheating. Just as for peg solitaire, this has nothing to do with notions of truth. They can also look at this game, bearing in mind that the logician claims the symbols mean something and allow the game player to express truths. Then there are many potential problems, some having to do with what counts as an acceptable definition (for example of notions like function and real number), some with the range of quantifications, some with the validity of inference rules, and some with the axioms. What these objections have in common is that intuitionists believe that the use of unreliable definitional approaches, unreliable inference rules and unreliable axioms does not offer a reliable way for examining the truth of mathematical claims. Clearly, derivations assuming LoEM or using double negative elimination are not considered kosher. Intuitionists will consider a PM derivation of a → a from a V ~a as a good example of how you can occasionally and accidentally reach correct conclusions using unreliable methods.
- The "cure" intuitionists would prescribe to the mathematical ailment of unreliability is: Use only methods whose reliability has been established. What is reliable and what not, is open to discussion, as is the question what constitutes sufficient evidence or justification. But if, in order to justify a principle, you need to resort to a circular argument, you have failed to establish reliability. Also, the argument that something has a respectable pedigree harking back to Aristotle, is believed to be sound by more than five million mathematicians, and has not failed thus far in any case where it was applied, is unacceptable.
- I'm not sure how much detail of this (assuming proper citations) should be presented in the article Law of excluded middle. If it should be presented at all, then the article Intuitionism may be a better place. --LambiamTalk 18:16, 12 June 2006 (UTC)
Background w.r.t. Intuitionism 
(originally copied from Law of Excluded Middle, but deviates substantially. wvbaileyWvbailey 18:22, 27 June 2006 (UTC))
"analysis." Encyclopædia Britannica. 2006. Encyclopædia Britannica 2006 Ultimate Reference Suite DVD 15 June 2006, "Constructive analysis" (Ian Stewart, author)
Goldstein, Rebecca, Incompleteness: The Proof and Paradox of Kurt Godel, Atlas Books, W.W. Norton, New York, 2005.
Rosenbloom. Paul C., The Elements of Mathematical Logic, Dover Publications Inc, Mineola, New York, 1950.
Anglin, W. S., Mathematics: A Concise history and Philosophy, Springer-Verlag, New York, 1994.
Davis, Martin, Engines of Logic, Norton, 2001. Reviewed by Richard S. Wallace
Kleene, Stephen Cole, Introduction to Metamathematics, North-Hoalland Publishing Company, Amsterdam, Elsevier Science Publishing Company, NY, 1st published 1952, 10th edition 1991.
Kleene (1952): Introduction to Metamathematics 
Quoted from §13 Intuitionism, pp.46ff
Kronecker and Poincare as roots of Brouwer's philosophy
- " In the late 1880's, when the methods of Weierstrass, Dedekind and Cantor were flourishing, Kronecker argued vigorously that their fundamental definitions were only words, since they do not enable one in general to decide whether a given object satisfies the definition.
- " Poincare, when he defends mathematical induction as an irreducible tool of intuitive mathematical reasoning (1902, 1905-06), is also a forerunner of the modern intuitionistic school.
- " In 1908 Brouwer, in a paper entitled "The untrustworthiness of the principles of logic", challenged the belief that the rules of the classical logic, which have come down to us essentially from Aristotle (384-322 B.C.), have an absolute validity, independent of the subject matter to which they are applied. Quoting from Weyl 1946, "According to his view and reading of history, classical logic was abstracted from the mathematics of finite sets and their subsets....Forgetful of this limited origin, one afterwards mistook that logic for something above and prior to all mathematics, and finally applied it, without justification, to the mathematics of infinite sets...."[here Kleene gives two examples from finite set theory that do not carry over to infinite sets] (Kleene p. 46)
The infinite, the antinomies:
- " The non-intuitionistic mathematics which culminated in the theories of Weierstrass, Dedkind and Canotr, and the intuitionistic mathematics of Brouwer, differ essentially in their view of the infinite. In the former, the infinite is treated as actual or completed or extended or existential. An infinite set is regarded as existing as a completed totality, prior to or independently of any human process of genration or construction ... in the later [intuitionism], the infinite is treated only as potential or becoming or constructive. the recognition of this distinction, in the case of infinite magnitudes, goes back to Gauss, who in 1831 wrote, 'I protest ... against the use of an infinite magnitude as something completed, which is never permissible in mathematics.'(Werke VIII p. 216)."(p. 48)
- " According to Weyl 1946, 'Brouwer made it clear, as I think beyond any doubt, tht there is no evidence supporting the belief in the existential character of the totality of all natural numbers ... the sequence of numbers which grows beyond any stage already reached by passing to the next number, is a manifold of possibilities open towards infinity; it remains forevere in the status of creation, but is not a closed realm of things existing in themselves. That we blindly converted one into the othere is the true source of our difficulties, including the antinomies -- a source of more fundamental nature than Russell's vicious circle principle indicated. Brouwer opened our eyes and mde us see how far classical mathematics, nourished by a belief in the 'absolute' that transccends all human possibilities of realization, goes beyond such statements as can claim real meaning and truth founded on evidence."(p. 48-49)
- " mathematical induction is an example of an intuitionistic method for proving generality propostions about the natural numbers. A proof by induction of the proposition for all n, P(n) shows that any given n would have to have the property P, by reasoning which uses only the numbers from 0 up to n....(p. 49)
constructive versus non-constructive proof (all italics and wording are as in the original)
- " An existence statement there exists a natural number n having the property P, or briefly there exists an n such that P(n), has its intuitionistic meaning as a partial communication (or abstract) of a statement giving a particular example of a natural number n which has the property P, or at least giving a method by which in principle one could find such an example.
- " Therefore an intuitionistic proof of the propostion there exists an n such that P(n) must be constructive in the following (strict) sense. The proof actually exhibits an example fo an n such that P(n), or at least indicates a method by wihch one could in principle find such an example.
- " In classical mathematics there occur non-constructive or indirect existence proofs, which the intuitionits do not accept. For example, to prove there exits an n such that P(n), the classical mathematician may deduce a contradiction from the assumption for all n, not P(n). Under both the classical and intuitionistic logic, by reductio ad absurdum this gives not for all n, not P(n). The classical logic allows this result to be transformed into there exists an n such that P(n), but not (in general) the intuitionistic...The classical meaning, that somewhere in the completed infinite totality of the natural numbers there occurs an n such that P(n) is not available to him, since he does not conceive the natural numbers as a completed totality.
- " As another example of a non-constructive existence proof, suppose it has been shown for a certain P, by intuitionistic methods, that if Fermat's 'last theorem' is true, then the number 5013 has the property P, and also that if Fermat's 'last theorem' is false, then 10 has the property P. Classically this suffices to demonstrate the existence of a number n such that P(n). But with the problem of the 'last theorem' unsolved, Brouwer would disallow such an existence proof, because no example has been given. ... [this goes on for a bit more into law of excluded middle]...
- " As appears in this example, intuitionistic methods are to be distinguished from non-intuitionistic ones in the case of defintions as well as in the case of proofs. In the present state of our knowledge, Brouwer does not accept the number n which is equal to 5013 if F, and equal to 10 if not F as a valid definition of a natural number" p. 49-51
wvbaileyWvbailey 18:19, 27 June 2006 (UTC)
Rosenbloom (1950): Elements of Mathematical Logic 
meaning of 'existence' ,
- "A third objection to the Boolean propositional logic goes back to Kronecker, and has been advanced in modern times especially by Brouwer and Weyel, and in more or less extreme form by others, notably Lusin. This objection originates in the question of the meaning of existence. The proponents of the point of view under discussion hold that an object exists only if a method is given for constructing it.
'naive' application of Law of Excluded Middle to infinite classes, the paradoxes
- " The motivation of the intuitionists' cirterion for existence is that the naive application of the law p V ~p to existential propostions involving infinite classes is known to lead to contradiction. Godel has shown that various Boolean popositional logics which have been proposed up to now and which are adequate for arithmetic, if consistent are inadequate to prove their own consistency, so that in this sense no Boolean logic of this very general type can be 'safe' ... The intuitionts say that a logic based on their principles is 'safe', that the restrictions thus placed on the naive logic which is known to lead to contradictions, are natural, that their criteria correspond to intuitively acceptable 'natural' laws of thought, and that the restrictions which have been proposed in the so far proposed Boolean logics in order to avoid the known paradoxes are ad hoc, i.e. manufactured for the specific purpose. One outstanding difficulty is the proof that the intuitionistic logic is actually 'safe'. According to another result of Godel, if the intuitionistic arithmetic is consistent, then so is the arithmetic based on the Boolean logic, so that the latter is as 'safe' as the former. On the other hand, Godel's work shows that every sentence in the latter can be translated into a sentence in the intuitionist arithmetic such that either both are provable in their respective logics or both are unprovable. Thus the intuitionist arithmetic is as adeequate as the Boolean arithmetic." Rosenbloom p. 57]
Transfinite induction, Gentzen
- " By using a method based on transfinite induction Gentzen has proved the consistency of a system which is adequate for arithmetic, bu the reasoning of Gentzen cannot be expressed in the object language itself...The consistency proofs of Gentzen and others for systems adequate for large parts of mathematics, even though they are based on methods which are under fire, for example by the intuitionists, are convincing to the extent that no one seems to try seriously to construct counterexaamples to results proved in this way...." (p. 73)
Intuitionism ultimately too complicated, but valuable because of insistence on constructive proof
- "Brouwer and his disciples have been attempting the reconstruction of mathematics in the effort to develop as much as possible by intuitionist methods. Nevertheless, may of the important properties of real numbers which are used in everyday mathematical practice cannot be developed on such a basis, and their intuitionist analogues are probably too complicated to be considered as adequate substitutes. On the other hand, the work of Godel, Kleene, and Nelson on intuitionist arithmetic provides a certain justification for that point of view and makes it seem less dogmatic and more plausible.... We repeat that the work of the intuitionists is valuable even for those who do not accept their phiolosphy, since a constructive proof often carries with it important additional information which is not yielded by a non-constructive proof." (p. 73)
The Axiom of Choice In Section 7 THE AXIOM OF CHOICE Rosenbloom observes:
- "...Obviously the intuitionists are strong opponents of the axiom of choice. Often these opponents profess not to understand the very meaning of existence without explicity construction." (p. 147)
He follows with a sly aside:
- "It follows for this reason that the axiom of choice is so useful, and simplifies so much of mathematics, that opponents of this axiom, when not writing about the foundations of mathematics, often make free use of it." (p 151)
On page 199 Rosenbloom discusses intuitionistic references in annotated bibliography but ... provides no actual bibliography! Whether the edition is flawed or the original is flawed is unknown.
The names he mentions are the following: Brouwer, Weyl, Heyting, Dresden, Lusin. "Interpretations" by Komogorov, Godel. Postulates of Gentzen. Further papers by Heyting, Godel, Glivenko, McKinsey, Wajsberg, Kleene, Nelson.
wvbaileyWvbailey 18:19, 27 June 2006 (UTC)
Martin Davis 2001: Engines of Logic 
Wallace says in his review that "Davis also mentions the Dutch mathematician L.E.J. Brouwer, who propounded somethat unorthodox views, largely discredited, on the foundations of logic. 'Although Brouwer never recanted his views," Davis writes, "he felt more and more isulated, and spent his laast years under the spell of totally unfounded financial worries and a paranoid fear of banruptcy, persecution, and illness'" [review at http://www.alicbot.org/articles/wallaace/mathematicians.html]
Stewart for Encyclopedia Britannica 2006 
Stewart's reference in E.B.:
- "Errett Bishop and Douglas Bridges, Constructive Analysis (1985), offers a fairly accessible introduction to the ideas and methods of constructive analysis."
- "Constructive analysis
- "One philosophical feature of traditional analysis, which worries mathematicians whose outlook is especially concrete, is that many basic theorems assert the existence of various numbers or functions but do not specify what those numbers or functions are. For instance, the completeness property of the real numbers tells us that every Cauchy sequence converges, but not what it converges to. A school of analysis initiated by the American mathematician Errett Bishop .... This philosophy has its origins in the earlier work of the Dutch mathematician-logician L.E.J. Brouwer, who criticized “mainstream” mathematical logicians for accepting proofs that mathematical objects exist without there being any specific construction of them (for example, a proof that some series converges without any specification of the limit which it converges to). Brouwer founded an entire school of mathematical logic, known as intuitionism, to advance his views [italics and boldface added]
- "However, constructive analysis remains on the fringes of the mathematical mainstream... Nevertheless, constructive analysis is very much in the same algorithmic spirit as computer science, and in the future there may be some fruitful interaction with this area" (Britannica Analysis/Constructive Analysis)
wvbaileyWvbailey 13:10, 15 June 2006 (UTC)
W.S. Anglin (1994) Mathematics: A Concise History and Philosophy, Chapter 39 Foundations 
In his Chapter 39. Foundations, Anglin has three sections titled “Platonism”, “Formalism” and “Intuitionism”. I will quote most of “Intuitionism”. Anglin begins each as follows:
- ”Platonists, such as Kurt Gödel, hold that numbers are abstract, necessarily existing objects, independent of the human mind” (p. 218)
- “Formalists, such as David Hilbert (1862-1943), hold that mathematics is no more or less than mathematical language. It is simply a series of games...” (p. 218)
- ”Intuitionists, such as L. E. J. Brouwer (1882-1966), hold that mathematics is a creation of the human mind. Numbers, like fairy tale characters, are merely mental entities, which would not exist if there were never any human minds to think about them.
- ”Intuitionism is a philosophy in the tradition of Kantian subjectivism where, at least for all practical purposes, there are not externally existing objects at all: everything, including mathematics, is just in our minds. Since, in this tradition, a statement p does not acquire its truth or falsity from a correspondence or noncorrespondence with an objective reality, it may fail to be ‘true or false’. Thus intuitionists can, and do, deny that, for any mathematical statement p, it is a logical truth that ‘either p or not p’.
- ”Since intuitionists reject objective existence in mathematics, they are not necessarily convinced by the reasoning of the form:
- ”If there is not mathematical object A, then there is a contradiction; hence there is an A.
- [I found this confusing. Does he mean: There exists B: (~A -> ~B) & B -> A [?]]
- [I think you're correct, but without a logical order defined, your statement is ambiguous...
- A better form is that of "There exists B: ((~A -> (~B & B)) -> A)"]
- "If the details of the reasoning provide a way of imagining or conceiving an A, in a way open to ordinary human beings by, say, calculating it in a finite number of steps), then the intuitionist will agree that there is, indeed, an A. However, if the details of the reasoning do not provide this, the intuitionist will remain skeptical. For a Platonist, it is of interest that there is an A even if it is only God who can conceive it. For an intuitionist, however, a mathematical object is meaningless unless it can be somehow ‘constructed’ and ‘intuited’ by a human being.
- "For the intuitionist, the human mind is basically finite, and Cantor’s hierarchy of infinites is just so much fantasy. Intuitionists thus reject any mathematics which is based on it, including most of calculus and most of topology.
- "... To ... objections, the intuitionist can replay: (1) it does not make sense for human minds to try to conceive a world without human minds, and (2) it is better to have a small amount of mathematics all of which is solid and reliable than to have a large amount of mathematics, most of which is nonsense”(p. 219)
wvbaileyWvbailey 16:01, 27 June 2006 (UTC)
Comment by User:126.96.36.199 
I feel I should alert the editors that the statement "Intuitionism takes the truth of a mathematical statement to be equivalent to its having been proved" is plainly false. This better describes formalism.188.8.131.52 23:49, 10 October 2006 (UTC)
Article rating 
This is a Start-class article. It has a lot of references, but the article itself is very short, and the main section is written in a way that would make it hard for the average person to read it without knowing what is going on already. This article is rated Mid importance because of its wide interest to people who are not well trained in logic, so the article needs to be especially novice-friendly (and correct, and neutral in viewpoint) to be a resource for them. Important topics like the BHK interpretation are currently not mentioned at all. CMummert 19:18, 25 October 2006 (UTC)
Missing reference 
The text refers to Davis (2000) but there is no entry for this in the references. The references also appear to have a formatting problem - the second and subsequent references are indented when they probably should not be. —The preceding unsigned comment was added by 184.108.40.206 (talk) 01:32, 4 March 2007
- Fixed. The indents show which papers in van Heijenoort are applicable (as there are many papers). wvbaileyWvbailey 14:03, 5 June 2007 (UTC)
Comment by Frank Waaldijk (user Frank W) 
This is a truly terrible page. It mixes philosophical motivation with pure mathematics in an incomprehensible manner. It is on the verge of gross untruth. I cannot even begin to discuss the incredible misinterpretation displayed here of what intuitionistic mathematics is about.
Intuitionistic mathematics is a branch of pure mathematics, conforming to all the high standards of this exact science. The difference between intuitionism and classical mathematics can be expressed by an axiomatic difference, comparable to the difference between euclidean and non-euclidean geometry. Furthermore, intuitionistic theorems require constructive proofs. This simply means that added to being a mathematical truth, an intuitionistic theorem also carries a lot of computational information. The notion of truth is no more vague in intuitionism than it is in classical mathematics, in fact one could easily argue that it is much more precise in intuitionism.
I think this page should be restarted from scratch. --Frank W 10:56, 4 June 2007 (UTC)
- I disagree utterly. If you want to write a screed re "intuitionism for experts" this is not the place. This is an encyclopedia. The first banner/flag that will go up will be "inaccessibility" and the screed will be rewritten. (i) The philosphic components -- e.g. nature of "truth" and "falsity" -- is just part of what distinguishes intuitionism from the other -isms. (ii) The history -- Brouwer's obsessiveness versus Hilbert et. al., Weyl's turn to the "dark side" etc. -- are a necessary component for a newbie's understanding; also, the disappearance to some degree of "intuitionism" -- why is this? (iii) Because of their importance to "logic", the LoEM and double negation invoked in non-finitistic proofs (i.e. reductio ad absurdum over the infinite) appears as a fundamental sticker that rippled (and perhaps continues to ripple) throughout "traditional logic" -- for example in Principia Mathematica (1913, 1927) the authors state on p. 13 (Chapter 1, Primitive Propositions):
- "Some simple propositions. In addition to the primitive propositions we have already mentioned, the following are among the most important of the elementary properites of propositions appearing among the deductions.
- "The law of excluded midddle:
- " -> .p V ~p
- "This is *2.11 below.
- "The law of contradiction (*3.24):
- "-> .~(p.~p)
- "The law of double negation (*4.13)
- "-> .p = ~(~p)" [etc. pp. 12-13]
- "The law of excluded midddle:
- You take these away and you have a serious degradation of "logic" (Hilbert's complaint). For example, Gödel wrestled with whether or not intuitionism was "viable" -- you see it prominently in his writing and in his biographies. I hope this won't be another instance of big hat no cattle: if you rewrite something please present your sources with their in-line citations, and in the spirit of intuitionism try to be constructive, please. A section on "modern intutionism" or "formal intuitionism" [writ ironic] would be a good addition to the page. wvbaileyWvbailey 13:49, 4 June 2007 (UTC)
Please allow me to repeat that this article is definitely NOT understandable for ANY beginner, IF you wish them to grasp what intuitionistic mathematics is. Like I said intuitionistic mathematics is a branch of pure mathematics. I fail to see why that statement is too hard to grasp for a beginner. On the other hand, the concept of truth is a difficult philosophical issue, which broadly speaking plays an equal role in classical mathematics and intuitionistic mathematics alike. Definitely no beginners' stuff, please avoid, but IF you insist on it then please do it correctly, since like you stated this is an encyclopedia.
However I'm ready to give up on this discussion, I have better things to do. I'm not going to rewrite anything here, I just wanted to point out that this article in my not so humble opinion is very far from its supposed goal: enlightening beginners about intuitionism. (signing off semi-permanently...if you wish to know more about my own work on intuitionism, check out my math page on http://home.hetnet.nl/~sufra/mathematics.html ). --Frank W 17:03, 4 June 2007 (UTC)
Cantor's hospitalization ?? 
still hardly any improvement in this misleading article 
i have neither much time or energy to put into this discussion, but i am as disheartened as i was last year to see what wikipedia still manages to produce under `intuitionism'.
did anyone with a mathematician's background in intuitionism contribute to this article?
i cannot imagine so. this article does more damage than good. it gives a very distorted image of a perfectly pure branch of mathematics, which -in contrast to what is stated somewhere above- has not disappeared at all but is very alive. apart from intuitionism itself, much of brouwer's work has been adopted in computer science, in so-called constructive mathematics and also in formal topology.
there is no mathematical vagueness in intuitionism. there are extremely clear axioms, from which the theory is built in a mathematical rigorous way, just as one would expect in any branch of pure mathematics.
my advice is to split this article into two articles, one called `intuitionistic mathematics' and one called `history and philosophy of mathematical intuitionism'. the latter could act as a continuation of the current article - if corrected, since it even contains many errors and omissions on this score.
the first article `intuitionistic mathematics' should as i stated one year ago be started from scratch. if i get any sign that people would be happy to see some form of such articles, i might be tempted to write a first version of this first article. Frank W (talk) 20:22, 25 June 2008 (UTC)
- Please be bold and create the division, maybe putting up a stub for the Intuitionism (mathematics) subarticle. Diego (talk) 21:32, 25 June 2008 (UTC)
- No, I think there's no need for that sort of division. Please be bold and take an axe to this article. Or maybe start at constructive mathematics which is also a bit dodgy right now. Or maybe start a choice sequence article, which is still a red link. --Unzerlegbarkeit (talk) 21:47, 25 June 2008 (UTC)
The phrase "Thus the connectives "and" and "or" are not dual in intuitionistic logc as they are in classical logic" is an appealing one but I wonder to what extent it can be sourced. The phrase tends to imply that there is a notion of duality even for intuitionistic logic, but and and or don't satisfy it. In reality it seems to me there is no such duality. Or is there? Since negation is not an involution, how is such a duality to come about? Tkuvho (talk) 15:02, 23 January 2011 (UTC)
- If there is no duality at all in intuitionistic logic, then the claim "the connectives are not dual as in classical logic" is still perfectly reasonable, because that only refers to the notion in classical logic. Nevertheless, I replaced the word "dual" with "de Morgan's laws". It seems to me that this is a completely trivial wording issue. — Carl (CBM · talk) 17:11, 23 January 2011 (UTC)
- There are some other sorts of duality, but I don't have a big picture of the research. One way to get some duality is to have a "strong negation", which was proposed by an old article in the JSL by Nelson; search for "Nelson strong negation". This involves an extra unary "strong negation" operator which is an involution. There is also something called "bi-intuitionistic logic" which is based on some other sort of duality. But all that the article here was trying to say is that de Morgan's laws fail. — Carl (CBM · talk) 18:20, 23 January 2011 (UTC)
Naive question 
Reading between the lines, this article (and a few other related ones) seem to suggest that by rejecting the law of the excluded middle (LoEM), that somehow infinities are also rejected. But this is quite unclear. Is it that the intuitionists reject the axiom of infinity or something like that?? Or maybe by rejecting LoEM, various proofs and arguments fail, such as the Cantor slash? Somehow one is no longer able to prove/derive/deduce the uncountable infinity? Is it impossible to deduce large cardinals simply by abandoning LoEM? Or is this completely unrelated? Maybe these just happen to be two distinct issues having nothing to do with each other???
Do intuitionists reject any particular axioms in ZFC, or or do they accept them all? Would it be valid to define "modern-day intuitionism" as 'all the axioms of zfc but only inuitionist logic is used' ? I suspect, as commented by user Frank W, there is some rigorously defined modern-day conception of intuitionism (that abandons the baggage of the historical debate, and replaces it with some axioms or models or whatever). But what is it? linas (talk) 02:56, 22 April 2012 (UTC)
- The term "intuitionism" in general is difficult, because there are two threads in history: the development of constructive mathematics, and the legacy of Brouwer's personal philosophy of "intuitionism". The former has been quite influential; the latter not so much. If I want to talk about mathematical systems that don't have the excluded middle, I prefer to just call them "constructive". But if I want to talk about Brouwer's philosophy, and particular topics like choice sequences that he found philosophically important, I would call them "intuitionistic". However, the term "intuitionistic" also gets used for systems that are "constructive" but which Brouwer might have completely disapproved of. In particular "intuitionistic logic" refers to various logics without the excluded middle, not to Brouwer's philosophy. So you have to infer what each author means when you read their writing.
- In any case, there is nothing in constructive mathematics that prevents uncountable sets or completed infinities. Both constructive set theories (like CZF/IZF) and constructive type theories are fine with uncountable sets. There might be some philosophical objections of Brouwer to uncountable sets, but those objections are part of the philosophical program of Brouwerian intuitionism rather than the mathematical program of constructive mathematics. — Carl (CBM · talk) 11:36, 22 April 2012 (UTC)
- It's also worth knowing that the constructivists are a little like Protestants. After splitting from their historical "church" of classical mathematics, the proto-constructivists began bickering with themselves over details and now there are lots of small constructive "denominations" rather than a unified single group of constuctivists. The classic Varieties of Constructive Mathematics gave an overview of three of the more influential denominations at the time; since then topos theory and CZF/IZF have gained more prominence. So any claim that "all" constructivists think one thing or another has to be viewed with great suspicion. — Carl (CBM · talk) 11:45, 22 April 2012 (UTC)
- Thanks. I'd been playing with answer-set programming recently, which explicitly rejects the law-of-excluded middle. The solvers are implemented using the modern SAT solver algorithms. One distinctive feature is that most solvers don't implement disjunction, for some kind of algorithmic reasons I don't understand: implementing it is somehow hard, or makes everything run slow, etc. Instead, they work around this by using "aggregates" and other ideas/tricks. One primary trick, ahem, distinctive aspect of solving problems using ASP is to first specify/instantiate the entire universe, and then trim it down (using conjunctions), until the desired solution (obeying all of the sentences that you've specified) is found. Of course, this universe is finite; but I thought it was kind over interesting to start with "everything" and then whittle things down, this being forced by algorithmic efficiency considerations. It got me to daydreaming... linas (talk) 03:54, 25 April 2012 (UTC)