We consider the logic  of [reflexive directed graphs](https://ncatlab.org/nlab/show/reflexive+graph), i.e. the set
${\bf L}_1$ of those [propositional formulae](https://en.wikipedia.org/wiki/Propositional_formula) $\varphi$ in the variables $p_i$, which are valid in exactly these graphs.
It is a proper extension of [intuitionistic logic](https://en.wikipedia.org/wiki/Intuitionistic_logic).

As explained [here](http://mathoverflow.net/questions/231492/heyting-algebras-originating-from-directed-graphs), this logic can be characterized as  the set of those propositional formulae $\varphi$, which are valid by a [valuation](https://en.wikipedia.org/wiki/Valuation_(logic)) 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 

[![Hasse-diagram][1]][1]


 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"](https://en.wikipedia.org/wiki/Modus_ponens) and ["substituition"](https://en.wikipedia.org/wiki/Substitution_(logic))?


If so, how can one find such a finite generating set?


  [1]: https://i.sstatic.net/8cmND.png