# What do dual-intuitionistic and minimal logic model?

As someone interested in theoretical computer science, I'm fairly comfortable with what intuitionistic logic represents. An intuitionistic proof is a proof we can act upon algorithmically. The law of the excluded middle is rejected because we don't have a magic oracle which can decide any proposition, and thus tell us what to do. By contrast, classical logic assumes that there is such an oracle, and our job is to work out what answer it will give us without invoking it.

Minimal logic can be described as intuitionistic logic without the law of non-contradiction, and dual-intuitionistic (Brazillian) logic is made similarly from classical logic. However, I'm lacking intuition as to how the lack of the law of non-contradiction can be justified. My guess is that – as eschewing A ∨ ¬ A gives positive proofs structure – eschewing ¬ (A ∧ ¬ A) gives negative proofs structure. But I don't know what one might want to do with structure in an impossible situation.

Also, I expect that there is an equivalent of the intuitionistic practice of excluding the middle for certain families of propositions. For example, we can usually justify the fact that ∀ x y : ℕ. (x = y) ∨ ¬ (x = y) by saying that equality of natural numbers is algorithmically decidable (and actually proving it via the Curry-Howard correspondence). I don't know what would recover non-contradiction on a family of propositions, but it surely holds for many of the families of propositions considered in ordinary mathematics.

• Welcome to Phil.SE! A quick question, when you say that minimal logic does 'without the law of non-contradiction'; is this the same as the law/principle of explosion? Commented Aug 20, 2016 at 10:52
• No, I am very much separating the ideas of (A ∧ ¬ A) and ⊥, and saying that (A ∧ ¬ A) → ⊥ is not true in all cases. To me, ⊥ ⊢ P defines ⊥. If I misunderstand, and there are no interesting logics like this, please mention it. But I'm interested in lack of A, ¬ A ⊢ ⊥. Commented Aug 20, 2016 at 11:46
• the article that you link to for minimal logic specifically mentions the principle of explosion - you might want to take a closer look. Commented Aug 20, 2016 at 12:02
• Actually yeah, upon a closer look, it does. I guess I'm okay with ⊥ ⊢ ¬ P being the rule, at least for the sake of this question. But maybe I don't want to define ¬ A as A → ⊥, as suggested in this bit about dual-intuitionistic logic (specifically with mention of #). I'm happy about an answer for either, if it gives rise to some interesting and applicable logic. Commented Aug 20, 2016 at 12:09
• One use of these is to leave the basic logic of a construction very weak and clap a complex metric on the outside. Basic inconsistency is probably not useful, but limited inconsistency models realistic situations like law, which are almost always inherently overdetermined for historical reasons. (E.g. I have worked in optimization of labor plans for chain stores, where policies (and even laws) simply are going to be violated. You want contradiction to be reluctant but not forbidden. You want to actively generate degenerate solutions and rule them out in competition.)
– user9166
Commented Aug 20, 2016 at 13:49