# Is disjunction pointless in intuitionistic logic?

Sec. 5.3 of the SEP article on constructive and intuitionistic set theories makes note of a property meant for theories that compromise on the LEM:

A theory T has the disjunction property (DP) if whenever T proves (ϕ∨ψ) for sentences ϕ and ψ of L(T), then T proves ϕ or T proves ψ.

What is the point of even having disjunction in such a system? If I am inclined to say, "It's raining or it's not," then I will be thinking that I don't know one way or the other; maybe I'm in a dungeon somewhere, for example, and have no chance of finding out (unless I somehow escape or am released on this very day, or a weather-reporter angel visits me, or whatever). I won't even have much of a "theory" (about what? the weather?) behind my claim; or, then, no theory such that I would believe I could know if it's raining by inference (deductive or not) from said theory.

For all that, I will still be thinking that if it's raining, then it's not not raining, and if it's not raining, then it's not raining. If I knew there was a way to find out (an "intuition" of raining/not-raining) at the same time as I was wondering, then I would have reason to just look to my intuition to tell me. If I didn't have such an intuition (because I'm in a dungeon, etc.), and I thought a disjunction indicated the availability of such an intuition, why would I make a disjunctive statement at all? Generally, I seem able to intend to refer in an exclusively disjunctive way, i.e. my will to refer can disjoin A from ~A in every case, so either I reject the display of my semantic will (in the syntax of disjunction) in the first place, or I just use the word "or" in the usual way.

Caveat: however, I can appreciate the sentiment:

1. The absence of a term x is not the same as a term for the absence of x.

Then, modulo questions of trying to quantify over "all numbers" and the like, I understand where predicativists and intuitionists are coming from, even in the way of compromising on the LEM for infinity-talk (the absence of my knowledge of a number with a property P is not equivalent to knowledge that such a number is itself absent from the indeterminate ensemble of absolute infinity). Even so, I would think something like what I think about dialethic logic: even if there are (natural-language) versions of the concept/word "or" (or "not") that aren't exclusive, there is still the exclusive use of those terms regardless, and when I say, "For all assertions A, either A is true or A is not true," I mean by that the exclusion function (whether or not there is some broader notion of quasi-exclusion that intuitionists/dialethicists are working with on their side of things).

• In constructivism (and anti-realism more broadly), disjunction is not about having an "intuition", but about having a way to verify "in principle". This is why, for example, disjunction is constructively valid when one can find out which disjunct is true by finite exhaustive search, even if the said search is beyond one's physical capabilities. And, "in principle", one has a way to get out of the dungeon. Commented Aug 3, 2023 at 16:23
• To prove A ∨ ~A I don’t have to prove either disjunct, like the common approach for A ∨ B. Just go right to a tautology law and it’s a theorem (classic). For A v ~A constructively, I have to be able to prove/verify either disjunction. But my goal was more than just a singular disjunct. So it doesn’t appear useless Commented Aug 4, 2023 at 10:20
• @JKusin I think I misworded my question. I should have asked something more like, "Is disjunction introduction redundant in intuitionistic logic?" since per the two answers below, I'm seeing that that's where my confusion/disagreement shows up. Broadstroke claims of pointlessness/uselessness were easy to falsify, even though I appreciated that there was some sense behind my question. I'm reluctant to edit my question, though, since that would make the given answers less applicable, and I don't want to prompt people to edit their answers for a mutating question 😕 blargh! Commented Aug 4, 2023 at 13:23
• Okay wasn’t sure if you were still unsure about their answers. I don’t know a ton of background, but proving wise, it’s not redundant. It’s a way to talk about important universes of discourse for one. It’s useful to prove: “all integers are even or odd”. That’s the goal of the proof. “v” is central to the semantics of that important goal, not redundant. If we can come up with a way to prove for any integer, either it is odd or it is even, we have succeeded. We can’t use tautology law, but we can keep the disjunctive, useful goal intact and prove constructively. Commented Aug 4, 2023 at 17:13
• I do see a lot of sense outside of the proving aspect. We don’t have as much “intuition” for the behavior of things outside mathematical objects, so constructive methods + disjunction carried over to the real world does seem a bit odd. Commented Aug 4, 2023 at 17:22

Intuitionism has a verificationist semantics. The point of a disjunction, like any connective, is that it tells you how to verify it. You want to verify φ ∨ ψ? Well then verify φ or verify ψ. Those are the only options to an intuitionist. You want to verify φ ∧ ψ? Verify φ and verify ψ. You want to verify ¬φ? Verify that there is no verification of φ.

Note that I am explaining intuitionism here, not defending it. For myself, I am quite happy with using non-constructive proofs where appropriate.

If this seems strange, consider that the way disjunction behaves in a computer program is much closer to being intuitionistic than classical. Most programming languages allow you to write something like this:

``````IF < A > OR < B > THEN do < X >.
``````

Where < A > and < B > are expressions that evaluate to a boolean value. The computer will evaluate < A > and if it evaluates to false, evaluate < B > in order to get a value for the disjunction. But the crucial point is that the computer must actually get a truth value for < A > or for both. This is comparable to the way that in intuitionistic logic, to prove φ ∨ ψ you must prove φ or prove ψ. If the computer proceeds to do < X > then it is because < A > has been evaluated as true or < B > has been evaluated as true.

If you were to write:

``````IF < A > OR < not A > THEN do < X >.
``````

the computer is not going to say, Aha! you've written a classical tautology, so I'm going to do < X > without bothering to check on the value of < A >. The computer will evaluate < A > and if it is false, it will evaluate < not A >. If one or other evaluates to true, then < X > happens. And, unless you are using a pure functional language, which is very rare, there is actually no guarantee that one or other will evaluate to true, so there is no guarantee that < X > happens.

• Intuitively one should never code a tautology in above conditional expression, thus this example actually defends intuitionism, seems contrary to your intention. Maybe a better example to critique intuitionism could be found in proof related to infinity… Commented Aug 4, 2023 at 19:07
• @DoubleKnot I'm not trying to critique intuitionism. For myself, I am happy with a pluralistic approach to logic, and there are plenty of applications where I would happily use intuitionistic logic. The point I am making with my examples from programming languages is that disjunction in programming is intuitionistic, not classical. So, in answer to the question of whether intuitionistic disjunction is pointless, my response is far from it: programmers use it all the time and it's fine. Commented Aug 4, 2023 at 20:59
• Logical pluralism implicitly critiques some logic in some specific use cases. Re your using a pure functional language there’s guarantee one or the other will evaluate to true, if you mean Haskel like functional programming language to evaluate some statement involving floating point arithmetic, it’s same approximate nature as other imperative languages, not sure what do you mean by that sentence… Commented Aug 4, 2023 at 22:00
• @DoubleKnot By pure functional language, I mean roughly those that treat computations as evaluations of functions with no side effects. en.wikipedia.org/wiki/Purely_functional_programming Haskell would qualify. My own favourite language, Lisp, is not pure. In a pure functional language A or not A is guaranteed to evaluate to True, but in other languages this is not guaranteed. Since pure functional languages are comparatively rare, my point is that disjunction in most programming languages is not classical. Commented Aug 4, 2023 at 22:34

I guess, your question reveals a common misunderstanding of intuitionistic logic. To us, the assertion of a disjunction, 'ϕ or ψ', is not a casual declaration of uncertainty. Instead, it is a promise that we can constructively demonstrate the truth of either ϕ or ψ. When you say, 'It's raining or it's not,' without a means to verify either, you're making a statement that lacks constructivist meaning. Our truths aren't abstract entities, but must be demonstrated constructively.

The disjunction property you mention is not a limitation, but an expression of this fundamental commitment to constructivism. We don't casually assert 'A or not A', because to do so asserts the ability to decide whether A is true. If we lack such decision-making means, we lack the grounds to assert the disjunction.

As to your point about an 'exclusive' version of 'or', I must say, there isn't a separate 'intuitionistic' interpretation and 'classical' interpretation. The intuitionistic interpretation isn't a 'broader' or 'quasi-exclusionary' understanding, but rather, the correct one. The classical logic's law of excluded middle, which allows for the assertion of 'A or not A' without the ability to decide between A and not A, is a misunderstanding. It's not about excluding, it's about constructing.

Would you agree then, that the essence of a statement's truth lies not in its abstract existence, but in our ability to construct and demonstrate its truth?

• I don't agree with that, though. I can focus on my mental willing and "intuit" that I can refer in an exclusive/disjunctive way (although this is more or less just generalized semantic intuition). But the main point is that: grant the intuitionist their sense of the word "or," yet I still don't see what the point of using the word "or" is. What does it add to intuitionism that is useful? Similarly, what does a dialethic logician have by retaining the word "not" that is useful "in the long run"? Commented Aug 3, 2023 at 15:19
• When intuitionists use 'or', they're kinda making a commitment to provide a constructive proof for one of the options. It's like saying, 'I can make an apple pie or a cherry pie, but only if I have the ingredients for one of them.' It's not just about the possibilities, but about the practicality of these possibilities.
– user66933
Commented Aug 3, 2023 at 15:29
• As for 'not', it's a basic way to express negation or opposition. In dialethic logic, 'not' is important in understanding and dealing with contradictions, which are allowed in this logic system. It's like saying, 'The light is not on.' Without 'not', we wouldn't be able to express this simple concept
– user66933
Commented Aug 3, 2023 at 15:30