Universal Entailments in the Rieger-Nishimura Lattice for Conditionals

intuitionistic-logiclattice-ordersmodel-theory

I'm working on a bottom-up (atomics-to-proposition) intuitionistic decision procedure, and I encountered some fruits with the Rieger-Nishimura lattice. Specifically, I am looking at this article from Kocsis, which constructs the RN lattice as follows:

  • $d_0 = i_0 = \bot$
  • $d_1 = A$
  • $i_1 = \neg A$
  • $d_{n+1} = d_n \vee i_n$
  • $i_{n+1} = i_n \rightarrow d_n$
  • $d_\infty = i_\infty = \top$

So, $\neg\neg A$ is $i_2$, for example, and the LEM is $d_2$.

The article also cites these entailments:

  1. $d_n \rightarrow d_m = \top$ when $n \leq m$,
  2. $d_n \rightarrow i_m = \top$ when $n=0$ or $n<m$,
  3. $i_n \rightarrow d_m = \top$ when $n=0$ or $n<m$, and
  4. $i_n \rightarrow i_m = \top$ when $n=0$, $n=m$, or $n+1<m$.

My question is, are there guaranteed outputs for cases when the opposite is the case for $n$ and $m$ above?

For $d_n \rightarrow d_m$ and $n>m$, I was able to find equivalent solutions:

  • When $m=0$, $d_n \rightarrow d_m = \neg d_n$ (which is $\bot$ when $n>1$ and $i_1$ when $n=1$)
  • When $m>0$ and $n-m=1$, $d_n \rightarrow d_m = i_n$
  • When $m>0$ and $n-m>1$, $d_n \rightarrow d_m = d_m$

The basic idea in that case was to exploit that $d$ is disjunctive, so $d_n \rightarrow d_m$ is always

  • $d_n = d_1 \vee i_1 \dots \vee i_{n-1}$
  • $d_m = d_1 \vee i_1 \dots \vee i_{m-1}$

Since $(A \vee B) \rightarrow C$ iff $(A \rightarrow C) \wedge (B \rightarrow C)$ is an intuitionistic theorem,

$(d_1 \vee i_1 \dots \vee i_{n-1}) \rightarrow d_m$ cancels out redundancies from the $\vee$–$I$ theorem as…

  • $⊤ \wedge \dots \wedge (i_m \rightarrow d_m) \wedge \dots \wedge (i_{n-1} \rightarrow d_m)$

and yield the above results, depending on the distance of $n$ from $m$.

I didn't see any straightforward way to do this with the remaining combinations of $d$ and $i$ after negating the condition from before. Can this be done? If so, how?

For clarification, the remaining questions are those of entailment for…

  • $d_n \rightarrow i_m$ when $n > 0$ and $n \geq m$;
  • $i_n \rightarrow d_m$ when $n > 0$ and $n \geq m$; and
  • $i_n \rightarrow i_m$ when $n > 0$, $n \neq m$, and $n+1 \geq m$.

Best Answer

I give a full definition / case analysis for the operations $\vee$, and $\rightarrow$ and $\wedge$ on the Rieger-Nishimura latice below. I do this for four reasons:

  1. Alex's otherwise excellent answer contains a few minor mistakes at the time of writing, so I want to write down something whose correctness I've checked.
  2. I'd like to put the full operation tables here for future reference.
  3. I have immediate need for these tables to answer another question on this website.
  4. I prefer a presentation where different cases are not merged even if they yield the same result, and overlapping cases are guaranteed to give the same result: it makes the structure easier to see, and correctness easier to ascertain.

Keep in mind that the four cases I give in the article linked above do determine the order of the Rieger-Nishimura lattice completely. Consequently, one could deduce all of these equalities from those four. However, this boils down to giving a proof of Nishimura's theorem, and takes a significant amount of work, which I can't invest right now: I might come back to this answer at some point, and expand it into a proof.

In what follows, $x$ denotes one of $\top, d_n, i_n$, and the notations $d_n$ and $i_n$ have $n < \infty$: to keep things simple, we always treat the cases $\top=d_\infty=i_\infty$ separately.

Disjunction $\vee$

  • $\top \vee x = \top = x \vee \top$

  • $d_n \vee d_m = \begin{cases} d_m & \text{if } n < m\\ d_m & \text{if } n = m\\ d_n & \text{if } n > m \end{cases}$

  • $d_n \vee i_m = \begin{cases} d_n & \text{if } m = 0\\ i_m & \text{if } n < m\\ d_{n+1} & \text{if } n = m, m > 0\\ d_n & \text{if } n > m \end{cases}$

  • $i_n \vee d_m = d_m \vee i_n$

  • $i_n \vee i_m = \begin{cases} i_n & \text{if } m = 0\\ i_n & \text{if } n = 0\\ i_m & \text{if } n + 1 < m, n > 0\\ d_{m+1} & \text{if } n + 1 = m, n > 0\\ i_m & \text{if } n = m, n > 0, m > 0\\ d_{n+1} & \text{if } n = m + 1, m > 0\\ i_n & \text{if } n > m + 1 \end{cases}$

Implication $\rightarrow$

  • $\top \rightarrow x = x$

  • $x \rightarrow \top = \top$

  • $d_n \rightarrow d_m = \begin{cases} \top & \text{if } n < m\\ \top & \text{if } n = m\\ i_{m+1} & \text{if } n = m + 1\\ d_m & \text{if } n > m + 1 \end{cases}$

  • $d_n \rightarrow i_m = \begin{cases} d_n \rightarrow d_0 & \text{if } m = 0\\ \top & \text{if } n < m\\ i_m & \text{if } n = m, m > 0\\ i_m & \text{if } n > m, m > 0 \end{cases}$

  • $i_n \rightarrow d_m = \begin{cases} \top & \text{if } n = 0\\ \top & \text{if } n < m\\ i_{n+1} & \text{if } n = m, n > 0\\ i_{n+1} & \text{if } n = m + 1\\ i_{m+1} & \text{if } n = m + 2\\ d_m & \text{if } n > m + 2 \end{cases}$

  • $i_n \rightarrow i_m = \begin{cases} i_n \rightarrow d_0 & \text{if } m = 0\\ \top & \text{if } n = 0\\ \top & \text{if } n + 1 < m\\ i_m & \text{if } n + 1 = m, n > 0\\ \top & \text{if } n = m\\ i_m & \text{if } n > m, m > 0 \end{cases}$

Conjunction $\wedge$

  • $\top \wedge x = x = x \wedge \top$

  • $d_n \wedge d_m = \begin{cases} d_n & \text{if } n < m\\ d_m & \text{if } n = m\\ d_m & \text{if } n > m \end{cases}$

  • $d_n \wedge i_m = \begin{cases} d_n & \text{if } n < m\\ d_0 & \text{if } n = m = 0\\ d_{n-1} & \text{if } n = m, n > 0\\ i_m & \text{if } n > m \end{cases}$

  • $i_n \wedge d_m = d_m \wedge i_n$

  • $i_n \wedge i_m = \begin{cases} i_n & \text{if } n + 1 < m\\ i_m & \text{if } n > m + 1\\ i_m & \text{if } n = m\\ d_0 & \text{if } m = 0\text{ or } n = 0\\ d_{m-1} & \text{if } n = m + 1, m > 0\\ d_{n-1} & \text{if } n + 1 = m, n > 0 \end{cases}$

One can derive megation using the identity $\neg x = x \rightarrow d_0$: the resulting table is also given in the comments.

Related Question