Is there a modal modification of the law of excluded middle that may render constructive?

Question

Intuitionistic logic rejects the law of excluded middle, and paraconsistent logic rejects the law of non-contradiction. I wondered whether the rejected laws can still be incorporated, if they're modified with modal aspects.

I see an easy modification of the law of non-contradiction that is compatible with paraconsistency. Instead of ￢(P∧￢P), have ￢□(P∧￢P). I call this the law of unprovable contradiction. This law states that, though there might be true contradictions, they don't admit a proof.

But is there a modification of the law of excluded middle, P∨￢P, that constructivists won't frown upon? The particular candidate I'm seeing is P∨￢□P: Either P is true, or P doesn't have a proof. This law seems rather relaxed than P∨￢P. Would constructivists really accept this?

Answer 1

There are some moments in intuitionistic logic that resemble the options you've considered. Here's one from the SEP article on intuitionistic logic:

While ∀x¬¬(A(x) ∨ ¬A(x)) is a theorem of intuitionistic predicate logic, ¬¬∀x(A(x) ∨ ¬A(x)) is not; so ¬∀x(A(x) ∨ ¬A(x)) is consistent with intuitionistic predicate logic.

One approach to formalizing Brouwer's talk of a "freely creating subject" includes:

□_nA ∨ ¬□_n A (at time n, it can be decided whether the Creating Subject has a proof of A)

Earlier in the same entry, they note:

The dependence of intuitionism on time is essential: statements can become provable in the course of time and therefore might become intuitionistically valid while not having been so before.

So though we cannot have a strong first-order shadow of excluded middle, here, it seems that a strong second-order shadow is more debatable. Let β (following Gödel) mean "it is provable that" and ◊ mean "it is possible that," with □ meaning "it is necessary that" and w as "it will be true that." Then we can ask about:

1. □◊wβ ∨ ¬□◊wβ?
2. ◊□wβ ∨ ¬◊□wβ?
3. □◊wβ ∨ □¬◊wβ?
4. □◊wβ ∨ □◊¬wβ?
5. □◊wβ ∨ □◊w¬β?
6. □◊wβ ∨ □◊wβ¬?

... and so on and on; various permutations^!! seem to be less in tension with the philosophy behind intuitionism, while other permutations might run a greater risk of being inconsistent with that philosophy. I would like to find peer-reviewed analyses of such questions, but I'm not sure how exactly to search for them, though I expect that some do exist. At a glance, an overview of basic intuitionistic modal logic does not testify for or against various flavors of modal excluded middles, but then maybe see Simpson[94] or Paiva[15] for helpful details.

Corollary: not exactly a modal option, but we can also ask about the relationship between the concept of deminegation and excluded middle. Let √ be used to signal "the square root of negation." Then we might ask:

1. A ∨ √A?

Now, if one uses Paoli's analysis of √, one has (letting √ = f):

... which is isomorphic to the rotation of complex coordinates (1 + 0i), (0 + 1i), (-1 + 0i), (0 - 1i) around the origin in the complex plane. So it seems that the theory of √ supports quadruple negation elimination (since i⁴ⁿ = 1), which would be inconsistent with intuitionism. However, if we are willing to pursue the mathematical analogy further, we might distinguish √ from ∛, wherefore:

2. ∛∛∛A = √√A

But then:

3. ∛∛A = √A?
4. ∛A = √A?

Wherefore we might ask:

5. A ∨ ∛A?
6. A ∨ ∛∛A?

... and so on and on.

---

^!!This is a partial guess, but I think there would be 5! = 120 permutations to sort through, taking the set {¬, □, ◊, w, β} as our base.