>>11281620>but is strictly weaker than classical logicYou may put it like that. However, it should be highlighted what "weaker" ought to mean here.
Namely, for every classically provable proposition, there is an intuitionistically provable statement, which is classically equivalent to it.
E.g. non-contradiction ¬(P?¬P) is constructively provable, as in
>>11280499. And, for any P, classically equivalent to P?¬P (LEM).
All classical statements have a proof of a statement that is constructive, until the very last step:
E.g. if P is any statement in propositional logic provable from a set of axioms A, then ¬¬P is intuitionistically provable from (an even weaker set of axioms than) A as well.
https://en.wikipedia.org/wiki/Double-negation_translation.
>Logics without the law of non-contradiction are called "paraconsistent logics" and they are fucking stupid and don't do anything.This is not really accurate.
Paraconsistent logics tend to prove their non-contradiction, with the same proof as in
>>11280499.
Moreover, many paraconsistent logics are indeed also meta-logically non-contradictory (so the logic reflects correctly on itself).
What happens is that paraconsistent logics don't adopt the principle of explosion, so that from having proven a false proposition, one is allowed to draw any conclusion.
This isn't as bad as one may think. It mostly just renders disjunctions involving negations a dead end.
In particular, the disjunctive syllogism (separate true propositions from ruled out possibilities) relies on it:
((P ? Q) ? ¬P) implies Q
The proof of this requires you to have explosion, so that the case (P ? ¬P) enables you to prove Q.
If you don't have that, then there's less use in "?".
So that is a bit like a programming language where you have to know all your if-clauses at compile time.
Those logics still permit you to prove many implications. And the nice thing is that they have less axioms, so they are consistent with wilder semantics.
