Is disjunction pointless in intuitionistic logic?

Question

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

Answer 1

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.

Answer 2

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?