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?

  • 2
    Sounds your paraconsistent law of unprovable contradiction modal logic replacing the classic LNC is in the right direction for a more rational compassionate agent application than the mere removal of LNC. As for your inclusion of modal LEM it won't impress constructivists since they really care only the proof instead of any supposed bivalent unadulterated truth while your proposal simply swept such interest under the carpet... Commented Aug 18, 2023 at 6:57

1 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):

enter image description here

... 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 i4n = 1), which would be inconsistent with intuitionism. However, if we are willing to pursue the mathematical analogy further, we might distinguish √ from ∛, wherefore:

  1. ∛∛∛A = √√A

But then:

  1. ∛∛A = √A?
  2. A = √A?

Wherefore we might ask:

  1. A ∨ ∛A?
  2. 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.

You must log in to answer this question.

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