We consider the logic of reflexive directed graphs, i.e. the set ${\bf L}_1$ of those propositional formulae $\varphi$ in the variables $p_i$, which are valid in exactly these graphs. It is a proper extension of intuitionistic logic.
As explained herehere, this logic can be characterized as the set of those propositional formulae $\varphi$, which are valid by a valuation in a finite Heyting-Algebra $\Omega_1$, so that $${\bf L}_1=\{\varphi\mid \Omega_1 \models \varphi \}.$$ The underlying set of $\Omega_1$ consists of the five elements $|\Omega_1|=\{0, s,t,s\vee t,1\}$ (truth-values) and its lattice operations are given by the tables $$\begin{array}{c|ccccc} \wedge & 0 & s & t & s\vee t & 1 \\\hline 0 & 0 & 0 & 0 & 0 & 0 \\ s & 0 & s & 0 & s & s \\ t & 0 & 0 & t & t & t \\ s\vee t & 0 & s & t & s\vee t & s\vee t \\ 1 & 0 & s & t & s\vee t & 1 \\ \end{array}\qquad\qquad \begin{array}{c|ccccc} \vee & 0 & s & t & s\vee t & 1 \\\hline 0 & 0 & s & t & s\vee t & 1 \\ s & s & s & s\vee t & s\vee t & 1 \\ t & t & s\vee t & t & s\vee t & 1 \\ s\vee t & s\vee t & s\vee t & s\vee t & s\vee t & 1 \\ 1 & 1 & 1 & 1 & 1 & 1 \\ \end{array}$$
So its underlying poset has the Hasse-diagram
Its (relative) pseudocomplement is given by the table
$$\begin{array}{c|ccccc} \Rightarrow & 0 & s & t & s\vee t & 1 \\\hline 0 & 1 & 1 & 1 & 1 & 1 \\ s & t & 1 & t & 1 & 1 \\ t & s & s & 1 & 1 & 1 \\ s\vee t & 0 & s & t & 1 & 1 \\ 1 & 0 & s & t & s\vee t & 1 \\ \end{array}\qquad\qquad \begin{array}{c|c} \neg & \\\hline 0 & 1 \\ s & t \\ t & s \\ s\vee t & 0 \\ 1 & 0 \\ \end{array} $$
Hence my question:
Is there a finite set of propositional formulae (axioms) such that ${\bf L}_1$ is the closure under the derivation-rules "modus ponens" and "substituition"?
If so, how can one find such a finite generating set?
