5

I have seen many questions discussing intuitionist logic (Brouwer, Weyl etc.) on the site.

However, this whole area of logic seems to be dead, and it also looks like philosophers / mathematicians / logicians don't even take it seriously (or am I mistaken?).

I find intuitionist logic interesting, it was very much in the spirit of Schopenhauer, Nietzsche and Heidegger. It's a curious fact that Wittgenstein was so amazed by a Brouwer lecture in 1929 that he decided to get back to philosophy after a 16 year long break. However, he described intuitionist logic as "nonsense, all of it".

What caused the decline / death of attempts to found logic on immediate human intuition?

Mauro ALLEGRANZA
  • 35,764
  • 3
  • 35
  • 79
Dennis Kozevnikoff
  • 1,247
  • 2
  • 15
  • 3
    I don't know if it was abandoned so much as never having been more than an intellectual curiosity. – David Gudeman Feb 25 '23 at 23:00
  • 8
    What makes you think it is abandoned? It was and is a minority view, so it does not get as much exposure, but the minority is stably reproduced in each generation and remains active. It got additional boost from interest in constructive mathematics with the rise of computers and computational applications, see [SEP survey](https://plato.stanford.edu/entries/mathematics-constructive/) that includes recent references. However, the name is not descriptive. Founding logic on intuition applies as much to classical logic as to intuitionistic one, they just emphasize different intuitions. – Conifold Feb 26 '23 at 01:25
  • 3
    I agree with Conifold. It is a minority interest, but alive and well. Particularly in the case of intuitionistic type theory and topos theory. Per Martin-Löf and Dag Prawitz are leading logicians who use it. Intuitionism as a philosophy of mathematics is no longer common, but the logic has taken on a life of its own for understanding constructive mathematics and computation. – Bumble Feb 26 '23 at 06:01

3 Answers3

24

Intuitionistic logic is certainly not abandoned in math. Even if most people use classical logic, there is still a large community of people who work with intuitionistic foundations, look up for example homotopy type theory.

Furthermore, even if one is only interested in working with classical foundations, intuitionistic logic can still be useful. For example toposes are used in algebraic topology (and in other areas). And toposes have something called their internal logic, which in general is a form of intuitionistic logic.

Carla_
  • 341
  • 4
  • 1
    I upvoted, but allow me to emphasize on something, mainly for other people, not for you: people don't use logic! Only their proofs do. The "choice of a logic" is not at all a philosophical problem for the person who is writing proofs. For example, I don't need to "believe" in the axiom of choice (in fact, I think this sentence has no meaning) to write proofs that use it (or that use its negation). – Plop Feb 27 '23 at 15:27
10

The chief difficulty of intuitionistic logic seems to be that it is cumbersome and difficult to use. It is not truth-functional, which means that the truth-table methods that work to establish or verify tautologies and theorems in classical logic cannot be used, and a strictly deductive approach must be employed. Since intuitionism has non-standard rules of deduction, it is more difficult to handle, and in practice is not nearly as intuitive as the name promises.

This does not seem to be accompanied by any great advance in explanatory power. While it raises some intriguing possibilities with its rejection of the the Law of the Excluded Middle while retaining the principle of Bivalence, and its exploration of of the distinction between true and provable, its connections with other branches of non-classical logic is obscure.

My own opinion is that the chief importance of intuitionism is theoretical and historical, but it contains a subtle, hidden inconsistency in its concept of negation which makes it fundamentally and uncorrectably flawed and ultimately a dead end. Better results can be obtained with 3-valued logic.

#Edit: I have modified my opinion. Intuitionism is an incomplete, asymmetrical, and partial rejection of the law of the excluded middle. It is compatible with 3-valued logic as far as it goes, but it doesn't go far enough for identity.

Confutus
  • 574
  • 2
  • 9
  • Is there a replacement for truth tables of some kind? Seems fatally impractical to work with only deductions. – J Kusin Feb 26 '23 at 17:10
  • 4
    On explanatory power: the intuitionistic ∃ *x*. P(*x*) is provable exactly when there exists an algorithm to compute a suitable *x* which satisfies P. (Proofs for other quantifiers and connectives can similarly be given interpretations as algorithms.) So I think there is a very real sense in which it is explanatory of what computation can be done, and I think it's hard to deny that computation underlies a large fraction of modern society. – Daniel Wagner Feb 26 '23 at 17:24
  • @ J Kusin It's already been established that it cannot be reduced to a finite set of truth values. It does seem impractical to use deduction only, but if there are other methods, they do not appear to simplify it. – Confutus Feb 26 '23 at 20:48
  • 4
    (-1) This does not answer the question, "difficult to use" is not a valid reason for "abandoning" the study of a subject and as the other answer shows, the subject is by no means abandoned, and has a lot of applications in rising fields of math. – Vivaan Daga Feb 27 '23 at 06:50
  • 3
    Can you summarize this inconsistency in a few words, or link to an explanation? – reinierpost Feb 27 '23 at 09:52
  • 1
    "truth-table methods that work to establish or verify tautologies and theorems in classical logic cannot be used" But truth table works for propositional logic only, and no one can develop mathematics using prop logic alone. – Mauro ALLEGRANZA Feb 27 '23 at 12:41
  • @DanielWagner: Your sentence about the provability of $\exists x, \ P(x)$ being equivalent to the existence of an algorithm computing an $x$ satisfying $P$ is not true. – Plop Feb 27 '23 at 15:30
  • @Plop Err, hm. That's troubling, it seems I've misunderstood something important. Would you care to expand on that a bit and teach me? – Daniel Wagner Feb 27 '23 at 15:37
  • Sure! Let $P$ be any proposition with one free variable. For all $x$, define $A_x := "return x;"$. If $P$, then there exists $x$ such that $A_x$ returns something that satisfies $P$. Et voilà ! – Plop Feb 27 '23 at 15:42
  • @DanielWagner: I think the true statement is: $\exists x,\quad P(x)$ is provable if and only if there is a term $t$ such that $P(t)$ is provable. See 4.2 https://plato.stanford.edu/entries/logic-intuitionistic/ or 3 https://ncatlab.org/nlab/show/intuitionistic+logic – Plop Feb 27 '23 at 16:01
  • 1
    @Plop Yes, good point. There must also be an algorithm to check that P(*x*) holds for the *x* you compute. I was a bit sloppy there. But I think the point stands: there is a strong connection between intuitionistic logic and computability that I think makes it useful and explanatory in a way that classical logic isn't. – Daniel Wagner Feb 27 '23 at 16:27
  • 1
    If you are talking about the Curry-Howard correspondence, then sure! – Plop Feb 27 '23 at 16:31
  • @Mauro ALLEGRANZA If the domain of a propositional function is a finite set of objects, classical propositional logic works fine as a basis for predicate logic. The problem comes with the pesky infinities. – Confutus Feb 27 '23 at 17:51
  • @ Shinrin-Yoku I'm not saying that difficulty in using and interpreting it is sufficient reason for neglecting it it. I don't claim to be a majority of mathematicians or philosophers. – Confutus Feb 27 '23 at 18:04
  • @reinierpost Proof by contradiction is tricky in 3vl. Specifically, ((P -> (P & ~P)) -> ~P) doesn't hold for the equivalent of intuitionistic negation. – Confutus Feb 27 '23 at 18:06
  • @Confutus: That's not a bug, it's a feature. What is more: it is the whole point. In intuitionism, we may only say something exists when we can show an example. That is a perfectly sensible point of view. – reinierpost Feb 28 '23 at 21:10
  • @reinierpost The devil is in the details of necessary falsehood and necessary implication. Proof by contradiction (which is what this statement is about) has more stringent requirements in 3vl than it does in intuitionism. The effect is to make the systems incompatible. – Confutus 1 hour ago – Confutus Feb 28 '23 at 23:23
8

Artificial Intelligence is one discipline that over the last 50 years has looked for models of logic to deal with bounded rationality, and while connectionist models are all the rage and are being funded by industry at a tremendous rate, symbolic systems employed in automated reasoning employ a tremendous variety of logics. I've never heard of intuitionistic logic itself characterized as failing. Intuitionist type theory is one theory that came from it that still receives attention. And the defeasibility of human reason certainly precludes classical logic as sufficient as a model for human reasoning. Both Montague grammar and Kripkean semantics can be squared with intuitionistic logic. Perhaps its best to characterize intuitionistic logic as influencing logicians to broadening logical research into a pluralism of non-classical models beyond Aristotle and Tarski's narrow conception in the same way non-Euclidean geometry freed geometers from Euclid. If that's the measure of success, then intuitionistic logic is not only NOT dead, but Brouwer is immortal. In fact, among category theorists, topoi, which are a category class can be conceived as an intuitionist endeavor since topoi ground logical systems generally.

EDIT

In response to Frank's request for intuitionistic logic implemented in AI, I'll just say that I only meant to imply that intuitionistic logic inspired AI to move beyond classical logic into non-monotonic logics and paraconsistent logic, however I think it's defensible to say that AI implements intuitionist automated reasoning systems, also. For instance, one type of human-machine implementation that uses intuitionistic logic is the proof assistant. At random, I'd offer Agda which is based on an alternative to the intuitionistic type theory of Per-Lof and implemented in Haskell and is capable of constructing proofs. In fact, while Agda is contemporary, John McCarthy, the man who cointed "artificial intelligence" had a system called circumscription, which starts as a FOL non-monotonic logic and attempts to construct proofs by extending truth piecewise. Nils J. Nilsson characterizes the specific predicate circumscription as "limiting the set of entities that make predicates true to just those that can be proved to be true." Thus, double negation isn't presumed since the system can handle propositions that 'it is not the case that the statement is not true' only by extending truth to determine 'a statement' is true.

My caveat, though, is that it's not entirely clear to me as a non-logician, about where to draw the line of the application of intuitionistic logic between man and machine, which is a philosophical question in and of itself.

J D
  • 19,541
  • 3
  • 18
  • 83
  • 1
    **Comments have been [moved to chat](https://chat.stackexchange.com/rooms/143241/discussion-on-answer-by-j-d-why-was-intuitionist-logic-abandoned); please do not continue the discussion here.** Before posting a comment below this one, please review the [purposes of comments](/help/privileges/comment). Comments that do not request clarification or suggest improvements usually belong as an [answer](/help/how-to-answer), on [meta], or in [chat]. Comments continuing discussion may be removed. – Geoffrey Thomas Feb 28 '23 at 08:39