Enumerate propositional formulas that are classically valid, but intuitionistically invalid

Question

tl;dr I'm looking for a syntactical way to enumerate tautologies in propositional logic that are not tautological in intuitionistic logic.

---

Intuitively, the theorems of propositional logic are enumerable – I can start with a tautology, say $p \vee \neg p$, and then apply all natural deduction rules to generate more tautologies. I'm not sure exactly how one can implement this, but since I remember the theorems of first-order logic to be (recursively) enumerable, this should be possible especially for propositional logic.

I'm now however interested in classical tautologies for which an intuitionistic countermodel exists. So all $\phi \in CPC \backslash IPC$. The countermodel is not of interest, only an efficient way to enumerate all those $\phi$.

My first idea was to start with a generator $p \vee \neg p$ and then somehow only derive theorems of classical logic.

Do you know of papers in this area? I'm struggling to get off the ground with the problem, but do you think my lastly mentioned approach could work?

Answer 1

Your problem asks for a decision procedure for intuitionistic propositional logic, which was the intended topic of this older Question. Despite getting off on the wrong foot with the Accepted Answer, the other two Answers (and their Comments) are relevant to your mission.

See Dychhoff's recent (2016) survey of developments since Gentzen, who showed decidability in his doctoral thesis. From the Abstract:

Gentzen solved the decision problem for intuitionistic propositional logic in his doctoral thesis [31]; this paper reviews some of the subsequent progress. Solutions to the problem are of importance both for general philosophical reasons and because of their use in implementations of proof assistants (such as Coq [4], widely used in software verification) based on intuitionistic logic.

This paper is "open access".