Can we make intuitionistic logic "intuitive"?

This is something I am wondering about, because all the formulations I've seen of the logic seem fairly difficult to grasp, e.g. lists of abstract axioms that have a few missing versus classical logic. Yet, I've had the following idea floating around and wonder if it could work.

For me, ordinary classical logic is "more intuitive" because I can put it to a concrete evaluation algorithm, in the sense that if you know whether the elementary facts (atomic variables) of a given situation are true or false, you can easily evaluate the truth of a compound statement about them by using truth tables, which also have simple, intuitive interpretations, e.g. that "and" is only true when both its inputs are true, which makes sense from casual usage in English. Yet, as is well-known, for intuitionistic logic, not only is this not possible, but any "truth-functional", i.e. truth table-based approach must utilize a system with infinitely many truth values. Hence, what I am wondering about is - is there some non-truth functional "evaluation algorithm" for intuitionistic logic?

To illustrate what I mean. For the infinite truth values approach, one such system that works is to use the open subsets of $(0, 1)$ (I believe), where a full subset (i.e. $(0, 1)$ itself) is maximum truth, an empty subset is maximum falsehood, and the "middle ground" is every other subset, where many subsets are incomparable as truth values - we can only say one is "more truthful" than another if the former includes the latter as a subset, thus forming in effect a sort of fibrated structure to the truth values. This is, admittedly, a bit more "intuitive", but what would it mean for a realistic proposition to have, say, a truth value of $(0, 0.5)$ or $(0, 0.1) \cup (0.2, 0.9)$?

Now I suppose that, if one interprets the underlying epistemic basis of intuitionist logic as starting from that "truth means verifiability", i.e. to say that a proposition $P$ is "true" means we can prove it to be true, and to say that a proposition $P$ is "false" means we can prove it to be false, these may represent, perhaps, states of incomplete proof, i.e. they correspond to a situation in which we have some, but not all, evidence a given proposition is true, and perhaps we can understand the subsets of the interval as "coloring in" different areas where we have and don't have evidence with a suitable understanding of what the different numbers in the interval mean. After all, topologies or, better, open sets, have been described as generally specifying "semi-decidable properties", i.e. properties for which an assertion of their truth can be verified.

In addition, we perhaps could use more complicated topological spaces, too, as they will also form Heyting algebras in the same fashion, which then gives a ready example of what I'm talking about. Suppose an atomic proposition is "The car is red". Now we have a "car-shaped" topological space (i.e. a surface in $\mathbb{R}^3$ shaped like at least the hull of the car), which then induces a Heyting algebra. We've not seen the whole car, but only its back end, and seen that yes, it is red. Thus we should valuate that atomic formula to the open subset consisting only of the back end of the car. Would this make any sense? In this regard, it would become a richer version of fuzzy logic, where we can only give a percentage (0% to 100%) in which something is true.

But if it is not sensible, and also for its own sake, I will also say what I mean by a non-truth functional approach, which was the original thrust of this question. First, it would seem natural and intuitive to, given that the "excluded middle" is rejected, first expand the set of truth values to include an additional "unknown" or "unverifiable" value (U), in addition to "true" and "false". Now we have three, but not two, truth values. It is clear this is insufficient for a truth-functional interpretation. Hence, what I wonder then is if we can come up with some algorithm - which need not be efficient - that:

1. Takes as input an intuitionistic propositional formula,
2. Takes as input an assignment of T/F/U values to each atomic variable,
3. Evaluates the formula to the correct T/F/U value. Most importantly, that tautological formulas always evaluate to T and contradictory ones always to F.

Is such an algorithm possible? If not, why not? If so, what does it look like?

Solution 1:

There are a variety of semantics you can give to different systems.

You seem to be arguing intuitionistic logic has a more complicated denotational semantics than classical logic. A huge motivation behind constructive logics today is the fact that they can be given useful operational semantics. It is sort of possible to give an operational semantics to law of excluded middle in terms of control flow but the matter is confusing.

Ultimately I think it is a goal of constructive logics to have more complicated denotational semantics than classical logic. Otherwise such logics could not be interpreted into more complicated structures than boolean values.

Solution 2:

Hence, what I wonder then is if we can come up with some algorithm - which need not be efficient - that:

1. Takes as input an intuitionistic propositional formula,
2. Takes as input an assigment of T/F/U values to each atomic variable,
3. Evaluates the formula to the correct T/F/U value. Most importantly, that tautological formulas always evaluate to T and contradictory ones always to F.

Is such an algorithm possible? If not, why not? If so, what does it look like?

Let $p$ be the given formula. For every variable $x$ assigned T, let $p := x \to p$. For every variable $x$ assigned F, let $p := \neg x \to p$. The problem then reduces to checking whether $p$ is a tautology (T), $\neg p$ is a tautology (F), or neither (U). SEP says

The decidability of IPC [intuitionistic propositional logic] was first obtained by Gentzen in 1935.

referencing [1]. A tighter tesult is that this problem is PSPACE-complete [2]:

There is a polynomial time translation of intuitionistic logic into the modal logic S4 due to Tarski (see Fitting [3, p.43]). Ladner [4] shows that S4 can be decided in p-space, so the problem is p-space complete.

See this question for more details.

1. Gentzen, G., 1934–5, “Untersuchungen Über das logische Schliessen,” Mathematische Zeitschrift, 39: 176–210, 405–431.

2. Intuitionistic propositional logic is polynomial-space complete. Richard Statman. Theoretical Computer Science 9 (1):67-72 (1979).

3. Intuitionistic Logic, Modal Theory and Forcing. Melvin Fitting. North-Holland, Amsterdam (1969).

4. The computational complexity of provability in systems of modal propositional logic. Richard E. Ladner. SIAM Journal on Computing 6 (3):467–480 (1977).

Solution 3:

Topological semantics is indeed one natural way to look at intuitionistic logic, but your line of thinking with the car is based on a misinterpretation of the topological semantics. You seem to be focused on the idea that intuitionistic logic has infinitely many truth values, but it really doesn't (except in a technical algebraic sense which has little relevance to your request for an intuitive understanding of intuitionistic logic). Intuitionistic propositions have two truth values, just like classical ones, namely verified and not verified (or if you will, asserted and not asserted).

To understand how intuitionistic logic is the logic of open subsets of topological spaces, we first need to understand how classical logic is the logic of arbitrary subsets of arbitrary sets. In the classical case, the ambient set is the set of all possible worlds, or state of affairs, or outcomes of some experiment or observation, or something along those lines. A proposition is determined by its being true in some possible worlds and false in others. A proposition in classical logic is therefore interpreted as a subset of the set of all possible worlds, namely the set of all those worlds where it is true. Of course, if propositions $p$ and $q$ are interpreted by some subsets $X$ and $Y$ of the set of possible worlds $W$, then their conjunction $p \wedge q$ is interpreted by $X \cap Y$, whereas the negation $\neg p$ of the proposition $p$ is interpreted by $W \setminus X$.

Sticking to your car example, the proposition "this car is red" would be interpreted by the set of all possible worlds (however you conceive of those) where the color of the car, which I suppose for the sake of simplicity to be completely uniform, lies in some specified range. We can simplify this model by saying that the only relevant feature of the world that we are interested in is the color of the car, in which case the ambient set can perhaps be represented as the interval of wavelengths measured in nanometers $(0, \infty)$ and the proposition "this car is red" would be interpreted by some subinterval. It could be a closed interval, or an open one, or neither. Let us say that it is the open interval $(650, 700)$.

Now, for classical logic, this semantics is an overkill. This is because to determine whether a complex proposition of classical logic is true at a given world $w \in W$, all you need to know is whether its atomic subpropositions are true at the given world. In other words, if you are only interested in truth in the actual world, there is no reason whatsoever to bring other possible worlds into consideration. You can always take the ambient set to be a singleton.

This is not so with intuitionistic logic. To obtain a semantics for intuitionistic logic, we assume that the set of all possible worlds is in fact a topological space, the open sets representing things that you can verify (semi-decidable properties, in your terminology). We assume that each proposition is interpreted by an open set. Now suppose that I pick a possible world $w$ and a proposition $p$, e.g. your proposition "this car is red" again. Think of $p$ as a measuring stick that I apply against $w$. What could possibly happen?

If $p$ is verified in $w$, then we are good. The car is red. In other words, the measured wavelength lies somewhere in the interval $(650, 700)$.

If $p$ never gets verified, there are two possible reasons for this. One is that we can verify that the wavelength lies outside of $(650, 700)$. How could we possibly verify that? Well, our only measuring sticks are open sets, so the only way to verify that the wavelength lies outside of $(650, 700)$ is to verify that it lies in $(0, 650)$ or $(700, \infty)$. In this case, we say that $\neg p$ is verified. More formally, $\neg p$ is true in those worlds which lie in the interior of the complement of the open set of worlds where $p$ is true.

Of course, the remaining possibility is that we can verify neither $p$ or $\neg p$. The measured wavelength lies just on the borderline. We keep measuring for more and more precision, but we get $650.0$, $650.00$, $650.000$ and so on. At no point will we verify that the wavelength lies in $(650, 700)$, but at no point will we also be certain that this is not the case. Thus, the possible worlds where neither $p$ nor $\neg p$ can be verified may be thought of as the borderline cases, if you will. I hope that clarifies things at least a little.

You could also think of this as running parallel computational processes for $p$ and $\neg p$: one outcome is that $p$ successfully terminates, another outcome is that $\neg p$ successfully terminates, but it could also happen that neither process will terminate, in which case you are left in the dark about whether the point lies inside the set or not.

tl;dr: you should not think of open sets as truth values and then boggle your mind by thinking about what it could possibly mean to talk about the truth value $(0, 0.1) \cup (0.2, 0.9)$. Rather, you should think of them as interpretations of propositions in different worlds, scenarios, states of affairs, etc. Each proposition has only two possible truth values at each world: either the world lies inside the given open set, or it doesn't.