A set of valid Propositional logic formulas is decidable. A set of implicational propositional formulas is a subset of this set. If we limit Axiom schemas by removing Axiom schema 3 (Peirce's law) we get an implicational fragment of propositional intuitionistic logic.
Based on my reading about Curry–Howard correspondence this set is isomorphic to a set of types in Simply typed lambda calculus / Combinatory logic.
How to enumerate this set?
I suppose it is possible to list all propositional formulas: ${a, a\rightarrow a, a \rightarrow b, a\rightarrow a\rightarrow a,... ((a → b) → a) → a), ...}$ and use SAT solver to check validity. How to filter formulas that are valid due to Peirce's law? Are there SAT solvers that validate only propositional intuitionistic logic?
Is there a more efficient procedure to enumerate this set? The size of all formulas grows very fast ((n^n)*(Number of binary trees of size n)).