# Enumerate propositional formulas that are classically valid, but intuitionistically invalid

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?