What is the relationship between intuitionistic logic and 3-value logic?

Question

Intuitionistic logic is a form of logic that doesn't have the law of the excluded middle, or LEM. The LEM says basically that a proposition that is not true is false, and a proposition that is not false is true. Classical logic has LEM but intuitionistic logic does not.

A 3-value logic is a logic where a proposition can be not merely True or False, but also something else, typically Unknown. It can be used to handle various propositions that 2-value logic cannot, propositions formed such that there is no consistent way to assign either true or false to them. Naturally, LEM also does not apply to a 3-value logic. I tend to view LEM as a device for defining what counts as a proposition. In a logic with LEM, for example, you can't allow a proposition like the Liar, "This sentence is false", so it just can't be formulated as a proposition, but in 3-valued logic it would be possible to allow it.

It occurs to me that Intuitionistic logic is a sort of stub 3-value logic, one where there is no way to deal with the third value, but where the possibility of a 3rd value is still allowed for. That is, without LEM, there is no way to prove that a proposition can only have one of two values.

Are there any developments of this idea in the literature? For example, is there any work where intuitionistic logic is used as a base for either classical logic or 3-value logic just by adding axioms or other features?

Answer 1

A few points can be made here.

In the modern way that the Law of Excluded Middle is defined, it is a syntactic statement. It states that "φ ∨ ¬φ" is a theorem of logic. It is the Principle of Bivalence that states that "either φ is true or φ is false". Classical logic features both and intuitionistic logic lacks both. But they are not the same thing and some formal systems have one but not the other.

Intuitionistic logic is not three-valued. In fact, it is not n-valued for any finite n. This was proved by Kurt Gödel.

The term proposition is not usually limited to the two-valued case. For example, the SEP article on many-valued logic uses the term proposition and propositional logic to include the many-valued case.

Allowing three values does not satisfactorily resolve the liar paradox, since one can extend the paradox by weakening it, e.g. "This sentence either has no truth value or it is false."

You can treat superintuitionistic logic as a base for logics that are intermediate between intuitionistic and classical. There are several such logics.

Answer 2

In answer to the last question: is there any work where intuitionistic logic is used as a base for either classical logic or 3-value logic just by adding axioms or other features?

It's not in the literature, but it may be possible to do it the other way around, that is, to construct a model that satisfies Heyting's axioms of intutionism ( as for instance https://www3.cs.stonybrook.edu/~cse541/15chapter11.pdf ) using suitable definitions based on Lukasiewicz 3-valued logic. This does not establish equivalence. It appears that intuitionism uses a "strong" negation instead of the standard, which in a way breaks the system to make it non-truth functional, but the idea that intuitionism may be an incomplete stub of a more complete and robust (as well as truth-functional) 3-valued logic seems likely.

This doesn't really solve the paradox of the liar, since L3 has an "excluded fourth" law in place of the excluded middle, but an incomplete logic that can consistently handle the unknown is already useful in some computer applications.

As a bonus, it also seems possible to do the same with the Lewis axioms for S5: that is, construct a truth-functional 3-valued model that satisfies the axioms. Again this is not an equivalence, because the definition of the strict conditional is different, and Lewis's definition breaks the system, but the 3-valued version appears to be more robust.

Answer 3

In intuitionistic logic, we can't use LEM in order to prove propositions, but that doesn't mean that LEM is false. After all, the idea that "either LEM is true, or there's a proposition that is neither true nor false" is itself an LEM-like / classical piece of reasoning.

I mostly came into contact with intuitionistic logic via constructive logic, via proof assistants where you identify propositions with the set of their proofs and prove them by giving an explicit member of the set. In particular, when you're proving a disjunction "p or q", you need to pick which one of p or q you're going to produce a proof for, and then produce a proof for it, and on the other hand, when you have a proof for a disjunction, you're always able to inspect it and ask which of p or q it proves. In this way "p or q" means not only "p is true or q is true" but further "... and I can tell you which one".

Clearly we can't have LEM in such a system unless we're able to know not only that each statement is true or false, but decide which of those it is, which rules out any system that can encode basic integer arithmetic.

This doesn't mean that there's some secret third thing that propositions can be, that isn't either true or false. It just means that by restricting ourselves from exploiting the two-valued nature of our logic, we get proofs that can have more structure or content to them. These proofs are always also construction / decision procedures.

I intend this as an example of where an intuitionistic logical system may be useful despite conceptually having no need for a third truth value. I guess you could say "ok but this system doesn't track truth, it tracks provability, and there are three proof states, proven true, proven false, and unprovable", and that's kind of true? But it's not really central to what the system is for or how it works (and, as you suggested, the system doesn't really have a way of referring to the third state directly.)