What is the intuitive meaning of the Heyting algebra? I'm curious about this.
As we all know, classical logic can be described as what is called the Boolean Algebra, in particular, you can think of figuring out the truth of a classical composite statement like "P and Q" from the truth values of its components or atomic statements, by applying truth tables to look up the values of the connectives.
However, one with a bit more initiation will realize that classical logic is, of course, not the only logic out there - there are others as well, such as the intuitionistic logic in which we try to reject the law of the excluded middle, i.e. that "P OR NOT P" must be tautological, and that there may be $P$ where it may not attain truth (Actually, it is one such logic, there are others you can make as well that do the same.). In particular intuitionistic logic is strictly weaker than classical logic meaning that it will never affirm anything that classical does not and anything it does affirm will be affirmed in classical - which also implies that the law of excluded middle is never actually falsified, just not always affirmed, for falsifying the law is equivalent to affirming its negation, i.e "NOT (P OR NOT P)", and thus it is tautological in IL that "NOT NOT (P OR NOT P)", but the double negation doesn't cancel.
Given the ease of the "truth table" paradigm, a natural question arises as to whether you can do the same thing for the intuitionistic logic, and it turns out that the answer is, in a sense, yes: but it requires what amounts to a truth table involving not just an infinite, but an uncountably infinite (namely $\beth_1$ - same as the real line!) amount of truth values - which are not, as you might naively think, reals between 0 and 1 as though representing a "middling" truth like in another non-classical system called "fuzzy logic", at least not in any straightforward way, but rather are something muucchh weerder: in particular, the "truth values" are effectively all open sets of the real line (though this may not be the only model but I believe any model has to be at least this big!), where "false" is the empty set and "true" the whole line. The great stringy middle is just that - the ordering is by inclusion, and this leads to a complex, fibrated structure (in infinitiye-dimensional infinityey infispace!) instead of the naively-expected continuum "in the middle". (E.g. one "fiber" of truth values is the one formed by the sets $(-a, a)$ with $a \in [0, \infty]$ (no the last bracket is NOT a typo and YES that makes sense) while a different "fiber" would be $(100 - a, 100 + a)$ with the same range of $a$ after at least a suitably great "depth" $\frac{1}{a}$.)
So my question is why is this? Why is it that the structure of truth values that we must accept, following some relatively simple modifications or "weakenings" of the classical logic, to make the truth tables, must "suddenly" explode to not just a large or even infinite but this enormously infinite set that even more has a structure which to me it seems at least you could never guess a priori? Moreover, is there any "meaning" that can be assigned to these weird truth values?
 A: Gödel showed (in effect) that no finite Heyting algebra is complete. The term model or Lindenbaum algebra of intuitionistic propositional logic (IPL) is a countable Heyting algebra that is complete for IPL.
The extent to which the term model provides any insight into meaning, however, is limited: the elements of the term model are equivalence classes of propositional formulas under the equivalence relation $\simeq$ defined by $\phi \simeq \psi$ iff IPL proves $\phi \Leftrightarrow \psi$. So the "meaning" is defined in terms of the provability relation.
So you don't need uncountably many truth values to get completeness. The topology of the real numbers just provides a mathematically natural example of a Heyting algebra that is complete for IPL and happens to be uncountable.
An algebraically more natural countable Heyting algebra that is complete for IPL was discovered in the 1930s by Jaśkowski. In modern terminology, Jaśkowski describes a construction that adds a new co-atom to a Heyting algebra. I.e., given a Heyting algebra $H$, he defines $\Gamma(H)$ to be the disjoint union $H \sqcup \{*\}$ ordered so that $x < * < \top$ for every $x \in H \setminus \{\top\}$ and with the operations defined in the only possible way that agrees with the operations of $H$ on elements of $H$. He then defines a sequence of finite Heyting algebras:
$$
\begin{align*}
J_0 &= \Bbb{B} \\
J_{k+1} &= \Gamma(J_k^{k+1})
\end{align*}
$$
where $\Bbb{B}$ is the 2-element Heyting algebra.
If you let $J = \bigcup_kJ_k$ (where we consider $J_k$ to be embedded in $J_k^{k+1}$ via the diagonal embedding), then $J$ is clearly a countable Heyting algebra and it can be shown that $J$ is complete for IPL.
I say "it can be shown", but proofs are hard to find.
The original paper is Recherches sur le systeme de la logique intuitionistique [in Actes du Congres International de Philosophie Scientifique 6, pages 58–61, 1936], which can be found at https://gallica.bnf.fr/ark:/12148/bpt6k383699. Jaśkowski gives a very bare sketch of the proof and filling in the details is far from trivial. There is a paper by Gene F. Rose, Propositional calculus and realizability [Trans. Am. Math. Soc., 75:1–19, 1953] that gives a more detailed proof and refers to his Ph. D. thesis for even more details. (I think Rose's proof can be much simplified.) Like Jaśkowski, Rose uses the older notion of "matrix" rather than Heyting algebra.
This question inspired me to put up some notes I made on the Jaśkowski  models and Roses's proof on the arXiv. See http://arxiv.org/abs/1809.00393
