Talk:Paraconsistent logic

Don't follow

"Now consider a valuation V\, such that V(A,1)\, and V(A,0)\, but it is not the case that V(B,0)\,. It is easy to check that this valuation constitutes a counterexample to both explosion and disjunctive syllogism." It really isn't that easy to check. It is not clear what the point is. I don't really see how the statement in question differs from FDE - it seems to accept that a formula can be both true and false, or, if it does not, what precisely does it entail? "A formula must be assigned at least one truth value, but there is no requirement that it be assigned at most one truth value." Does this not entail that LP is FDE? I find it quite unclear. Could you at least draw out how you relate the logical statement cited above to the disjunctive syllogism?

Thanks —Preceding unsigned comment added by 89.100.19.185 (talk) 13:50, 26 March 2010 (UTC)

2005 comments

The article seems to suggest that the liar doesn't "explode" in paraconsistent logics. that's not true for most PLs. Kim Stebel 23:57, 5 September 2005 (UTC)

What might we say about the choice between the man's utterance of "I am currently in the room" as opposed to its negation "I am not currently in the room" (1998)? Perhaps that the actual negation should be "It is not true that I am currently in the room". This is a false choice like that between "P is true" and "The negation of P is true": It could be that P is in fact unprovable, and the actual choice should be between "P is true" and "It is not the case that P is true". 203.116.59.23 13:55, 20 September 2005 (UTC)Joel Tay

Removed some content from the "Motivation" section

I removed some content from the "Motivation" section on the ground that it seemed to me not particularly well-written, and involved material that is (or ought to be) covered more thoroughly in Liar paradox and Dialetheism, both of which are prominently linked to. Feel free to integrate this material back into the article if you feel it would be an improvement. dbtfz^talk 05:47, 25 February 2006 (UTC)

Recent addition of material on direct logic

I removed the recently added content on "direct logic" since no evidence is provided indicating that it is more notable than any of the many other systems of paraconsistent logic that have been proposed over the years. We can't include all of them, so only a few of the most notable and important ones are discussed. (Remember: this article is aimed primarily at non-specialists.) For example, LP is discussed briefly in the article because it is easily the most influential and well-known paraconsistent logic. And dual-intuitionistic logic is discussed (very briefly) because it illustrates the relation of paraconsistent logic with another notable type of logic, intuitionistic logic. If someone wants to add a brief characterization of da Costa's C-systems, that would be appropriate.

Quite frankly, the addition of the material on direct logic looks like a blatant case of a researcher trying to promote his or her own work with little or no regard for whether the material is actually appropriate for the article. If anyone really believes that the material I removed should be in Wikipedia, I recommend creating a new article, Direct logic (cf. Relevance logic), which could be linked to from this article. Also, a very brief mention of direct logic in this article might be approprite, if done right. dbtfz^talk 18:40, 1 April 2006 (UTC)

• I removed the following:

Classical mathematical logic was devised for mathematical theories which are consistent and consequently make heavy use of the principle of indirect proof which can expressed formally as

$(B\vdash A,\lnot A)\vdash \lnot B$

which expresses the intuitive idea that if a contradiction follows from $B$, then $B$ must be false. The principle "from a contradiction, anything follows" can be derived from the principle of indirect proof. Some paraconsistent logics (such as Direct Logic) allow a more limited form of indirect proof called direct indirect proof which can be expressed formally as

$(B\vdash \lnot B)\vdash \lnot B$

which expressed the intuitive idea that if $B$ infers its own negation, then it cannot hold. Unlike full indirect proof, the principle of direct indirect proof can be used without causing explosion.

This section is basically out of synch with what the rest of the article says. It is also, I think, not quite correct. Ex contradictione quodlibet has as much to do with the rule of weakening as with reductio ad absurdum. Relevant logic rejects the rule of weakening, for instance. -Dan 14:31, 5 June 2006 (UTC)

Article lacks motivation for Ex contradictione quodlibet

The article currently lacks motivation for Ex contradictione quodlibet, so it proposed to add the following (which is the heart of the matter):

The above principle of "from a contradiction, anything follows" may not seem very intuitive. So why is it included in classical logic? Classical mathematical logic was devised for mathematical theories which are consistent and consequently make heavy use of the principle of indirect proof which can expressed formally as

$(B\vdash A,\lnot A)\vdash \lnot B$

which expresses that if a contradiction follows from $B$, then $B$ must be false which is reasonable for consistent theories.

The principle of indirect proof can be used to derive the principle that "from a contradiction anything follows" in the following way in classical logic:

$A,\lnot A\vdash (\lnot B\vdash A,\lnot A)\vdash \lnot \lnot B\vdash B$

Now if the above is added, then the article ought to also mention direct indirect proof as well because it is a closely related principle that does not cause explosion.

• Except it looks like the above derivation also makes use of the rule of weakening (and in fact double-negation elimination). Your paragraph makes it sound like indirect proof is the motivation for ex contradictione quodlibet, and the only way to avoid it is to reject or restrict indirect proof. This goes against what the rest of the article about disjunctive syllogism. I also think it is flat out wrong. Now I don't mind a brief mention of direct logic, but maybe we can do better than this? -Dan 20:58, 5 June 2006 (UTC)

• Of course, both weakening and double negation elimination are part of classical logic. The question being addressed is the motivation for including Ex contradictione quodlibet in classical logic. Indirect proof is certainly one of the most important motivations for Ex contradictione quodlibet.

• It turns out that rejecting (or restricting it as in Direct Logic) indirect proof by itself is not sufficient to prevent explosion. As the article points out, many paraconsistent logics (including Direct Logic) reject disjunction expansion as well. It turns out that restricting indirect proof and rejecting disjunction expansion is sufficient to prevent explosion. Imposing both of these seems to be one of the fundamental ideas behind Direct Logic.

• But it certainly can be improved!

Well, we'll have to leave this until we get some clarification on the system in question. If you haven't already, you might want to pop over to Talk:Direct logic. -Dan 15:09, 7 June 2006 (UTC)

Both weakening and double negation elimination produce explosion?

Why do you think that both weakening and double negation elimination produce explosion as stated in the article?

Oh. I really meant all three together. I hope it is better now. -Dan 20:34, 14 June 2006 (UTC)

How exactly is Paraconsistent Logic weaker?

The article says that paraconsistent logics deem fewer inferences valid, and rarely deem inferences valid that classical logic doesn't. I always thought that standard logics restricted themselves to making claims about inferences concerning statements whose atoms were true or false, but not both or neither, but that paraconsistent logics validate inferences over a far broader range of statements. That means they validate lots and lots of inferences about which standard logics say nothing one way or the other right? This means that the logical truths of LP are not "precisely those of classical propositional logic" because they include truths of the form p triple bar p, where p is an atom which is both true and false. This is a logical truth of LP, but it is not even in the domain of consideration for standard logic. By broadening the truth assignments we're are broadening the possible worlds under consideration, but that means we get to endorse truths about which we previously said nothing, even though we are endorsing them by using the same propositional variable we used before, right? Am I misunderstanding something? Bmorton3 18:05, 27 July 2006 (UTC)

In paraconsistent logics, one may use a set of inconsistent premises which would explode in classical logic without suffering such an explosion. So to allow more (inconsistent) assumptions, one is sacrificing some of the deductive power of classical logic. If one did not, then the explosion would occur and the theory would become trivial, i.e. every proposition would be a "theorem" in the theory. Is that clear? JRSpriggs 05:36, 28 July 2006 (UTC)

One way of looking at it is that propositions actually mean less than they seem to mean in paraconsistent logics. JRSpriggs 05:44, 28 July 2006 (UTC)

One is sacrificing some deductive power by giving up some inferences you could make in standard logic, in return for gaining deductive power of a different kind, being able to make inferences at all over domains you couldn't touch safely before. We are weaker in some ways but stronger in others. Even inferentially, we give up some inferences, but can also make inferences where previously we had to keep silent. We can cash out what we've given up in lots of different ways (and it often varies on our approach), maybe we weakened the power of adjunction, or of negation, like in the Polish or South American stuff. Maybe we weakened the conditional, like in the relevance stuff, or we weakened the assertion stroke by going non-monotonic and allowing retractions like in the Batens stuff. You could say we have weakened the meanings of the propositions (although even here, we weakened the meanings of one or more of the connectives, but in return bought ability to have broader meanings in our atoms!). You could say instead that we have retained the same meanings for the connectives but have changed our valuation system. In that case the propositions haven't changed their meaning at all, its just that the meaning of true and false has change. But on any other these we've weakened some things, but gained strength in others. It looks to me like Classicist POV to say that we have fewer inferences in a paraconsistent logic; classical logic endorses inferential formulae that paraconsistent logic does not, but paraconsistent logic in turn endorses application of inferential formulae to particular inferences that classical logic does not because of the domain changes (and not just a few, but lots). We have to weaken something to escape explosion, but that doesn't mean we wind up being overall weaker (even in the strictly inferential sense) at the end of the day. This is still an issue of trade-offs not of being "invariably weaker" Right? Am I being partisan here, or misunderstanding something? 'Cause I've almost convinced myself to demote the "invariably weaker" paragraph and integrate some of it into the trade-off stuff Bmorton3 13:35, 28 July 2006 (UTC)

I do not understand what extra power you think paraconsistent logics have (other than tolerating inconsistent assumptions, as I said). Please give a specific example of an inference which you could do in a paraconsistent logic which you could not do in classical logic. JRSpriggs 04:10, 29 July 2006 (UTC)

It includes atomic claims which are at once both true and false in its domain, which is forbidden by the valuation rules in a classical logic. See my example below. Bmorton3 16:42, 31 July 2006 (UTC)

The article as it stands reads:

It should be emphasized that paraconsistent logics are in general weaker than classical logic; that is, they deem fewer inferences valid...

So I think it is clear weaker is to be understood in a strictly technical sense. Classical logic does, in fact, allow you to work with incoherent assumptions, and it allows you to derive any conclusion. Now, in the above discussion, there seems to be some implication that classical logic does not make claims about what happens in these situations. Technically, it does! True, it might then be noticed that the classical conclusions are useless. But, this sort of judgement is not in itself a rule of classical logic. For one thing, it is not always obvious when assumptions are incoherent.

Classical logic makes claims about what happens when multiple formulae conflict with each other, but each is consistently evaluatable, like the explosion claims, (A&~A)horseshoe B. Both classical and paraconsistent logics deal with this claim. Part of the value of paraconsistent logic is the weakening of explosion. Classical logic does make claims about what happens when contradictory WFFs are conjoined, namely we get triviality. But it makes no claims about what happens when an ATOM is both true and false. In that sense, it does not allow one to work with incoherent assumptions. Part of the value of paraconsistent logics is the loosening of the restrictions on valuation. Consider some very basic inference, like &E, A&B therefore B. Classical logic endorses &E, only over A's and B's which are true or false but not both. Most paraconsistent logics will endorse it over A's and B's that are true, false or both (and some probably endorse it for the neither case as well). So consider the inference "This clause is false; and it is snowing outside, therefore it is snowing outside." Classical logic says nothing about this inference because the first clause isn't in it's domain of discourse. Paraconsistent logics endorse the inference. For each inference schema that classical logic endorses, and paraconsistent logic doesn't reject, we can create an inferential instance that paraconsistent logic will endorse, but classical logic will stay silent on by using an atom that is both true and false (if any such atoms exist). So if the dialethists are right, there are lots of inference instances that paraconsistent logics endorse, but classical logics stay silent on. Paraconsistent Logics are not weaker full stop, they are inferentially weaker in someways and stronger in others. Bmorton3 16:42, 31 July 2006 (UTC)

I think I see where you're coming from now. In the article, PL is presented in terms of semantics and not syntax. A paraconsistent system of logic will have a broader class of semantic models. But in fact, weaker inference rules should always result in a broader class of semantic models, and vice versa. Inferences are made with formulas though, not valuations. So, "This clause is false; and it is snowing outside, therefore it is snowing outside" is classically valid, assuming we expand it to allow self-reference in formulas. Of course allowing self-reference makes classical logic, and many systems of paraconsistent logic, explode. 192.75.48.150 17:23, 31 July 2006 (UTC)

PS: I also sense you might also find the word weaker derogatory in this context. But I'm pretty sure that even advocates of paraconsistent logic use it, exactly the way we are using it. 192.75.48.150 17:42, 31 July 2006 (UTC)

First, no, folk who study Paraconsistent logics use stronger and weaker in lots of different senses, but the main one seems to be the distinction between strong paraconsistency and weak paraconsistency. See Bremer 2005, chapter 1. The worry isn't that you're being derogatory, but that your making "strong" paraconsistency look less "strong" than classical logic, when it isn't. In this sense, classical logic is significantly weaker than weak paraconsistency. Strong paraconsistency is strong because it endorses claims about inferences in even very non-normal models (such as nes where contradictions are finally provable). Now you are right that there is a sense in which strong paraconsistency is inferentially weaker than classical, but that's not the main sense in which the terms strong and weak are used in paraconsistency, and even inferentially, there is a sense in which strong paraconsistent logics can make claims about inferences that classical cannot.

Second, inferences are not made with formulae or valuations, they are made with premises in language, but understanding how formulae link up with premises in a language is an issue of syntax and semantics working together. Formal formulae can be thought of in 2 distinct ways, as themselves being premises in a formal language, or as attempts to represent formally premises in an informal language. If you think of a formulae as simply being elements of the formal language alone, then its hard to make any claims about stronger and weaker, because every formal langauge is going to use its own set of abstract atoms, otherwise we could create WFFs with elements from multiple logical systems. Thus A&B therefore A, in classical logic and A&B therefore A in paraconsistent logic are incommensurable, because the A's and B's are elements of different languages and should really be written A(CL)&B(CL) therefore A(CL), and A(PL)&B(PL) therefore A(PL). If instead we look at A&B as stand-in's for elements of a natural language, then we can't divorce the syntax and semantics so quickly. The semantics is part of how we decide how to translate from the one langauge to the other.

Third, classical logic does not endorse the inference "This clause is false, and its snowing outside, therefore its snowing" for 2 distinct but relevant reasons. First, the clause is self-referential and there is no good way to represent that in any n-order logic, and there is no good way to "expand classical logic to allow self-reference in formulae" and this is a key motivation for paraconsisent logics. But second, if you attempt to run a valuation of a set of claims including these claims using the classical rules for valuation, the expression "this clause is false" cannot be evaluated "suitably" (and on most def's this will mean it can't even be represented with a WFF, and that will mean it CAN'T explode CL). Most, well structured classical logics treat "This clause is false, and its snowing outside" the same way tehy treat &&&A, as a non-WFF, and therefore trivial in the other sense (implying nothing). Removing inference schema does in general mean broadening the possible models, but this just IS a species of strengthening the inferences allowed; that's the heart of my "derogatory" worry, I guess, if we don't treat broading the range of statements that are allowed to be represented with WFFs as a form of increasing the inferences allowed, then the main point of most non-classical projects is lost.

Fourth, The fact that the syntax-semantics distinction just isn't that clear cut for natural languages is a huge part of the Dialethists agenda and motivation, See Bremer chapter 2, or Priest 1979.Bmorton3 19:24, 31 July 2006 (UTC)

Erm, hmmm. I don't have the book you cite at hand, but "weak" as an adverb, or adjective applied to a property of a formal system, as in "X is weakly P" and "X is strongly P" (or "X has weak P-ity" and "X has strong P-ity") is something quite different from when the adjective is applied directly as a comparative between formal systems ("X is weaker than Y"), where I think it is understood the way I've been saying. In the context of substructural logics, for instance, I don't think it's controversial to say that linear logic is weaker than system R which is weaker than classical logic. Despite the fact that conjunction "splits", which is what I think (but I'm not sure) that you are referring to in point 2, we can still make good sense of the statement. A web-acccessible example is Restall's relevant and substructural logics, where in section 2.1 he talks about Church's "weak implication", further down "Meredith and Prior were... looking for logics weaker than classical propositional logic...", in 2.2 "So, a logic of entailment must be weaker than R. However, it need not be too much weaker", and so on. He never defines what is meant, but it is perfectly clear, and Restall is hardly pushing a Classicist POV (his POV is succinctly declared in section 2.4.2). As to allowing self-reference, this may be a motivation for some, but certainly not system R, for instance. I did oversimplify with the syntax/semantics bit, and I hope I have not insulted your intelligence by doing so, but still when we're talking about what inference rules are valid or admissible in a formal system, we are saying something specific about its consequence relation. In this respect we are perfectly in accord with the practice in, say, set theory, where we can assert that CZF is weaker than ZF, in turn being weaker than ZFC. This assertion is not confusing or ambiguous, and does not offend constructivists in any way, notwithstanding the fact that obviously CZF would therefore have a broader class of models than ZF, in turn than ZFC (assuming ZFC is consistent, blah blah blah) 192.75.48.150 20:10, 2 August 2006 (UTC)

You're right about "X is weakly P," being different from "X is weaker than Y," and further "X is weaker than Y in respect R" is different from either. Er the web location you cite seems to be a citation record, but lack the actual article (or I couldn't find it), but you are certainly right that "x is weaker than Y" is a normal locution when comparing odd formal logics. Sigh. I guess I am failing to articulate my point, and it is probably too subtle for the purposes of WP anyway (or is wrong). There is a perfectly good mathematical logic sense in which everything you say is right, I just worry that it obscures a point in philosophical logic. CL must endorse sequent schema which any PL does not in order to escape explosion (although which ones can vary). If that is all we mean by "X is weaker than Y" everything is rosy. But a sequent isn't an inference. An inference in a pragmatic notion that requires claims being used in a particular way, and this kind of pragmatics has to have feet in syntax and semantics. PL endorses inferences that CL does not even though it does not endorse sequents that CL doesn't (or rarely does). If you say ZF is weaker than ZFC, we might just let it go as a summary, or we might say "in what sense?" If you say ZF is weaker than ZFC in that claims are provable in ZFC that are undecided in ZF, well right, but there are also claims about choice-less worlds which are expressible and provable in ZF, but inexpressible in ZFC, at least if a claim can be about a world or a model. There is a real sense in which ZFC is weaker than ZF, even though there is also a real sense in which ZF is weaker than ZFC. If you say ZF is weaker than ZFC in terms of the claims it makes, well yes and no. But we're just going in circles now, and I'm no longer convinced my point can contribute to this article, sigh. Bmorton3 21:09, 3 August 2006 (UTC)

Feel free to clarify if you like, but please don't demote it too much, because I think the point is important: paraconsistent logic works in the domains for which it is intended precisely because it is weaker. 192.75.48.150 15:46, 31 July 2006 (UTC)

PS doesn't the article give the "or" rules for PL twice rather than the or and the and rules? Bmorton3 16:42, 31 July 2006 (UTC)

I think it is correct. There are supposed to be two "or" and two "not" lines. "And" is to be defined in terms of these. 192.75.48.150 17:23, 31 July 2006 (UTC)

You're right, I miss understood what you meant by the "in other words" just after that, I thought you were going one to spell out how to do so, rather than re-stating the same point again. my error. Bmorton3 17:57, 31 July 2006 (UTC)

Some general remarks

I'm a rookie here, that's why I decided to comment on the article instead of changing it.

1) Stating that in Aristotle's wrtings one can find some ideas concerning inconsistency-tollerant logic is ambiguous. In my opinion this statement needs at least some justification (outlining the disscusion might be too much).

2) "Not all advocates of paraconsistent logic are dialetheists" i would say that only few of them are. The picture you get depends on the references. in the references section I saw many books/articles by the representees of Australian school of paraconsistency. :)

3) As far as I know, G. Priest has two affiliations -- the Univeristy of Melbourne and St. Andrews.

4) In my opinion LP is not the most well-known paraconsistent logic. What is the criterion? What about da Costa's C?

5) "One important type of paraconsistent logic is relevance logic". According to my references, those two classes overlap. And even if we assume that this is not the case, it is paraconsistent logic which is a subset of relevance logic and not the other way.

5) Notable Figures section. Why {\L}ukasiewicz? His {\L}_{3} is paraconsistent but this wasn't intended, so to say. Even if we agree that he should be mentioned, there are others who fulfill the same criterion and are not on the list: Orlov, Kolmogorov, Lewis. The view that Vasiliev system(s) is(are) paraconsistent is widely criticized. As a forerunner should count also Carnot, shouldn't he?

6) In my opinion, Resources as well as External links section should be extended. They are not representative.Glaukon 16:23, 9 September 2006 (UTC)

1) the cite is in {\L}ukasiewicz if you want to add it. This page isn't doing much in-line yet. 2) No one has stats, but its to prevent the common misconception that advocating PL requires Dialethism 3)sure, as it says on his page 4) fine re-phrase. 5) Pl and RL DO overlap, but there are PLs which are not RLs, and RLs which are not PLs, so neither is a subset of the other, nor is that implied by calling RL one type of PL. 6) Why do you think {\L}ukasiewicz didn't intend to be paraconsistent? He wrote about the priority of the law of syllogism and the law of non-contradiction in Aristotle, right? I don't know the details of Kolmogorov or Orlov, maybe they should be added, Lewis is a weird case, look at what Rescher and Brandom argue about him. Maybe add him, but also the Rescher and Brandom cite. 6) They are a bunch of the more recent stuff. Add more if you want. Be BOLD! Bmorton3 14:59, 11 September 2006 (UTC)

Two comments... In one year Priest will no longer be affiliated with Melbourne, but will be moving to the graduate faculty at CUNY (and maintain his affiliation with the Arche research center at St. Andrew's). Second, L3 is not paraconsistent. What is your source on this? Paraconsistent (talk) 10:31, 21 July 2008 (UTC)

OK, I'll became bold soon -- I just need to think how to put things in the most appropriate order. Now -- just a reply. 1) you mean his "On the Principle of Contradiction"? I thought that you are rather referring to G. Priest interpretation of Aristotle's standpoint. Anyway, that's a fishy subject. I'll check the references. 2) OK, but, as far as I know, most of paraconsistent logicians are not "happy" with contradictions. They just want to explore the subject, to invent a tool for dealing with it and eventually get rid of the contradictions (Brazilian, Polish, Flemish schools) -- most of them do not connect their works with any ontological convictions concerning contradictions. That's is why this passage should be rewritten -- it suggests that dialetheism is some leading option among p. logicians. 5) Right. But, again, the article says different things. 6) I said that his system was not intended as paraconsistent. It was Jaśkoski who showed that in Ł3 the explosion law is not valid. Again, I'll consult the original text, but I think that Łukasiewicz was merely criticizing the principle of contradiction and he was not stating that it should be invalidated. Anyway, I do consider him as a forerunner of paraconsistency but others that I've mentioned should also be put on the list. Unfortunately I don't know much about Rescher's work. All I know that Lewis' system of strict implication is paraconsistent (the law is not valid there). It was not intended (as in the case of Łukasiewicz).Glaukon 16:58, 11 September 2006 (UTC)

1)Lukasiewicz, J. "On the Principle of Contradiction in Aristotle" reprinted in Review of Metaphysics 24 (1971), 2) No one knows the "most" claim one way or the other. There are plenty in both camps. Lots of PL logicians are exploring it for reasons you mention, lots are exploring it for more dialetheist reasons. How many Jain paraconsistent logicians are there left in the Indian traditions? I've got no clue and neither do you. I would love to see more discussion of Indian, Brazilian, Polish, and Flemish styles, but was afraid that anything I wrote would be POV and OR to boot. 6)The cite I was thinking of was, Rescher, Nicholas and Brandom, Robert. The Logic of Inconsistency. New York: Basil Blackwell, 1980. C. I. Lewis' position on paraconsistency is not entirely unrelated to his pragmatism, according to Rescher and Brandom, if I recall correctly. Like Lukasiewicz, even if he wasn't quite aiming at PL, concerns relating to PL were guiding his thinking. I think the argument that either were not intended to be PL would be hard to make, better to remain agnostic on it, unless you have good evidence. Good luck! Bmorton3 19:38, 11 September 2006 (UTC)

The reason why I've asked for a rationale for the presence of Łukasiewicz on the list was that: "OK, I do agree that this guy contributed a lot and there are strong reasons for treating his ideas as some sort of anticipation of this what is happening within the modern paraconsistent movement, BUT if he is on the list, for the same reasons, there should be a bunch of other guys, and which were NOT there". About dialetheism. Of course there was no research on Plogicians' ontological convinctions. But this argument also applies to the statement that "Not all p. logicians are dialetheists" which implies that most of them are. I can say something about Polish school, and to some extent about Flemish and Brasilian ones. In Poland dialetheism does not win much attention. On a contrary. The same goes, I believe, for the Flemish and Brasilian approaches (this view is confirmed in Takanaka's paper -- Three Schools of Paraconsistency, it's avaliable online, as far as I know). You've mentioned Jaina's logicians. I do agree that this is an extemaly interesting subject and some historical background of paraconsistency is something which is missing in this article too.Glaukon 16:17, 12 September 2006 (UTC)

Eesh Not all P are D implies that most are? I would never have thought so, but certainly phrase it, "Some P are D, and some are not", if you prefer which is neutral and in line with availible data. Bmorton3 19:34, 12 September 2006 (UTC)

You're right when it goes about (classical;)) logic. But this is about rhetoric and some kind of impression. If I say "There are Microsoft operating systems which are unstable. Not all Microsoft operating systems are unstable." It depends on the context and many other parameters but one of possible interpretations is that I imply that most of those OSs are unstable, isn't it? All I'm saying is that an article should be reader-oriented and if there is a risk (commonsense assumed:)) of misunderstanding of some fragmet, an author should change it.Glaukon 08:17, 13 September 2006 (UTC)

Weakness

The second subsection has the headline "Paraconsistent logics are invariably weaker than classical logic" and starts with the sentence "It should be emphasized that paraconsistent logics are in general weaker than classical logic". I know nothing of paraconsistent logic, but these statements contradict each other. Perhaps a better headline would be "Paraconsistent logic vs Classical logic", or "The relative strengths of...". -Ashley Pomeroy 22:56, 9 April 2007 (UTC)

They say the same thing, no? Paraconsistent (talk) 10:28, 21 July 2008 (UTC)

General remark: The defining feature of paraconsistency

I would say that the defining feature of a paraconsistent logic should be inconsistency
tolerance and not the fact that it avoids explosion. There are some proof systems around able
to deal with certain inconsistent sets of premisses that do explode in the presence of a contradiction.
That is, they go beyond consistency in the sense that they can get relevant information
out of certain inconsistent knowledge bases and I do believe they deserve to be called paraconsistent systems
even though they cannot deal with contradictory premisses {of the form 'p', 'not p'}.
David--Davidpm888 (talk) 14:24, 25 November 2007 (UTC)

The definition in terms of the invalidity of explosion is simply, technically how paraconsistent logics are classified. See here (http://plato.stanford.edu/entries/logic-paraconsistent/) Paraconsistent (talk) 10:28, 21 July 2008 (UTC)

Weakness Again

I notice there has not been much discussion lately, so I am going to put this in a new section. On the topic of weakness, some folks had raised some prior complaints. For the most part these complaints are based on misunderstanding. However, there is a real problem with the formulation in the current article. It seems that in response to some worries about how 'weakness' was being interpreted, an addendum was created which states " a paraconsistent logic may validate nonpropositional inferences that are classically invalid... In this way a paraconsistent logic can prove more than classical logic." This is a possibly very misleading way to state the point. What people have in mind is the following phenomenon: given the resources of arithmetic and Godel's technique for arithmetization of syntax, we can define a coding over a formal language which allows sentences of that language to effectively ascribe predicates to the very sentences of that language. This produces something like the natural language phenomenon of 'self-reference' and is the reason why Godel sentences are possible which can roughly be paraphrased as equivalents of ordinary sentences like "I am false", that is we have formal counterparts of the Liar and other such paradoxical sentences. Because these sentences are intrinsically explosive, they cannot even be expressed in a language underwritten by classical logic and as Tarski concluded, this shows that a language underwritten by classical logic cannot contain its own truth (or falsity) predicate. What the paraconsistent language can do is precisely get around this problem. So to my mind, the most perspicuous way to contrast the power of a paraconsistent logic to its classical rival is to emphasis this issue: expressibility. I propose replacing "a paraconsistent logic can prove more than classical logic" with some talk about how language underwritten by paraconsistent logic have greater expressive strength than those underwritten by classical logic. I will make these changes in a few days if there are no objections. Paraconsistent (talk) 10:41, 21 July 2008 (UTC)

You might want to take a look at the following:

• Carl Hewitt. Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency in "Coordination, Organizations, Institutions, and Norms in Agent Systems III" edited by Jaime Sichman, Pablo Noriega, Julian Padget and Sascha Ossowski. Springer. 2008.

--67.169.145.74 (talk) 16:27, 21 July 2008 (UTC)

Could you maybe just summarize what you find to be important about this article?

-Paraconsistent (talk) 00:15, 22 July 2008 (UTC)

The article points out that Gödel stopped short in the following sense: in the context of unstratified reflection, his argument leads to an actual inconsistency in mathematics. (Of course, Gödel assumed stratified metatheories.) However, the other paradoxes are apparently blocked, e.g., Russell, Curry, Liar, Kleene-Rosser, etc. Also a generalization of Löb's theorem is proved.--67.169.145.74 (talk) 07:20, 22 July 2008 (UTC)

Okay so how does this bear on the current discussion?

-Paraconsistent (talk) 13:02, 22 July 2008 (UTC)

The section is even more misleading in that paraconsistency is motivated by tolerance of inconsistency, not necessarily by tolerance of self-reference. In fact I think the example systems on this page would all fall to paradoxical sentences, yet still quailfy as paraconsistent. --EmbraceParadox (talk) 16:11, 21 July 2008 (UTC)

Point taken, we could just remove the discussion of the 'strengths' of paraconsistent logic, as you say it not clear that self-reference is the most important issue in this respect.

-Paraconsistent (talk) 00:15, 22 July 2008 (UTC)

Incompleteness theorem

Set theory and the foundations of mathematics (see paraconsistent mathematics). Some believe that paraconsistent logic has significant ramifications with respect to the significance of Russell's paradox and Gödel's incompleteness theorems.

We're going to need details here, because I find this very difficult to believe, and the article on paraconsistent mathematics makes no such claim. The incompleteness theorem can be expressed without logic at all. --EmbraceParadox (talk) 16:22, 21 July 2008 (UTC)

There is a good discussion at this SEP article. The basic work on the usefulness of paraconsistent logic to formulations of naive set theory (set theory which can tolerate the existence of the Rusell Set amongst other things) and to Godel's Theorems has been done in the context of relevant logics. Look for work by Meyers and Brady for starters.

-Paraconsistent (talk) 00:18, 22 July 2008 (UTC)

The SEP article is unhelpful. It says

The heart of Gödel's theorem is, in fact, a paradox that concerns the sentence, G, ‘This sentence is not provable’ ... If an underlying paraconsistent logic is used to formalise the arithmetic, and the theory therefore allowed to be inconsistent, the Gödel sentence may well be provable in the theory ... So a paraconsistent approach to arithmetic overcomes the limitations of arithmetic that are supposed (by many) to follow from Gödel's theorem.

But as I say, the incompleteness theorem does not need logic. To make my point I think it will be enough to arithmetize the "not" in the Gödel sentence: "If this sentence is provable, then 0=1." If 0=1, then wouldn't all numbers be equal? x = 1*x = 0*x = 0 = 0*y = 1*y = y. This is arithmetic, and not logic, so it seems to me that paraconsistent logic will be of no help against 0=1. So how could a paraconsistent approach to arithmetic prove that Gödel sentence and not be trivial? --EmbraceParadox (talk) 15:07, 22 July 2008 (UTC)

Sorry you are right the SEP article is too short. I should have looked at it more closely. But you clearly see the thrust of the interest in paraconsistent arithmetic. Put it this way: the paradigm Godel sentence "this sentence is unprovable" can be proven in an inconsistent arithmetic underwritten by a paraconsistent logic without trivializing the theory. That is an interesting result, no? Your concern seems to be (if I follow) that paraconsistent arithmetic might still be faced with incompleteness even if it makes some advance over classical arithmetic. But I don't think I understand your example. The sentence "If this sentence is provable, then 0=1" should not be provable in any context, right? Even in an inconsistent-but-non-trivial arithemtic underwritten by paraconsistent logic, this sentence could simply be unprovable given that the consequent of the sentence is false. You seem to be suggesting that we want an arithmetic theory which proves this sentence as a theorem, but that strikes me as wrong. Am I missing something here?

-Paraconsistent (talk) 15:25, 22 July 2008 (UTC)

Good point. The inconsistency is that both of the following are provable: ├G and ¬├G. In paraconsistent logic, nothing particularly interesting follows from the inconsistency. Your particular example "If if this sentence is provable, then 0=1" is not admissible and consequently cannot be reflected.--67.169.145.142 (talk) 15:46, 22 July 2008 (UTC)

Leaving aside the above discussion, with respect to sources, I think it is easy enough to produce some. Who are the "some people" that believe paraconsistent logic is helpful for dealing with incompleteness? Amongst them are Meyer, Brady, and Priest. Here are some sources. Some of them are clearly 'revisionary' in light of standard mathematical practice, but if your interest was to find sources then here they are.

• Meyer, R. and Friedman, H. Whither Relevant Arithmetic? The Journal of Symbolic Logic, Vol. 57, (1992)
• Priest, G. Is Arithmetic Consistent? Mind, Vol. 103 (1994)

-Paraconsistent (talk) 15:53, 22 July 2008 (UTC)

I have trouble believing Harvey Friedman would say that. The abstract of the paper makes it sound like it is actually to show up some proof-theoretic deficiencies in R# (and that does sound like Harvey Friedman). The abstract refers to some theorem of PA not provable in R# (so it is incomplete), and that Ackermann's γ rule is not valid (From "A" and "B or not A", infer "B".) While it refers to effective proof of consistency of R#, it does not claim that this proof can be formalised within R#. It extends this to "R##" by ω-rule, which is not effective. It asks if there is some effective axiomatisation, but I assume it does not answer this. If there is something important not found in the abstract, could you please quote it?

But you are right to doubt "if this sentence is provable, then 0=1" is true, especially if "if..then" is read as a relevant conditional (or as "├"). Sorry if this is getting complicated. I claim for any formal system that can express arithmetic, I can number its possible sentences and proofs, and that I have an arithmetic formula with two arguments, Bew(x,y), and that this formula will take on the value 1 if x is the number of a valid proof, in that formal system, of the sentence whose number is y, and 0 if not. I also claim there is a certain number G for which sentence number G is exactly "Bew(x, G) = 0" in the system (x is a free variable, G is a numerical constant). Suppose Bew(666,G) = 1, that is, 666 is the number of a valid proof of sentence number G, which is actualy "Bew(x,G) = 0". But there should also be a valid proof of "Bew(666,G) = 1" (or else it's incomplete), so it must prove "0 = 1", so the system is trivial. (Let me make this bit clear: this does not follow from the law of non-contradiction or reductio ad absurdam or what have you - rather, we prove that Bew(666,G) is equal to both 0 and 1, therefore they are equal to each other. We don't really care that we don't have two-valued logic, we just ignore the formal system's negation and conditional connectives altogether, and we use 0 and 1 explicitly.) The argument can be reversed so if the system is nontrivial then Bew(666,G) = 0. But 666 was arbitrary, so we, on the outside, see that Bew(x,G) = 0 (x a free variable). So we can see that sentence number G expressed something that was actually true. I hope this is readable, and that I haven't skipped over anything important.

Now, I'm not really sure what Graham Priest's paper is saying. I suppose I can believe that he believes it does something, but I wish I had more details. --EmbraceParadox (talk) 21:07, 22 July 2008 (UTC)

This is getting a little crazy, but I'll bite. First, the easy part. After a quick perusal I find that the Priest paper is likely the place you want to look on this particular issue. He proves the existence of paraconsistent models for inconsistent, but complete arithmetic. These models unsurprisingly involve a least inconsistent natural number which is its own successor. I didn't look closely at the proofs, but there is a discussion of Godel and Hilbert in that paper, so that would definitely be the place to look given your abiding question. Second, on your example, I still don't see it. You've got that (for example) 666 codes the sentence "Bew(x,G)=0" and you've got (by hypothesis of completeness) that "Bew(666,G)=1" is provable. You claim that this delivers the provability of "0=1". How? For one thing, "Bew(x,G)" is not the same expression as "Bew(666,G)". I might just be missing something, but I don't get it.

-Paraconsistent (talk) 23:25, 22 July 2008 (UTC)

Come to think of it, an open sentence like "Bew(x,G)=0" shouldn't be provable, right?

-Paraconsistent (talk) 00:07, 23 July 2008 (UTC)

Why can't I prove open sentences? Isn't "x+y = y+x" a true equation, provable in just about any formalisation of arithmetic? From that can we not go to "666+y = y+666" and "666+G = G+666" ? Bew is just a binary operation of arithmetic, like addition, but much more complicated.

Or, I suppose we can use only closed sentences if we have universal quantifiers. G' can code for "for all x, Bew(x,G')=0". If 666 codes for a valid proof of G', then "Bew(666,G')=1" and "for all x, Bew(x,G')=0", so "0=1". Or, if we don't have open sentences and we have no universal quantifiers, then how do we make general statements at all?

Unless Priest's point is that I cannot make this substitution for some reason? (I guess I just need to shut up and dig up the paper, right?) --EmbraceParadox (talk) 02:49, 23 July 2008 (UTC)

I wasn't really trying to argue anything that Priest says, like I say I haven't read his whole article myself. I was just arguing that I don't see what substitution you are even making in the first place. Binding with the universal quantifier makes sense and I can see that was the intention of your original formulation of your Godel sentence. But what are you substituting to get "0=1" as a theorem? I just don't follow that part of your argument at all.

-Paraconsistent (talk) 03:29, 23 July 2008 (UTC)

Oh!! Sorry. It's just symmetry/transitivity of equality. If two things are equal to a third, they are equal to each other. So from "Bew(x,G) = 0" I get "Bew(666,G) = 0"; from "Bew(666,G) = 0" and "Bew(666,G) = 1" I get "0 = 1". Not controversial I hope. --EmbraceParadox (talk) 04:44, 23 July 2008 (UTC)

Wow I knew it was going to be something dumb that I was missing. I realized you were trying to use the symmetry/transitivty of equality, what I could not for the life of me figure out was how you got "Bew(666,G) = 0". But this should have been obvious: it is just universal instantiation. Okay for the moment I have to rest my objections. I buy your argument. Makes me wonder about the Priest paper now.

-Paraconsistent (talk) 11:06, 23 July 2008 (UTC)

Language v. Theory

For some reason someone felt a need to change the language I had used in clarifying the expressive 'strengths' of paraconsistent logics, but the change makes no sense to me. This section of the article is meant as a commentary or qualification on the proof-theoretic weakness of paraconsistent logic relative to classical logic. This weakness makes paraconsistent logics somewhat conservative. Let me first quote my prose:

It is due to such conservativeness that paraconsistent languages can be more expressive than their classical counterparts. For example, Tarski's undefinability theorem shows that a truth predicate cannot be expressed in the language of arithmetic underwritten by classical logic. This expressive limitation can be overcome in paraconsistent arithmetic.

And here is the change made a day later:

It is due to such conservativeness that paraconsistent languages can be more expressive than their classical counterparts including the hierarchy of meta-theories due to Tarski et. al. According to Feferman [1984]: “…natural language abounds with directly or indirectly self-referential yet apparently harmless expressions—all of which are excluded from the Tarskian framework.” This expressive limitation can be overcome in paraconsistent logic.

I say this ammendation makes no sense because it is formal languages which can be more or less expressive, not theories. While it may be true that a paraconsistent semantic theory has some advantages over the Tarskian heirarchical semantics, that is a largely philosophical question. On the other hand it is relatively straightforward to prove that a language underwritten by paraconsistent logic can contain its own truth predicate (its just an extension of Kripke's technique for inductively defining the extension of the truth predicate). I think my original prose is more to the point, not to mention that it makes sense -- theories can't be more or less expressive than each other. I'll change it back unless anyone sees reason to keep the new prose or something like it.

-Paraconsistent (talk) 23:15, 25 July 2008 (UTC)

Feferman is a highly respected authority. So his published views cannot be so easily dismissed. The current wording of the article says that the expressive limitation referenced by Feferman can be overcome by paraconsistency. Thus it doesn't take a position either way on your thesis that "it is formal 'languages' which can be more or less expressive, not theories."

Furthermore, it's not clear that "truth" makes sense for all paraconsistent logics. So hanging everything on a truth predicate is probably not appropriate. --67.169.145.142 (talk) 10:03, 26 July 2008 (UTC)

Forget it, I don't even feel like debating the issue. If everyone likes the current prose keep it.

-Paraconsistent (talk) 13:15, 26 July 2008 (UTC)

Don't be discouraged. The current version of the article is not perfect. However, improving it is hard.

For example, the status of "truth" in paraconsistent logic is subtle and controversial:

Frege suggested that, in a logically perfect language, the word ‘true’ would not appear! According to McGee [2006], he argued that “when we say that it is true that seawater is salty, we don’t add anything to what we say when we say simply that seawater is salty, so the notion of truth, in spite of being the central notion of [classical] logic, is a singularly ineffectual notion. It is surprising that we would have occasion to use such an impotent notion, nevermind that we would regard it as valuable and important."

--67.169.145.142 (talk) 17:52, 26 July 2008 (UTC)

I've made a minor change which suffices to address my worries without requiring any substantive alteration of the prose. The issue which I was getting at and which this prose is getting at are basically the same issue, it just seems to be a round about way of getting at it to talk about the Tarskian hierarchy at all. After all, the Tarskian hierarchy comes about as Tarski's solution to the apparent puzzle raised by his undefinability theorem which, in my original prose, was the locus of the discussion. But I digress. As to the minor change I've made: rather than talk of Tarski's semantic theory I've changed the term "meta-theories" to say "metalanguages". This keeps the section all in the same spirit of talk about the expressiveness of languages, broadly conceived. -Paraconsistent (talk) 03:31, 27 July 2008 (UTC)

Quote

Some rapper once said something like, "my soul is large, there is space for many contradictions" -- anyone know what this was? It's a nice quote to introduce this kind of topic! —Preceding unsigned comment added by 143.167.74.60 (talk) 16:36, 31 July 2008 (UTC)

Sorry, I don't know, and it's not suitable for Wikipedia anyway. Articles must be bland and colourless.

Wikipedia, the hobgoblin of small minds since 2001. (TM) --EmbraceParadox (talk) 18:22, 31 July 2008 (UTC)

haha, not a rapper, it was Walt Whitman.

"Do I contradict myself? Very well, then, I contradict myself. I am large, I contain multitudes." -- Walt Whitman, Song of Myself

-Paraconsistent (talk) 20:55, 2 August 2008 (UTC)

Applications

A friend of mine once showed a book about Paraconsistent logic, where the listed applications were not math-related. He was a psychologist, and he specifically wanted to study Paraconsistent logic to understand the reasoning of psychopaths - one of its applications. Other applications were the analysis of marketing, politics and religion :-) Albmont (talk) 19:56, 11 December 2008 (UTC)

Prof. Hewitt, while I am waiting for Hewitt et.al. 2015 to arrive, I was trying out Gardenfors' idea to use topological reasoning, rather than restricting our concepts to logical reasoning --(formulation due to Norman Foo 1994). My vehicle is market failure. In particular, the segmentation by economists to rivalrous vs. nonrivalrous goods in one dimension, and to exclusive vs. nonexclusive goods in another dimension. The segmentation is logical, but Foo teaches us that there is something overlooked in this economic formulation (Foo 1994 figures 3 and 4). That something is to be determined, as far as I know. Following Foo 1994, if we examine the convexity of the concepts in market failure, we can see that the concepts hinge not only on human wants, but also on their utility. Thus market failure is not a universal, stable condition, but rather a time and situation-dependent condition. The domain of definition for market failure is not just economic, but also political, psychological, and social. It appears that the very names of the things I am seeking are currently to be determined. Might this search for domains of definition be an interest of yours? I can see how the robustness of the domains of definition might qualify as an interest of yours. --Ancheta Wis   (talk | contribs) 08:08, 10 September 2016 (UTC)

Paraconsistency is too weak for inconsistency tolerant logic

Carl Hewitt has objected that paraconsistency (defined as inconsistency does not infer every proposition) is far to weak a criteria for inconsistency tolerant logic.. For example, adding the following rule (which is not incosistency tolerant):

For all propositions p: p,¬p⊢GreenCheese[Moon]

preserves paraconsistency because not all propositions are inferred from an inconsistency.

• Hewitt, Carl (2008b). "Common sense for concurrency and inconsistency tolerance using Direct Logic^TM and the Actor model".{{cite web}}: CS1 maint: numeric names: authors list (link) ArXiv. 0812.4852.

Below is a suggestion how to the following section more accurate and authoritative.

Carl (talk) 14:14, 26 August 2016 (UTC)

I have copied over the prose changes into the tradeoffs section, although not the reference to your article, as I am not sure whether the the philosophy literature would be a better source for that section. I have added your paper to the "examples" section, because software engineering seems to me to be an application of paraconsistent logic rather than the main subject. Of course, other people can also edit the article. — Carl (CBM · talk) 15:33, 26 August 2016 (UTC)

Thanks. I cleaned up the remainder of the section since I don't have a conflict because it is not my work. Please make improvements.

The correct reference for the applications section is the following:

Carl Hewitt. Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic Reasoning and the Actor Model. in Vol. 52 of Studies in Logic. College Publications. ISBN-10: ISBN 1848901593. 2015.

Carl (talk) 17:14, 26 August 2016 (UTC)

Hi there. The changes in question seem to have been implemented, as per the comment above. Please note that, while citing yourself should be discussed on the talk page (as you have done), it is not necessary to place the edit request template, unless no other editors are working on the article. Regards, VB00 (talk) 11:49, 1 January 2017 (UTC)

Tradeoffs

Paraconsistency involves tradeoffs. In particular, abandoning the principle of explosion requires one to abandon at least one of the following three principles:

Disjunction introduction	$A\vdash A\lor B$
Disjunctive syllogism	$A\lor B,\neg A\vdash B$
Transitivity of Inference	If $A\vdash B$ and $B\vdash C$, then $A\vdash C$

Each of these principles has been challenged.

One approach is to reject disjunction introduction but keep disjunctive syllogism and transitivity. In this approach, rules of natural deduction hold, except for disjunction introduction and excluded middle; moreover, inference A⊢B does not mean necessarily mean entailment A⇒B. Also, the following usual Boolean properties hold: double negation as well as associativity, commutativity, distributivity, De Morgan, and idempotence inferences (for conjunction and disjunction). Furthermore, inconsistency-robust proof by contradiction holds for entailment (A⇒(B∧¬B))⊢¬B. Carl Hewitt favours this approach, claiming that having the usual Boolean inferences, Natural deduction, Double negation elimination, Weakening for inference (If ⊢A, then B⊢A), and inconsistency robust Proof by Contradiction are huge advantages in software engineering.

Another approach is to reject disjunctive syllogism. From the perspective of dialetheism, it makes perfect sense that disjunctive syllogism should fail. The idea behind this syllogism is that, if ¬ A, then A is excluded and B can be inferred from A ∨ B. However, if A may hold as well as ¬ A, then the argument for the inference is weakened.

Yet another approach is to do both simultaneously. In many systems of relevant logic, as well as linear logic, there are two separate disjunctive connectives. One allows disjunction introduction, and one allows disjunctive syllogism. Of course, this has the disadvantages entailed by separate disjunctive connectives including confusion between them and complexity in relating them.

The three principles below, when taken together, also entail explosion, so at least one must be abandoned:

Reductio ad absurdum	$A\to (B\wedge \neg B)\vdash \neg A$
Weakening for implication	$A\vdash B\to A$
Double negation elimination	$\neg \neg A\vdash A$

Both reductio ad absurdum and the rule of weakening have been challenged in this respect, but without much success. Double negation elimination is challenged, but for unrelated reasons. By removing it alone, while upholding the other two one may still be able to prove all negative propositions from a contradiction. — Preceding unsigned comment added by Prof. Carl Hewitt (talk • contribs) 20:53, 24 August 2016 (UTC)

References

I think there is a typo

Shouldn't the line that reads "Furthermore, inconsistency-robust proof by contradiction holds for entailment (A⇒(B∧¬B))⊢¬B." be "(A⇒(B∧¬B))⊢¬A"? — Preceding unsigned comment added by 2601:602:200:DD1D:45C:20C:ECA5:624B (talk) 02:33, 19 February 2017 (UTC)

Outline of completeness proof and needed axiom schemas

Regarding the system of Paraconsistent logic#An ideal three-valued paraconsistent logic, it appears to me that it should be possible to select 35 or fewer axiom schemas (the axioms being tautologies of paraconsistent logic) from which one could prove (using modus ponens) any tautology of paraconsistent logic (and not prove any other formulas). Given propositions P and F, one can define what it means for P to be t (true only, not-false), b (both true and false, not-sharp), or f (false only, not-true) as follows:

$\lnot P\to F$ is true (t or b) iff either P is t or F is true;

$((P\land \lnot P)\to F)\to F$ is true iff either P is b or F is true; and

$P\to F$ is true iff either P is f or F is true.

See implicational propositional calculus#Completeness for an example of how a completeness proof works for a much simpler system. As in that case, two axiom schemas would be used here to get the deduction theorem.

The completeness proof would follow the process by which one evaluates whether a formula F is a tautology. For each valuation, one calculates (by induction on the length of subformulas) the value of each subformula. For example, when P is t and Q is b so that P→Q is b, we would need a theorem of the form

$(\lnot P\to F)\to ((((Q\land \lnot Q)\to F)\to F)\to ((((P\to Q)\land \lnot (P\to Q))\to F)\to F))$.

This might require upto 3 (for negation) plus 9 (for implication) plus 9 (for disjunction) plus 9 (for conjunction) axiom schemas (3+9+9+9=30).

After one finishes that induction reaching the full formula F, we should have one of the following for each valuation:

$\lnot F\to F$ if the value of F is t for this valuation;

$((F\land \lnot F)\to F)\to F$ if the value of F is b for this valuation; or

$F\to F$ if the value of F is f for this valuation.

If F is indeed a tautology, then we should be in either the first or second case (not the third case). So now we need two more axiom schemas:

$(\lnot F\to F)\to F$; and

$(((F\land \lnot F)\to F)\to F)\to F$.

At this point we should have that F can be deduced from a sequence of hypotheses describing the valuation. Now we do a backward induction to remove the hypotheses by combining the different cases. If P is one of the propositional variables in F, then we would use the deduction theorem to remove it from the left side of the sequents and put it on the right side as an hypothesis.

$(\lnot P\to F)\to F$;

$(((P\land \lnot P)\to F)\to F)\to F$; and

$(P\to F)\to F$.

So now we use one axiom schema of the form:

$((\lnot P\to F)\to F)\to (((((P\land \lnot P)\to F)\to F)\to F)\to (((P\to F)\to F)\to F))$.

This then gives us that F can be deduced from a shorted valuation which excludes P. When this downward induction is finished, we will have an unconditional proof of F alone.

So we might (in the worst case) need 2 (for deduction) plus 30 (for construction) plus two (for getting F itself) plus one (for removing hypotheses). Total axiom schemas needed 2+30+2+1=35. JRSpriggs (talk) 04:27, 29 August 2018 (UTC)

Although all those 35 axiom schemas are tautologies of paraconsistent logic, they are not especially convenient as axioms. They are non-intuitive and mostly too specialized to be useful for general proofs. So we should try to replace them with shorter more general and intuitive axioms. For example, instead of using

$(((F\land \lnot F)\to F)\to F)\to F$

to go from

$((F\land \lnot F)\to F)\to F$

to F, we could use conjunction elimination

$(P\land Q)\to P$

to get

$(F\land \lnot F)\to F$

and then apply

$((F\land \lnot F)\to F)\to F$

to that to get F. Also instead of having three axiom schemas to get from an hypothesis being f to the implication being t, we could use just one

$(P\to F)\to (\lnot (P\to Q)\to F)$.

Or we could go even further and use

$\lnot (P\to Q)\to P$

followed by

$(P\to Q)\to ((Q\to R)\to (P\to R))$ (from the deduction theorem).

JRSpriggs (talk) 01:29, 30 August 2018 (UTC)

I was able to reduce it to twenty (20) axiom schemas which I listed at Paraconsistent logic#Included. Most of them are simpler (and thus potentially more useful) than they might have been. JRSpriggs (talk) 02:00, 31 August 2018 (UTC)

Illustrating the use of the axiom schemas by proving selected theorems

• to prove $(\lnot P\to P)\to P$

$(P\to ((Q\to P)\to P))\to ((P\to (Q\to P))\to (P\to P))$ axiom 2

$P\to ((Q\to P)\to P)$ axiom 1

$(P\to (Q\to P))\to (P\to P)$ modus ponens

$P\to (Q\to P)$ axiom 1

$P\to P$ modus ponens

$(P\to P)\to ((\lnot P\to P)\to P)$ axiom 20

$(\lnot P\to P)\to P$ modus ponens QED

• to prove $((P\to Q)\to P)\to P$ Peirce's law

$\lnot (P\to Q)\to P$ axiom 3

$(P\to Q)\to P$ hypothesis

$((P\to Q)\to P)\to ((\lnot (P\to Q)\to P)\to P)$ axiom 20

$(\lnot (P\to Q)\to P)\to P$ modus ponens

$P$ modus ponens

$((P\to Q)\to P)\to P$ deduction QED

• to prove $P\lor \lnot P$ the law of excluded middle

$(P\to (P\lor \lnot P))\to (((\lnot P\to (P\lor \lnot P))\to (P\lor \lnot P))$ axiom 20

$P\to (P\lor \lnot P)$ axiom 8

$(\lnot P\to (P\lor \lnot P))\to (P\lor \lnot P)$ modus ponens

$\lnot P\to (P\lor \lnot P)$ axiom 9

$P\lor \lnot P$ modus ponens QED

• to prove $\lnot (P\land \lnot P)$ the law of noncontradiction

$(\lnot P\to \lnot (P\land \lnot P))\to ((\lnot \lnot P\to \lnot (P\land \lnot P))\to \lnot (P\land \lnot P))$ axiom 20

$\lnot P\to \lnot (P\land \lnot P)$ axiom 16

$(\lnot \lnot P\to \lnot (P\land \lnot P))\to \lnot (P\land \lnot P)$ modus ponens

$\lnot \lnot P\to \lnot (P\land \lnot P)$ axiom 17

$\lnot (P\land \lnot P)$ modus ponens QED

• to prove $(\lnot P\to Q)\to (P\lor Q)$ the converse of disjunctive syllogism

$(P\to (P\lor Q))\to ((\lnot P\to (P\lor Q))\to (P\lor Q))$ axiom 20

$P\to (P\lor Q)$ axiom 8

$(\lnot P\to (P\lor Q))\to (P\lor Q)$ modus ponens

$\lnot P\to Q$ hypothesis

$Q\to (P\lor Q)$ axiom 9

$\lnot P$ hypothesis

$Q$ modus ponens

$P\lor Q$ modus ponens

$\lnot P\to (P\lor Q)$ deduction

$P\lor Q$ modus ponens

$(\lnot P\to Q)\to (P\lor Q)$ deduction QED

When and how paraconsistent logic might be used

Suppose we are given a question in the form "Given data Γ, does condition Δ hold?" where Γ and Δ maybe compound propositions composed from atomic propositions using the logical connectives not, implies, or, and and.

In classical logic, we might proceed by testing whether Γ→Δ is a tautology (of classical logic) and whether Γ→~Δ is a tautology. If neither is a tautology, then there is insufficient data. If Γ→Δ is a tautology and Γ→~Δ is not, then the answer is yes. If Γ→Δ is not a tautology but Γ→~Δ is, then the answer is no. If both are tautologies, then the data is inconsistent and no conclusion can be drawn unless the data is modified (perhaps by deleting some parts).

If we have paraconsistent logic available, then we could re-evaluate the inconsistent case by asking the same questions with respect to tautologies of paraconsistent logic. If neither is a tautology of paraconsistent logic, then there is insufficient relevant data. If Γ→Δ is a tautology and Γ→~Δ is not, then the answer is yes. If Γ→Δ is not a tautology but Γ→~Δ is, then the answer is no. If both are tautologies of paraconsistent logic, then even the relevant data is inconsistent and we are still stumped. JRSpriggs (talk) 05:38, 9 September 2018 (UTC)

Translation of classical logic into paraconsistent logic

See Double-negation translation. Following this idea to translate classical logic into paraconsisent logic will show that paraconsistent logic's expressive power is not fundamentally inferior to that of classical logic. Reserve a propositional atom p₀ to play the role of falsity. Then the translation is done as follows:

• Any propositional atom p_n for n ≥ 1 will be translated as (p_n → p₀) → p₀ which is classically equivalent to p_n v p₀.
• If P is any proposition of classical logic whose translation is Q, then the translation of ~P is Q → p₀ which is classically equivalent to ~P v p₀.
• If P translates to Q and R translates to S, then P → R translates to Q → S which is classically equivalent to (P → R) v p₀. [From this we get that modus ponens carries over to the translated formulas.]
• If P translates to Q and R translates to S, then P v R translates to Q v S which is classically equivalent to (P v R) v p₀.
• If P translates to Q and R translates to S, then P & R translates to Q & S which is classically equivalent to (P & R) v p₀.

Then if P (which does not contain p₀) translates to Q, P will be a tautology of classical logic if and only if Q is a tautology of paraconsistent logic. If p₀ has the value t or b, then the translation of any subformula of P will also have either the value t or b regardless of what the valuation does to the other propositional atoms. If p₀ has the value f, then the translation of any subformula of P will have either the value t or f and that value will be the same as the classical value of the (untranslated) subformula under the valuation which results by collapsing b into t.

What makes this work is that we have avoided having "~" in the translation. If p₀ has the value t, then t → t = t which is fine whereas ~t = f which would screw things up since this case is supposed to always have the value t and thus not affect whether the translation is a tautology or not. JRSpriggs (talk) 05:36, 14 September 2018 (UTC)

Another translation leaves the propositional atoms unchanged, adding a disjunction with p₀ on the outside instead. For example,

$(\lnot P\to \lnot Q)\to (Q\to P)$

is a classical tautology, but not a paraconsistent tautology. It could be translated to

$(((P\to R)\to (Q\to R))\to (Q\to P))\lor R$

which is both a classical tautology and a paraconsistent tautology (generalizing here from p₀ to R). To see that modus ponens carries over for this version of translation, we need

$((P\to Q)\lor R)\to ((P\lor R)\to (Q\lor R))$

to be a paraconsistent tautology which it is. JRSpriggs (talk) 20:37, 14 September 2018 (UTC)

Variations on the connectives

Disjunctive syllogism fails since the classical tautology

$(\lnot P\land (P\lor Q))\to Q$

is not a paraconsistent tautology. This occurs even though

$P=f$ and $Q=t$

is the obvious solution of the left-hand side in classical logic with no explosion occurring.

This suggests that perhaps a stronger version of disjunction should be used. We could define "strong disjunction" as

$(P\lor _{s}Q)=((\lnot P\to Q)\land (\lnot Q\to P))$.

This differs from the original disjunction in that

$(b\lor _{s}f)=(f\lor _{s}b)=f$ rather than $(b\lor f)=(f\lor b)=b$.

If the classical disjunction is translated this way, then disjunctive syllogism would work because

$(\lnot P\land (P\lor _{s}Q))\to Q$

is a paraconsistent tautology. However, this comes at a cost since

$P\to (P\lor _{s}Q)$ and $Q\to (P\lor _{s}Q)$

would not be paraconsistent tautologies.

It is also possible to define "weak disjunction" by

$(P\lor _{w}Q)=(P\lor Q\lor \lnot (P\to Q)\lor \lnot (Q\to P))$

$(b\lor _{w}f)=(f\lor _{w}b)=t$

although I find it hard to imagine a use for this.

Similarly, "strong conjunction" is

$(P\land _{s}Q)=(P\land Q\land (\lnot P\to \lnot Q)\land (\lnot Q\to \lnot P))$

$(b\land _{s}t)=(t\land _{s}b)=f$.

And "weak conjunction" is

$(P\land _{w}Q)=(\lnot (P\to \lnot Q)\lor \lnot (Q\to \lnot P))$

$(b\land _{w}t)=(t\land _{w}b)=t$.

One could define "strong implication" as

$(P\to _{s}Q)=((P\to Q)\land (\lnot Q\to \lnot P))$

$(t\to _{s}b)=f$.

This would restore contrapositive, but at the cost of losing the deduction metatheorem (or making it more complicated since you would have to prove both directions).

A "weak implication" might be

$(P\to _{w}Q)=((\lnot P)\lor Q)$

$(b\to _{w}f)=b$.

which would fail to satisfy modus ponens. Or one could go even further and define "very weak implication" as

$(P\to _{ww}Q)=((\lnot P)\lor _{w}Q)$

$(t\to _{ww}b)=(b\to _{ww}f)=t$.

Although, once again I cannot imagine what use they might be. JRSpriggs (talk) 01:02, 25 September 2018 (UTC)

By induction, we can define the strongest (most often f) reasonable interpretation of a classical formula and the weakest (most often t) reasonable interpretation as follows:

$S(p_{k})=W(p_{k})=p_{k}$ atoms are unchanged

$S(\lnot P)=\lnot W(P)$

$W(\lnot P)=\lnot S(P)$

$S(P\to Q)=(W(P))\to _{s}(S(Q))$

$W(P\to Q)=(S(P))\to _{ww}(W(Q))$

$S(P\lor Q)=S(P)\lor _{s}S(Q)$

$W(P\lor Q)=W(P)\lor _{w}W(Q)$

$S(P\land Q)=S(P)\land _{s}S(Q)$

$W(P\land Q)=W(P)\land _{w}W(Q)$.

Conjecture: If $\lnot \Gamma$ is not a classical tautology (that is, Γ is not a contradiction) and $\Gamma \to \Delta$ is a classical tautology, then

$S(\Gamma )\to W(\Delta )$

is a paraconsistent tautology. JRSpriggs (talk) 18:44, 26 September 2018 (UTC)

Need a plain English example - Badly

This article is not helpful to the average user who is not schooled in Logic symbols. We should give an example, or a couple of examples, in plain English without the use of symbols. Ileanadu (talk) 16:59, 1 November 2018 (UTC)

The feature of classical logic which supporters of paraconsistent logic are trying to avoid could be illustrated by "You do not have a pet dog. If you have a pet dog, then the Moon is made of green cheese.". JRSpriggs (talk) 17:48, 1 November 2018 (UTC)

The point is that from a false statement (such as a contradiction), one can (in classical logic) deduce anything including statements which are irrelevant and absurd. Some people are uncomfortable with this, especially if they want to be able to entertain contradictions, so they invented paraconsistent logic to get around it. JRSpriggs (talk) 19:00, 2 November 2018 (UTC)

Clarification

The first line of this article seems contradictory, at least if you see it in this way: A paraconsistent logic cannot be a subfield of logic that tolerates contradictions but at the same time deals with them in a "discriminating way". Orther it tolerates them or discrminates them. I think your first sentence should say, "a non-discriminating way" instead.

A typo?

In the implication table ($P\Rightarrow Q$) in the section https://wiki.riteme.site/wiki/Paraconsistent_logic#An_ideal_three-valued_paraconsistent_logic, shouldn't the $b\Rightarrow f$ cell be $b$? Isn't it the case: $(V(P,0){\text{ and }}V(P,1))\Rightarrow V(Q,0)\quad \Leftrightarrow \quad (V(P,0)\Rightarrow V(Q,0)){\text{ and }}(V(P,1)\Rightarrow V(Q,0))$ Sofviic (talk) 19:25, 11 November 2021 (UTC)

No. If you read the subsection on Paraconsistent logic#Strategy, you will see why it has to be what it is. You are implicitly assuming a certain relationship between classical logic and paraconsistent logic. But that assumption renders paraconsistent logic virtually useless. JRSpriggs (talk) 23:31, 11 November 2021 (UTC)

Ah! I see that now. Should we add a small caption near to the table that says something similar to "$b\Rightarrow f$ has to evaluate to $f$; explained further down in Paraconsistent logic#Strategy"?

If you do, then please put it in a comment which can only be read by those editing the article. Otherwise you are cluttering up the section to cater to people who might otherwise give it an erroneous interpretation. JRSpriggs (talk) 23:07, 12 November 2021 (UTC)