What do dual-intuitionistic and minimal logic model?

Question

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.

Answer 1

Minimal logic is intuitionistic logic without ex falso quodlibet. One way to understand the difference in interpretation between minimal (ML), intuitionistic (IL) and classical logic (CL) is by considering the different way they treat the implication operator →. In ML, A → B can be interpreted as "I can show that a proof of A can be manipulated into a proof of B". Or if you prefer the language of computation to the language of proof, "I can show that a program that solves A entails a program that solves B". In IL, implication is a little broader: it means "I can show that a proof of A can be manipulated into a proof of B OR that a proof of A can be manipulated into a proof of a contradiction". Again, using computational language, "I can show that a program that solves A entails a program that solves B OR that there cannot be a program that solves A". In CL the interpretion is broader still because it means simply "A is false or B is true" without claiming to be able to prove which disjunct is true or being able to solve for either disjunct constructively.

Dual-intuitionistic logic is a form of paraconsistent logic, in which the law of non-contradiction is dropped. If one thinks of IL as holding that one may only assert a proposition A if one can construct a solution for it, then dual-IL can be thought of as one may assert A provided one has no refutation or counterexample to it. IL rejects LEM because there may be propositions A, ¬A such that neither is provable, but accepts LNC because A and ¬A will never both be provable. Dual-IL rejects LNC because there may be propositions A, ¬A such that neither are refuted, but accepts LEM by default. One might say that IL starts from an empty base and requires you to prove everything, while dual-IL starts from a maximal base in which everything is accepted unless it is expressly falsified.

As to whether dual-IL has a meaningful model, that is an open question. Paraconsistency has been defended by some logicians, e.g. Graham Priest, on the basis that some contradictions are true, e.g. those arising from semantic paradoxes.