# Is the logic of directed graphs generated by a finite set of formulae?

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 here, 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?

In addition to a list of equations for Heyting algebras add the two equations $p \vee (p \Rightarrow (q \vee \neg q)) =1$ and $\neg(p\wedge q \wedge r) =\neg(p \wedge q ) \vee \neg(q \wedge r) \vee \neg(r \wedge p).$ The first forces a subdirectly irreducible Heyting algebra to have the structure of a Boolean algebra plus a 1 added at the top, the second restricts the size of the Boolean algebra under the 1 to at most 4 elements.