2
$\begingroup$

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

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.