I noticed that when I want to know (or rather see/understand) whether some classical tautology is valid intuitionistically, I first try to replace each propositional variable by a finite union of open intervals on the real line $\mathbb R$, and see whether I can construct a counterexample in this way. I started to believe that this approach would always work, and found the following on wikipedia:
It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line $\mathbb R$.
The reference for this statement is "Lectures on the Curry-Howard Isomorphism" by M. Sørensen and P. Urzyczyn, which contains the following theorem:
- A formula $\varphi$ of length $n$ is valid iff it is valid in all Heyting algebras of cardinality at most $2^{2^n}$;
- Let $\mathcal H$ be the algebra of all open subsets of a dense-in-itself metric space $V$ (for instance the algebra of all open subsets of $\mathbb R^2$). Then $\mathcal H \vDash \varphi$ iff $\varphi$ is valid.
This theorem is not sufficient for proving that my approach will always work, because it might be necessary to also consider open sets like the complement of the Cantor set, or at least complements of countable closed sets with interesting limit points.
But if my approach would always work, then already the algebra $\mathcal H'$ of all unions of open intervals with integer end points of $\mathbb R$ should satisfy "$\mathcal H' \vDash \varphi$ iff $\varphi$ is valid". Is this true? If not, what is a simple counterexample?
Unfortunately, your approach does not always work. The formula $$\lnot\lnot p \lor (\lnot\lnot p\rightarrow p)$$ is true whenever $p$ is a finite union of open intervals in $\mathbb{R}$, but it is not intuitionistically valid.
Let $T$ be a finite union of open intervals. We'll call $T$ the land and $\lnot T$ (the interior of the complement of $T$) the sea. Any point of $\mathbb{R}$ which is not in the land or the sea is a boundary point of $T$. Let's say a boundary point $x$ is a lake if $x$ is isolated in the complement of $T$, and $x$ is a beach if not. For example, if $T = (a,b)\cup (b,c)$, then $a$ and $c$ are beaches and $b$ is a lake. Let $L$ be the set of lakes. Since $T$ is a finite union of intervals, $L$ is a finite discrete set.
Then $\lnot\lnot T$ is the interior of the complement of the sea. This contains the land and the lakes, but no beaches, so $\lnot\lnot T = T\cup L$.
Now $(\lnot\lnot T \rightarrow T)$ is the largest open set with the property that its intersection with $T\cup L$ is contained in $T$. In other words, it's all the points which have a neighborhood not containing any lakes. Since the lakes form a discrete set, $(\lnot\lnot T \rightarrow T) = \mathbb{R}\setminus L$.
Hence $\lnot\lnot T \lor (\lnot\lnot T\rightarrow T) = (T\cup L)\cup (\mathbb{R}\setminus L) = \mathbb{R}$.
I found this example by looking for the first place where the free Heyting algebra on one generator collapses when the generator is assigned to a generic finite union of intervals.
The argument above also goes through when $L$ has no limit points outside of $L$ (we didn't use that it's finite). So this formula is also valid on the algebra $\mathcal{H}'$ of (not necessarily finite) unions of open intervals with integer end points.
To come up with an open subset of $\mathbb{R}$ which does not satisfy this formula, we just need the lakes to have a limit point which is a beach (a limit of lakes can't be on land or in the sea). So let $U = \bigcup_{n\in\mathbb{N}_+} (\frac{1}{n+1},\frac{1}{n})$. We have $\lnot\lnot U = (0,1)$ and $(\lnot\lnot U \rightarrow U) = \mathbb{R}\setminus (\{0\}\cup \{\frac{1}{n}\mid n\in\mathbb{N}_+\})$, so $0\notin \lnot\lnot U \lor (\lnot\lnot U \rightarrow U)$.