According to the Wikipedia article on Heyting algebras:
Every totally ordered set that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice). In this case p→q equals to 1 when p≤q, and q otherwise.
It gives an example of a ternary algebra that refutes the LEM, which appear generalizable to these equalities:
∀X(v(X) := lowercase(X))∀x(0≤x≤1)v(⊤) = 1v(⊥) = 0v(A∧B) = min(a, b)v(A∨B) = max(a, b)v(A→B) = cond(a≤b) := max(v(a≤b), b)v(¬A) = cond(a≤0) = v(a≤0)
An intuitionistic countermodel for the LEM with a totally ordered set {0, .5, 1}, where a = 0.5 is therefore:
v(A∨¬A) = max(a, v(a≤0))v(A∨¬A) = max(.5, v(.5≤0))v(A∨¬A) = max(.5, 0)v(A∨¬A) = 0.5
However, if these rules are taken for ¬A∨¬¬A under the same ordered set and value assignment for a, it returns:
v(¬A∨¬¬A) = max(v(a≤0), v(v(a≤0)≤0))v(¬A∨¬¬A) = max(v(.5≤0), v(v(.5≤0)≤0))v(¬A∨¬¬A) = max(0, v(0≤0))v(¬A∨¬¬A) = max(0, 1)v(¬A∨¬¬A) = 1
This version of the LEM is not an intuitionistic tautology, though.
At first blush, it looks like the smallest totally ordered set needs to contain intermediate values equal to the number of atomic WFF's in the proposition to have indeterminate values for each propositional variable:
HA values := {0, .3̄, .6̄, 1}; a = 6̄; b = 3̄
v(((A→B)→A)→A) = cond(cond(cond(a≤b)≤a)≤a)v(((A→B)→A)→A) = cond(cond(cond(6̄≤3̄)≤6̄)≤6̄)v(((A→B)→A)→A) = cond(cond(3̄≤6̄)≤6̄)v(((A→B)→A)→A) = cond(1≤.6̄)v(((A→B)→A)→A) = 6̄
However, I suspect that either that cond() is not generalizable as described if negation is defined as cond(x≤0) or that there's some caveat to negation that I'm overlooking.
Is my initial guess wrong or is my suspicion correct? If yes to either, is this procedure salvageable?