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?

3
  • 3
    I don't know if it was abandoned so much as never having been more than an intellectual curiosity. Feb 25, 2023 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 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, 2023 at 1: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, 2023 at 6:01

3 Answers 3

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.

17
  • 5
    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. Feb 26, 2023 at 17:24
  • 5
    (-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. Feb 27, 2023 at 6:50
  • 3
    Can you summarize this inconsistency in a few words, or link to an explanation? Feb 27, 2023 at 9:52
  • 3
    "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. Feb 27, 2023 at 12:41
  • 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. Feb 27, 2023 at 16:27
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.

1
  • 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, 2023 at 15:27
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.

1

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .