I had previously sought some insight for handling logical operators in the Rieger-Nishimura lattice and, with assistance here, was able to work out a fairly rigorous way. To the best of my ability, I constructed the following "RN-tables", let's call them?
$d$ refers to a disjunctive point (a proposition with $\vee$ as the main operator).
$i$ refers to an implicative point (a proposition with $\rightarrow$ as the main operator).
In the Rieger-Nishimura lattice:
- $d_0 = \bot$
- $i_0 = \bot$
- $d_1 = A$
- $i_1 = \neg A$
- $d_{n+1} = d_n \vee i_n$ when $n>0$
- $i_{n+1} = i_n \rightarrow d_n$ when $n>0$
- $d_\infty = \top$
- $i_\infty = \top$
Below, $x$ refers to either one of $d$ or $i$.
| $A$ | $B$ | $(n,m)$ | $A \rightarrow B$ |
|---|---|---|---|
| $x_n$ | $x_m$ | $n = 0$ | $\top$ |
| $x_n$ | $x_m$ | $m = 0$ | $\neg x_n$ |
| $d_n$ | $d_m$ | $n \leq m$ | $\top$ |
| $d_n$ | $d_m$ | $n = m + 1$ | $i_n$ |
| $d_n$ | $d_m$ | $n > m + 1$ | $d_m$ |
| $d_n$ | $i_m$ | $n < m$ | $\top$ |
| $d_n$ | $i_m$ | $n \geq m$ | $i_m$ |
| $i_n$ | $d_m$ | $n < m$ | $\top$ |
| $i_n$ | $d_m$ | $n = m$ or $n = m + 2$ | $i_{m+1}$ |
| $i_n$ | $d_m$ | $n = m + 1$ | $i_{m+2}$ |
| $i_n$ | $d_m$ | $n > m + 2$ | $d_m$ |
| $i_n$ | $i_m$ | $n = m$ or $n + 1 < m$ | $\top$ |
| $i_n$ | $i_m$ | $n + 1 = m$ or $n > m$ | $i_m$ |
| $A$ | $(n,m)$ | $\neg A$ |
|---|---|---|
| $x_n$ | $n = 0$ | $\top$ |
| $x_n$ | $n > 2$ | $\bot$ |
| $d_n$ | $n = 1$ | $i_1$ |
| $d_n$ | $n > 1$ | $\bot$ |
| $i_n$ | $n = 1$ | $i_2$ |
| $i_n$ | $n = 2$ | $i_1$ |
| $A$ | $B$ | $(n,m)$ | $A \wedge B$ |
|---|---|---|---|
| $x_n$ | $x_m$ | $n = 0$ or $m = 0$ | $\bot$ |
| $x_n$ | $x_m$ | $n = \infty$ | $x_m$ |
| $x_n$ | $x_m$ | $m = \infty$ | $x_n$ |
| $d_n$ | $d_m$ | $n \leq m$ | $d_n$ |
| $d_n$ | $d_m$ | $n > m$ | $d_m$ |
| $d_n$ | $i_m$ | $n < m$ | $d_n$ |
| $d_n$ | $i_m$ | $n = m$ | $d_{n-1}$ |
| $d_n$ | $i_m$ | $n > m$ | $i_m$ |
| $i_n$ | $d_m$ | $n < m$ | $i_n$ |
| $i_n$ | $d_m$ | $n = m$ | $d_{n-1}$ |
| $i_n$ | $d_m$ | $n > m$ | $d_m$ |
| $i_n$ | $i_m$ | $n = m$ or $n + 1 < m$ | $i_n$ |
| $i_n$ | $i_m$ | $n + 1 = m$ | $d_{n-1}$ |
| $i_n$ | $i_m$ | $n = m + 1$ | $d_{m-1}$ |
| $i_n$ | $i_m$ | $n > m + 1$ | $i_m$ |
| $A$ | $B$ | $(n,m)$ | $A \vee B$ |
|---|---|---|---|
| $x_n$ | $x_m$ | $n = \infty$ or $m = \infty$ | $\top$ |
| $x_n$ | $x_m$ | $n = 0$ | $x_m$ |
| $x_n$ | $x_m$ | $m = 0$ | $x_n$ |
| $d_n$ | $d_m$ | $n \leq m$ | $d_m$ |
| $d_n$ | $d_m$ | $n > m$ | $d_n$ |
| $d_n$ | $i_m$ | $n < m$ | $i_m$ |
| $d_n$ | $i_m$ | $n = m$ | $d_{n+1}$ |
| $d_n$ | $i_m$ | $n > m$ | $d_n$ |
| $i_n$ | $d_m$ | $n < m$ | $i_m$ |
| $i_n$ | $d_m$ | $n = m$ | $d_{n+1}$ |
| $i_n$ | $d_m$ | $n > m$ | $i_n$ |
| $i_n$ | $i_m$ | $n + 1 = m$ | $d_{m+1}$ |
| $i_n$ | $i_m$ | $n + 1 < m$ | $i_m$ |
| $i_n$ | $i_m$ | $n = m$ | $i_n$ |
| $i_n$ | $i_m$ | $n = m + 1$ | $d_{n+1}$ |
| $i_n$ | $i_m$ | $n > m + 1$ | $i_n$ |
Since all of the intuitionistically contentious (classical-only) axioms or theorems eventually resolve to a handful of base intuitionistic formulae that Heyting algebra and the Gödel-McKinsey-Tarski S4 translation also reject -- DNE, the LEM, and the WLEM -- and all of them take only one atomic statement, that the following strategy would work to check for intuitionistic validity:
- Generate all of the value-assignment combinations using all of the RN propositions that close under negation $\\{\bot, d_1, i_1, i_2, \top\\}$ for the number of atomic sentences in a proposition. That would make $5^p$ combinations where $p$ is the number of unique atomic sentences.
- Perform the evaluations from sub-proposition to proposition in the normal truth-table way.
- If the final outputs are all $\top$, then the proposition is an intuitionistic tautology (since it's a subintuitionistic tautology). If the final outputs are all $\bot$, then it's an intuitionistic contradiction. Otherwise, it's the set of unique values that it returns (which I've called "unsure" since my previous decision procedure lacked the $\rightarrow$ operator and just exploited Gilvenko's theorem to convert a Kleene "underdetermined" value to shift to
falsewhen a classical contradiction was found).
I know this really murks the syntactic-semantic distinction, since treating $d_1$ as a value, for instance, would not offer explicit semantic content. However, it does seem to deny the usual classical-only tautologies, and I'll check that it affirms all of the Hilbert axioms (I'm still working on them).
- The LEM and WLEM obviously fail.
- DNE fails in the usual way: $\neg \neg A \rightarrow A$ :: $i_2 \rightarrow d_1$ :: $i_3$.
- Peirce's law fails: $((A \rightarrow B) \rightarrow A) \rightarrow A$ :: $((d_1 \rightarrow i_1) \rightarrow d_1) \rightarrow d_1$ :: $(i_1 \rightarrow d_1) \rightarrow d_1$ :: $i_2 \rightarrow d_1$ :: $i_3$.
- DGP fails: $(A \rightarrow B) \vee (B \rightarrow A)$ :: $(d_1 \rightarrow i_1) \vee (i_1 \rightarrow d_1)$ :: $i_1 \vee i_2$ :: $d_3$.
- etc., etc.
However, I've hardly got a completeness proof up my sleeve for this. So, that leaves me with two questions:
- Are the above tables correct?
- Is this a legitimate decision procedure to explore for IPC completeness?
For help illustrating what this procedure's doing, I'll take @Z.A.K.'s commented examples and show what the outputs would look like:
Table for $A \vee \neg A$
| $A$ | $\neg A$ | $A \vee \neg A$ |
|---|---|---|
| $\bot$ | $\top$ | $\top$ |
| $d_1$ | $i_1$ | $d_2$ |
| $i_1$ | $i_2$ | $d_3$ |
| $i_2$ | $i_1$ | $d_3$ |
| $\top$ | $\bot$ | $\top$ |
Table for $A \rightarrow (A \vee B)$
| $A$ | $B$ | $A \vee B$ | $A \rightarrow (A \vee B)$ |
|---|---|---|---|
| $\bot$ | $\bot$ | $\bot$ | $\top$ |
| $\bot$ | $d_1$ | $d_1$ | $\top$ |
| $\bot$ | $i_1$ | $i_1$ | $\top$ |
| $\bot$ | $i_2$ | $i_2$ | $\top$ |
| $\bot$ | $\top$ | $\top$ | $\top$ |
| $d_1$ | $\bot$ | $d_1$ | $\top$ |
| $d_1$ | $d_1$ | $d_1$ | $\top$ |
| $d_1$ | $i_1$ | $d_2$ | $\top$ |
| $d_1$ | $i_2$ | $i_2$ | $\top$ |
| $d_1$ | $\top$ | $\top$ | $\top$ |
| $i_1$ | $\bot$ | $i_1$ | $\top$ |
| $i_1$ | $d_1$ | $d_2$ | $\top$ |
| $i_1$ | $i_1$ | $i_1$ | $\top$ |
| $i_1$ | $i_2$ | $d_3$ | $\top$ |
| $i_1$ | $\top$ | $\top$ | $\top$ |
| $i_2$ | $\bot$ | $i_2$ | $\top$ |
| $i_2$ | $d_1$ | $i_2$ | $\top$ |
| $i_2$ | $i_1$ | $d_3$ | $\top$ |
| $i_2$ | $i_2$ | $i_2$ | $\top$ |
| $i_2$ | $\top$ | $\top$ | $\top$ |
| $\top$ | $\bot$ | $\top$ | $\top$ |
| $\top$ | $d_1$ | $\top$ | $\top$ |
| $\top$ | $i_1$ | $\top$ | $\top$ |
| $\top$ | $i_2$ | $\top$ | $\top$ |
| $\top$ | $\top$ | $\top$ | $\top$ |
Table for $A \rightarrow (B \vee \neg B)$
| $A$ | $B$ | $\neg B$ | $B \vee \neg B$ | $A \rightarrow (B \vee \neg B)$ |
|---|---|---|---|---|
| $\bot$ | $\bot$ | $\top$ | $\top$ | $\top$ |
| $\bot$ | $d_1$ | $i_1$ | $d_2$ | $\top$ |
| $\bot$ | $i_1$ | $i_2$ | $d_3$ | $\top$ |
| $\bot$ | $i_2$ | $i_1$ | $d_3$ | $\top$ |
| $\bot$ | $\top$ | $\bot$ | $\top$ | $\top$ |
| $d_1$ | $\bot$ | $\top$ | $\top$ | $\top$ |
| $d_1$ | $d_1$ | $i_1$ | $d_2$ | $\top$ |
| $d_1$ | $i_1$ | $i_2$ | $d_3$ | $\top$ |
| $d_1$ | $i_2$ | $i_1$ | $d_3$ | $\top$ |
| $d_1$ | $\top$ | $\bot$ | $\top$ | $\top$ |
| $i_1$ | $\bot$ | $\top$ | $\top$ | $\top$ |
| $i_1$ | $d_1$ | $i_1$ | $d_2$ | $\top$ |
| $i_1$ | $i_1$ | $i_2$ | $d_3$ | $\top$ |
| $i_1$ | $i_2$ | $i_1$ | $d_3$ | $\top$ |
| $i_1$ | $\top$ | $\bot$ | $\top$ | $\top$ |
| $i_2$ | $\bot$ | $\top$ | $\top$ | $\top$ |
| $i_2$ | $d_1$ | $i_1$ | $d_2$ | $d_3$ |
| $i_2$ | $i_1$ | $i_2$ | $d_3$ | $\top$ |
| $i_2$ | $i_2$ | $i_1$ | $d_3$ | $\top$ |
| $i_2$ | $\top$ | $\bot$ | $\top$ | $\top$ |
| $\top$ | $\bot$ | $\top$ | $\top$ | $\top$ |
| $\top$ | $d_1$ | $i_1$ | $d_2$ | $d_2$ |
| $\top$ | $i_1$ | $i_2$ | $d_3$ | $d_3$ |
| $\top$ | $i_2$ | $i_1$ | $d_3$ | $d_3$ |
| $\top$ | $\top$ | $\bot$ | $\top$ | $\top$ |
From this procedure, only $A \rightarrow (A \vee B)$ is an intuitionistic tautology. The others are not.
For your first question: I have now provided full operation tables for these operations under another question, and I feel quite certain about the correctness of the values there. So as long as your tables give the same result, you're good.
For your second question: no. Unfortunately, this is not a sound decision procedure for intuitionistic propositional logic, because it returns the verdict intuitionistic tautology on many formulas which are not actually intuitionistic tautologies.
I'll give one example of such a formula, in six atoms $B,C,D,E,F,G$.
$ (B \leftrightarrow C) \vee (B \leftrightarrow D) \vee (B \leftrightarrow E) \vee (B \leftrightarrow F) \vee (B \leftrightarrow G) \vee (C \leftrightarrow D) \vee (C \leftrightarrow E) \vee (C \leftrightarrow F) \vee (C \leftrightarrow G) \vee (D \leftrightarrow E) \vee (D \leftrightarrow F) \vee (D \leftrightarrow G) \vee (E \leftrightarrow F) \vee (E \leftrightarrow G) \vee (F \leftrightarrow G) $
I will now explain why the formula above cannot be an intuitionistic tautology. Intuitionistic logic has the disjunction property: $\varphi \vee \psi$ is a tautology of intuitionistic propositional logic precisely if one of the disjuncts, $\varphi$ or $\psi$, is a tautology. But in the long disjunction above, every disjunct has the form $P \leftrightarrow Q$ for two different propositional letters $P,Q$. This $P \leftrightarrow Q$ is not an intuitionistic tautology - it's not even a classical tautology. And since none of the disjuncts are tautologies of intuitionistic logic, it follows from the disjunction property that the massive disjunction above is not a tautology of intuitionistic logic either.
However, if you assign one of the values $d_0, d_1, i_1, i_2, \top$ to the atoms $B,C,D,E,F,G$ above, and evaluate the result in the Rieger-Nishimura lattice, then you will always end up with the result $\top$. Why?
Well, you have 6 atoms, but only 5 possible values. The pigeonhole principle implies that no matter how you assign the values to the atoms, you will always find two atoms which got the same value. Let's say $B$ and $G$ got the same value. Then when you evaluate $B \leftrightarrow G$, you will evaluate either $d_0 \leftrightarrow d_0$, $d_1 \leftrightarrow d_1$, $i_1 \leftrightarrow i_1$, $i_2 \leftrightarrow i_2$, or $\top \leftrightarrow \top$. All of these evaluate to $\top$ in the Rieger-Nishimura lattice (as you'd expect, and as you can check using the operation tables linked above).
But this means that one of the disjuncts evaluates to $\top$, and since $\top \vee x = \top = x \vee \top$, the whole disjunct must therefore evaluate to $\top$, no matter how you assign the five values to the atoms.
When describing your method, you write that if the final outputs are all $\top$, then the proposition is an intuitionistic tautology. So your decision method would return that this formula is an intuitionistic tautology, even though we just established that it isn't. So your method is unsound.
Checking intuitionistic validity in full generality is a very very hard problem: Statman's article explains how difficult it really is. While your current idea is clever, it's ultimately too similar to a finite-valued semantics to get off the ground, and we know that no finite-valued semantics could work. But even if you were to extend the semantics to use more initial values instead of just the five you have above (e.g. dynamically based on the size of the formula), we know from complexity theory that the amount of information that you need to shuffle around to test whether a formula is an intuitionistic tautology grows faster than any exponential function in the number of connectives and variables. This means that most natural ideas for semantics based on the Rieger-Nishimura lattice simply won't work: the lattice has bounded width, so you cannot get sufficiently many different combinations of elements fast enough to make it work.