# 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? – Mozibur Ullah Aug 20 '16 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 ⊢ ⊥. – James Wood Aug 20 '16 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. – Mozibur Ullah Aug 20 '16 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. – James Wood Aug 20 '16 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 Aug 20 '16 at 13:49

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.

• I'll probably mark this as the answer soon. Just a couple of questions remain. Firstly, what would we expect to do to establish ∀ x. ¬ (P x ∧ ¬ P x) for some specific P? And secondly, what can we actually do with ML's implication? I'll explain with an example. Suppose we define even inductively, so 0 is even, and for each even n, 2 + n is even. We then want to prove that, for each natural number n, if n is even, then there exists d such that 2 * d = n. Is this provable? How do we handle odd n? It seems as if implications can only be proven if the conclusion is true anyway. – James Wood Aug 20 '16 at 21:40
• Actually, no, I'm thinking wrong about the second question. There's no need to consider non-even numbers at all. Just stick to the first question. – James Wood Aug 20 '16 at 21:47
• You cannot establish it, you can only attempt to refute it by finding a counterexample. This may seem a weird way of looking at things, but it has been argued by Neil Tennant and Yaroslav Shramko and others that minimal logic is a way of describing Popperian falsificationism within the philosophy of science. You may advance any hypothesis you choose and you may attempt to refute it with a counterexample, but if you fail to refute it, this does not prove the hypothesis, it just leaves it unrefuted. – Bumble Aug 21 '16 at 8:46
• Here are links to the Tennant and Shramko papers: u.osu.edu/tennant.9/files/2014/07/tennant_bjps1985-2m81cww.pdf and kdpu.edu.ua/shramko/files/… – Bumble Aug 21 '16 at 8:46