A Fast, Synthetic Decision Procedure for the Full Intuitionistic Propositional Logic

Toward a "Proof-Functional" Semantics

Introduction

Brouwer, in his “Changes on the Relation Between Classical Logic and Mathematics”, begins with this:

Classical logic presupposed that independently of human thought there is a truth, part of which is expressible by means of sentences called 'true assertions', mainly assigning certain properties to certain objects or stating that objects possessing certain properties exist or that certain phenomena behave according to certain laws.

He notes, though, that the birth of constructive mathematics and logic moved us from a binary paradigm to a ternary one. In it, rather than propositions being inherently true or false, propositions are proved, disproved, or yet-unproved.

Classical propositional logic’s (CPL) Boolean semantics, though, have a key advantage over intuitionistic propositional logic (IPL). That is that we have sound and complete decision procedures of composite formulae in CPL by means of bottom-up synthesis, instead of by means of top-down parsing. Here’s the main difference:

A synthetic decision procedure¹ like truth-functional tables involves evaluating composite formulae by:

1. Pre-evaluating atomic formulae,

2. Combining those evaluations for total semantic coverage, and

3. Synthesizing those evaluations through constituent superformulae to the whole.

Parsing decision procedures, by contrast, are the prevailing norm of IPL semantics, and they work in reverse by:

1. Assuming the existence of a counter-model for the whole,

2. Breaking the composite whole to its constituent subformulae, and

3. Ceasing evaluation when the eventually value-assigned atoms either present a counter-model or show that no consistent counter-model can be found.

All tableaux-based methods for IPL work this way. For the purpose of innovating in programming language design, though, this approach is not adequate. Programmers need to be able to assign specific primitive values to variables and get predictable outputs by inputting them into logical relation with one another. A parsing decision procedure does not facilitate that kind of design or thought process.² A “proof-functional” decision procedure, if one exists for the full IPL operator set, does.

Amazingly, new synthetic IPL decision procedures have popped up in the last five or so years, and I’ve also been working openly on devising some with limited success. So, my plan for the remainder of this article is to amend my work with the work of others, and then to optimize a synthetic IPL decision procedure so that a proved-disproved-unproved triad may succeed.

The Base: IPL Fragment {¬,∧,∨}

I’ve shown in other places that the IPL operational fragment containing only {¬,∧,∨} has a decision procedure that combines strong Kleene logic with classical logic. It’s an intuitive first choice because strong Kleene logic has no tautologies, so it provides an open semantics that we can modify. To admit IPL tautologies for this fragment, we need only a lemma from Gilvenko’s theorem which states that CPL contradictions are IPL contradictions, and vice-versa. This allows us to re-map the Kleenean “unknown” (U) value to “false” (F) upon the discovery of a classical contradiction.

We’ll use the set {0,1,2} to represent Kleene’s analogous {F,U,T} set, and we’ll assume that every atomic formula begins with a head-value of 1 and a 2ⁿ-long tail-value representing a unique column of a classical truth-table (where n is the number of unique atomic formulae in composite formula). The strong-Kleenean evaluations for the fragment {¬,∧,∨} are:

\(\begin{array}{rcl} v(\top) & = & 2 \\ v(\bot) & = & 0 \\ v(\neg \phi) & = & 2-v(\phi) \\ v(\phi \vee \psi) & = & max(v(\phi),v(\psi)) \\ v(\phi \wedge \psi) & = & min(v(\phi),v(\psi)) \end{array}\)

I’ll illustrate this decision procedure with the double-negated law of excluded middle ¬¬(A∨¬A):

\(\begin{array}{|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \vee \neg A & \neg(A \vee \neg A) & \neg \neg (A \vee \neg A) \\ \hline 1 & 1 & 1 & 1 & 1 \mapsto 0 & 2 \\ \hline 2 & 2 & 0 & 2 & 0 & \\ 3 & 0 & 2 & 2 & 0 & \\ \hline \end{array}\)

Because (d,2) through (d,3) signify a classical contradiction, the unsure value at (d,1) “shifts” from 1 to 0, per the related lemma of Gilvenko’s theorem. At this point, we can completely omit the classical evaluation, only to reintroduce tails from 1-valued operands from ψ of max(0,v(ψ)) or min(2,v(ψ)) or their commuted equivalents.

This Gilvenko switch works because both CPL and IPL share a common bottom value for contradictions, and negating contradictions yields tautologies in both logics. That’s what Gilvenko’s theorem states, that A is a classical tautology if, and only if ¬¬A is an intuitionistic tautology.

The Goal: Adding {→,↔} to the Fragment

Intuitionistic Truth-Tables

Leme, Coniglio, and Lopes (2024) successfully created a decision procedure with restricted, non-deterministic matrices (RN-matrices), which works off of Grätz’s (2021) three-valued RN-matrix for classical modal logic S4. Given the Gödel-McKinsey-Tarski translation and classical S4’s completeness, it’s a natural choice for these non-deterministic matrices. Leme, et al. successfully adapted Grätz’s tables to abstract the base “intuitionistic truth-values” {F,U,T} (for consistency with this article’s notation, {0,1,2}) into existence.

\(\begin{array}{|c|c|} \hline A & \neg A \\ \hline 0 & \{1,2\} \\ \hline 1 & \{1,2\} \\ \hline 2 & \{0\} \\ \hline \end{array} ~ \begin{array}{|c|c|c|c|c|c|} \hline A & B & A \to B & A \vee B & A \wedge B \\ \hline 0 & 0 & \{1,2\} & \{0\}& \{0\} \\ \hline 0 & 1 & \{1,2\} & \{0\}& \{0\} \\ \hline 0 & 2 & \{2\} & \{2\}& \{0\} \\ \hline 1 & 0 & \{1,2\} & \{0\}& \{0\} \\ \hline 1 & 1 & \{1,2\} & \{0\}& \{0\} \\ \hline 1 & 2 & \{2\} & \{2\}& \{0\} \\ \hline 2 & 0 & \{0\} & \{2\}& \{0\} \\ \hline 2 & 1 & \{0\} & \{2\}& \{0\} \\ \hline 2 & 2 & \{2\} & \{2\}& \{2\} \\ \hline \end{array}\)

We can arithmetically render these values, with a and b as elements of {0,1,2} which correspond to formulae A and B, and where // refers to integer division, as follows:

\(\begin{array}{rcl} u(A) & := & (3-a)//2 \\ \\ v(\neg A) & = & \{1 \times u(a), 2 \times u(a)\} \\ v(A \to B) & = & \{1 \times u(a) \times u(b), 2 \times ((u(a)+(b//2)) - (u(a) \times (b//2))) \} \\ v(A \vee B) & = & \{2 \times \ (((a//2)+(b//2)) - ((a//2)\times(b//2)) \} \\ v(A \wedge B) & = & \{2 \times (a//2) \times (b//2)\} \\ \end{array}\)

Because the tables and formulae are non-deterministic for the operators {→,¬}, the decision procedure requires reiterations over the resulting intuitionistic truth-tables’ cells to remove rows with 1/U-valued cells that lack corresponding validators — other rows that legitimize a cell’s 1-valuation. I’ll illustrate this procedure for the same proposition as above (¬¬(A∨¬A)):

Stage 1 — Building: Build the intuitionistic truth-table. Here, the child evaluations are explicitly marked by the row-numeration system for illustrative purposes, as this is not shown in the original paper. I’ll then rewrite the table with the scheme used in the original work.

\(\begin{array}{|l|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \vee \neg A & \neg (A \vee \neg A) & \neg \neg (A \vee \neg A) \\ \hline 1 & 0_0 \\ 11 & & 1_{1} \\ 111 & & & 0_{1,11} \\ 1111 & & & & 1_{111} \\ 11111 & & & & & 1_{1111} \\ 11112 & & & & & 2_{1111} \\ 1112 & & & & 2_{111} \\ 11121 & & & & & 0_{1112} \\ 12 & & 2_{1} \\ 121 & & & 2_{1,12} \\ 1211 & & & & 0_{121} \\ 12111 & & & & & 1_{1211} \\ 12112 & & & & & 2_{1211} \\ 2 & 2_0 \\ 21 & & 0_{2} \\ 211 & & & 2_{2,21} \\ 2111 & & & & 0_{211} \\ 21111 & & & & & 1_{2111} \\ 21112 & & & & & 2_{2111} \\ \hline \end{array}\)

\(\begin{array}{|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \vee \neg A & \neg (A \vee \neg A) & \neg \neg (A \vee \neg A) \\ \hline 11111 & 0_0 & 1_{1} & 0_{1,11} & 1_{111} & 1_{1111} \\ 11112 & 0 & 1 & 0 & 1 & 2_{1111} \\ 11121 & 0 & 1 & 0 & 2_{111} & 0_{1112} \\ 12111 & 0 & 2_{1} & 2_{1,12} & 0_{121} & 1_{1211} \\ 12112 & 0 & 2 & 2 & 0 & 2_{1211} \\ 21111 & 2_0 & 0_{2} & 2_{2,21} & 0_{211} & 1_{2111} \\ 21112 & 2 & 0 & 2 & 0 & 2_{2111} \\ \hline \end{array}\)

\(\begin{array}{c} Build \dots \\ \begin{array}{|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \vee \neg A & \neg (A \vee \neg A) & \neg \neg (A \vee \neg A) \\ \hline 1 & 0 & 1 & 0 & 1 & 1 \\ 2 & 0 & 1 & 0 & 1 & 2 \\ 3 & 0 & 1 & 0 & 2 & 0 \\ 4 & 0 & 2 & 2 & 0 & 1 \\ 5 & 0 & 2 & 2 & 0 & 2 \\ 6 & 2 & 0 & 2 & 0 & 1 \\ 7 & 2 & 0 & 2 & 0 & 2 \\ \hline \end{array} \end{array}\)

Stage 2 — Validation: Seek validators for the 1-valued cells, where a row yᵥ validates a 1-valued cell (xₙ,yₙ) under the following three conditions:

• If (xᵥ,yᵥ) is 0.

  • In this example, (e,1) is 1, and (e,3) is 0.

• For all cells (x,yₙ) and (x,yᵥ) where x ranges from a to |x|, (x,yₙ)=2, then (x,yᵥ)=2.

  • In this example, there’s no (x,1) with the value 2, so it trivially follows that every (x,3) satisfies this criterion.

• Row yᵥ is, itself, validated.

  • In this example, row 3 is not, itself validated, because row 6 is marked for deletion since (e,6) has no validators, and because (d,3) fails the second condition at (d,7). That cancels the sole validator for row 1, so we must likewise delete it.

If no validators for a 1-valued cell exist, mark its row for deletion. If one does exist, seek validators for every 1-valued cell in its row (e.g., (b,3)), but remove the validator if the row, itself, is not fully validated.

\(\begin{array}{c} Validate \dots \\ \begin{array}{|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \vee \neg A & \neg (A \vee \neg A) & \neg \neg (A \vee \neg A) \\ \hline \xcancel{1} & 0 & 1 & 0 & 1 & 1:\cancel{(e,3)} \\ 2 & 0 & 1 & 0 & 1 & 2 \\ \xcancel{3} & 0 & 1:\emptyset & 0 & 2 & 0 \\ \xcancel{4} & 0 & 2 & 2 & 0 & 1:\emptyset \\ 5 & 0 & 2 & 2 & 0 & 2 \\ \xcancel{6} & 2 & 0 & 2 & 0 & 1:\emptyset \\ 7 & 2 & 0 & 2 & 0 & 2 \\ \hline \end{array} \end{array}\)

Stage 3 — Reduction: Delete the non-validated rows and those rows whose validations are, themselves, non-validated. Stop when:

• Repeating the validation and reduction stages for all 1-valued cells demands no further row deletions; or

• The final column’s values are all identical, since any further deletions yield no better information.

\(\begin{array}{c} Reduce~and~Validate \dots \\ \begin{array}{|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \vee \neg A & \neg (A \vee \neg A) & \neg \neg (A \vee \neg A) \\ \hline 2 & 0 & 1:(b,7) & 0 & 1:\begin{cases}(d,5) \\ (d,7) \end{cases} & 2 \\ 5 & 0 & 2 & 2 & 0 & 2 \\ 7 & 2 & 0 & 2 & 0 & 2 \\ \hline \end{array} \end{array}\)

This is a sound and complete decision procedure for IPL. However, there are a few inconveniences and quirks with it:

• The non-deterministic evaluations for the operators in {¬,→} rapidly grow the size of the table when formulae contain many of those operators.

• The intermediate tables’ rows sometimes produce strange results.

  • In the example above, the negated law of excluded middle ¬(A∨¬A) is 1 at (d,2) in the fully reduced table and 2 at (d,3) in the intermediate table, meaning the double-negaded law of excluded middle ¬¬(A∨¬A) is 0 at (e,3) of the intermediate table, though we should reject them outright because negations of contradictions are tautologies. Note that the contradiction A∧¬A is not strange, but the law of non-contradiction ¬(A∧¬A) is:

    \(\begin{array}{c} Build \dots \\ \begin{array}{|c|c|c|c|c|} \hline & a & b & c & d \\ \hline & A & \neg A & A \wedge \neg A & \neg (A \wedge \neg A) \\ \hline 1 & 0 & 1 & 0 & 1 \\ 2 & 0 & 1 & 0 & 2 \\ 3 & 0 & 2 & 0 & 1 \\ 4 & 0 & 2 & 0 & 2 \\ 5 & 2 & 0 & 0 & 1 \\ 6 & 2 & 0 & 0 & 2 \\ \hline \end{array} \end{array}\)

  Above, all of the odd-numbered rows above are superfluous, since there are no validators for them.

• This procedure relies on intuitionistic truth-values, which the authors define as select elements resulting from a mapping from a nested operator set signature {{¬},{∨,∧,→}} to a Cartesian product of Grätz’s modal S4 truth-values after simplifying his truth-tables for that logic.³ Because of this, it’s hard to intuit what the values {F,U,T} mean.

• Verum (⊤) loyally maps 2/T for all intuitionistic evaluations under the understanding that 0 and 1 are “falsy” values, but falsum (⊥) does not so loyally map to 0/F. This is inconvenient because two defining features of IPL are

  • The definition of negation ¬A as A→⊥ and

  • The principle of explosion (that ⊥→A is an IPL theorem and tautology).

Optimizing the intuitionistic truth-table decision procedure can mask some of these oddities by preventing the evaluation or creation of “misfit” values for columns (e.g., 2-values for contradictions, 1-values for contradictions, etc.). While the main objective in the following optimizations is to reduce this decision procedure’s runtime, we’ll see where and how they also alleviate the aforementioned issues.

Intuitionistic Truth-Table Optimizations

Optimization 1: “Chinese Scroll” Skips

Ancient Chinese scrolls were made of bound strips of wood or bamboo called 簡牘 (“jiǎndú”). This was very convenient back then, since Chinese texts primarily read from top to bottom, then right to left, and did so until the 1950s.

During the validation stage, if we follow this same approach when evaluating cells, we can remove rows before we have to validate 1-valued cells to the column left of it.

\(\begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|} \hline & a & b & c & d \\ \hline & A & B & B \to A & A \to (B \to A) \\ \hline \xcancel{1} & 0 & 0 & 1:Skip! & 1:\emptyset \\ 2 & 0 & 0 & 1:(c,6) & 2 \\ 3 & 0 & 0 & 2 & 2 \\ 4 & 2 & 0 & 2 & 2 \\ \xcancel{5} & 0 & 2 & 0 & 1:\emptyset \\ 6 & 0 & 2 & 0 & 2 \\ 7 & 2 & 2 & 2 & 2 \\ \hline \end{array} \end{array}\)

Further, if we perform the reductions in this order and have determined validity where the column consists only of 0s or 2s on the final column (d in the example), we can also skip the checks because we’ve likewise established an intuitionistic contradiction or tautology.

\(\begin{array}{c} Reduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|} \hline & a & b & c & d \\ \hline & A & B & B \to A & A \to (B \to A) \\ \hline 2 & 0 & 0 & 1:Skip! & 2 \\ 3 & 0 & 0 & 2 & 2 \\ 4 & 2 & 0 & 2 & 2 \\ 6 & 0 & 2 & 0 & 2 \\ 7 & 2 & 2 & 2 & 2 \\ \hline \end{array} \end{array}\)

Optimization 2: Indirect Intuitionistic Truth-Tables

If we focus our attention on creating 0-valued rows for compose formulae and deleting those without possible validators, instead of creating all of the rows and validating those that we can, we can effectively work backwards and build intuitionistic truth-tables indirectly rather than directly. The principle follows what we might expect in semantic tableaux for IPL, but instead we deny the creation of rows by enforcing several rules that we can infer from the intuitionistic truth-tables for the operators and by pushing negations to their literals.

This is a very redundant, but sufficiently comprehensive, list of rules that we can use to minimize row expansions:

\(\def\nin{\not\in} \def\Ra{\Rightarrow} \begin{array}{rcl} A \text{ is atomic} & \Ra & 1 \nin v(A) \\ A \text{ is } (P \vee Q) & \Ra & 1 \nin v(A) \\ A \text{ is } (P \wedge Q) & \Ra & 1 \nin v(A) \\ \\ v(\neg A) = \{0\} & \Ra & v(A) = \{2\} \\ v(A \to B) = \{0\} & \Ra & v(A) = \{2\} \text{ and } 2 \nin v(B) \\ v(A \vee B) = \{0\} & \Ra & 2 \nin v(A) \text{ and } 2 \nin v(B) \\ v(A \wedge B) = \{0\} & \Ra & \begin{cases} v(A) = \{2\} & \Ra & 2 \nin v(B) \\ v(B) = \{2\} & \Ra & 2 \nin v(A) \end{cases} \end{array} \)

\(\def\nin{\not\in} \def\Ra{\Rightarrow} \begin{array}{rcl} v(A) = \{2\} & \Ra & v(\neg A) = \{0\} \\ v(A) = \{2\} & \Ra & 1 \nin v(A \to B) \\ v(A) = \{2\} & \Ra & v(A \vee B) = \{2\} \\ v(A) = \{2\} & \Ra & \begin{cases} v(B) = \{2\} & \Ra & v(A \wedge B) = \{2\} \\ 2 \nin v(B) & \Ra & v(A \wedge B) = \{0\} \end{cases} \\ v(B) = \{2\} & \Ra & v(A \to B) = \{2\} \\ v(B) = \{2\} & \Ra & v(A \vee B) = \{2\} \\ v(B) = \{2\} & \Ra & \begin{cases} v(A) = \{2\} & \Ra & v(A \wedge B) = \{2\} \\ 2 \nin v(A) & \Ra & v(A \wedge B) = \{0\} \end{cases} \\ v(A \to B) = \{2\} & \Ra & \begin{cases} v(A) = \{2\} & \Ra & v(B) = \{2\} \\ 2 \nin v(B) & \Ra & 2 \nin v(A) \end{cases} \\ v(A \vee B) = \{2\} & \Ra & \begin{cases} 2 \nin v(A) & \Ra & v(B) = \{2\} \\ 2 \nin v(B) & \Ra & v(A) = \{2\} \end{cases} \\ v(A \wedge B) = \{2\} & \Ra & v(A) = \{2\} \text{ and } v(B) = \{2\} \\ \end{array} \)

\(\def\nin{\not\in} \def\Ra{\Rightarrow} \begin{array}{rcl} 2 \nin v(A) & \Ra & 0 \nin v(\neg A) \\ 2 \nin v(A) & \Ra & 0 \nin v(A \to B) \\ 2 \nin v(A) & \Ra & \begin{cases} 2 \nin v(B) & \Ra & v(A \vee B) = \{0\} \\ v(B) = \{2\} & \Ra & v(A \vee B) = \{2\} \end{cases} \\ 2 \nin v(A) & \Ra & v(A \wedge B) = \{0\} \\ 2 \nin v(B) & \Ra & \begin{cases} v(A \to B) = \{0\} & \Ra & v(A) = \{2\} \\ 0 \nin v(A \to B) & \Ra & 2 \nin v(A) \end{cases} \\ 2 \nin v(B) & \Ra & \begin{cases} 2 \nin v(A) & \Ra & v(A \vee B) = \{0\} \\ v(A) = \{2\} & \Ra & v(A \vee B) = \{2\} \end{cases} \\ 2 \nin v(B) & \Ra & v(A \wedge B) = \{0\} \\ \\ 2 \nin v(A \to B) & \Ra & 2 \nin v(B) \\ 2 \nin v(A \vee B) & \Ra & v(A \vee B) = \{0\} \\ 2 \nin v(A \wedge B) & \Ra & v(A \wedge B) = \{0\} \\ \end{array} \)

And these (optional) distribution rules allow us to use the previously listed rules more readily, since most of the rules apply to binary operators:

\(\begin{array}{rcl} \neg (A \to B) & \equiv & \neg \neg A \wedge \neg B \\ \neg (A \vee B) & \equiv & \neg A \wedge \neg B \\ \neg (A \wedge B) & \equiv & A \to \neg B \\ & \equiv & B \to \neg A \\ \neg \neg (A \to B) & \equiv & A \to \neg \neg B \\ \neg \neg (A \vee B) & \equiv & \neg A \to \neg \neg B \\ & \equiv &\neg B \to \neg \neg A \\ \neg \neg (A \wedge B) & \equiv & \neg \neg A \wedge \neg \neg B \\ \neg \neg \neg A & \equiv & \neg A \end{array}\)

The indirect method begins by assuming that the formula we test takes a value 0. From there, we apply the above rules to reduce the row count of the intermediate table, and then we adapt the validation to include those validators that the creation of the smaller intermediate truth-table potentially omitted, or else prove that no such validators exist. This can be very powerful technique, which I’ll illustrate with the superintuitionistic Gödel-Dummett theorem (A→B)∨(B→A):

\(\begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & B \to A & c \vee d \\ \hline 1 & 0 & 0 & 1:(c,5) & 1:(d,6) & 0 \\ 2 & 0 & 0 & 1:(c,5) & 2 & 2 \\ 3 & 0 & 0 & 2 & 1:(d,6) & 2 \\ 4 & 0 & 0 & 2 & 2 & 2 \\ 5 & 2 & 0 & 0 & 2 & 2 \\ 6 & 0 & 2 & 2 & 0 & 2 \\ 7 & 2 & 2 & 2 & 2 & 2 \\ \hline \end{array} \end{array} \)

If we initialize the process by first assuming the formula is of value 0 at (|x|,1), meaning that there is a possible validator for a potential 1-valued cell at |x|, the indirect build stage gives only one row, as opposed to seven:

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & B \to A & c \vee d \\ \hline 1 & \{0,2\} & \{0,2\} & \{0,1,2\} & \{0,1,2\} & 0 \\ \Da \\ 1 & \{0,2\} & \{0,2\} & \{0,1\} & \{0,1\} & 0 \\ \Da \\ 1 & 0 & 0 & \{0,1\} & \{0,1\} & 0 \\ \Da \\ 1 & 0 & 0 & 1 & 1 & 0 \\ \Da \\ 1 & 0 & 0 & 1 & 1 & 0 \\ \hline \end{array} \\ \\ (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & B \to A & c \vee d \\ \hline 1 & 0 & 0 & 1 & 1 & 0 \\ \hline \end{array} \\ \end{array}\)

We cannot continue directly to the direct validation stage, because we do not generate all of the possible validators with this method. Rather, we must reason backwards from the validation rules to reintroduce rows that may also be validators for each 1-valued cell in the built table. We accomplish this with the following intermediate steps:

• Stage 1.5 — Reintroduction and Validation (or Invalidation)…

1. Add a row |y|+1 for the 1-valued cell (x,y) needing validation.

   1. Give (x,|y|+1) cell the value 0.

   2. Duplicate the 2-values of row y into their respective columns of row |y|+1.

2. Fill the remaining cells of the row according to the rules.

   1. Split the rows if the rules and intuitionistic truth-table do not decide single values for every column of row |y|+1.

3. If there is not a consistent assignment for the added row(s), meaning that the initial cell assignments (1a-1b) force an assignment to change via the above rules, then mark row y for deletion and delete row |y|+1.

4. If the row |y|+1 is forced to match an already invalidated row (one marked for deletion), mark row y for deletion and delete row |y|+1.

5. If the row |y|+1 (or a split from row |y|+1 per (2)) contains a 1-valued cell, add another row |y|+2 to attempt to validate row |y|+1, returning to (1).

\(\def\Da{\Downarrow} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & B \to A & c \vee d \\ \hline 1 & 0 & 0 & 1:(c,3) & 1:(d,3) & 0 \\ \hline 2 & \{0,2\} & \{0,2\} & 0 & \{0,1,2\} & \{0,1,2\} \\ \Da \\ 2 & 2 & 0 & 0 & \{0,1,2\} & \{0,2\} \\ \Da \\ 2 & 2 & 0 & 0 & 2 & \{0,2\} \\ \Da \\ 2 & 2 & 0 & 0 & 2 & 2 \\ \hline 3 & \{0,2\} & \{0,2\} & \{0,1,2\} & 0 & \{0,1,2\} \\ \Da \\ 3 & 0 & 2 & \{0,1,2\} & 0 & \{0,2\} \\ \Da \\ 3 & 0 & 2 & 2 & 0 & \{0,2\} \\ \Da \\ 3 & 0 & 2 & 2 & 0 & 2 \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & B \to A & c \vee d \\ \hline 1 & 0 & 0 & 1:(c,3) & 1:(d,3) & 0 \\ \hline 2 & 2 & 0 & 0 & 2 & 2 \\ \hline 3 & 0 & 2 & 2 & 0 & 2 \\ \hline \end{array} \end{array} \)

We’ll call a table that we build, validate, and reduce in the aforementioned way an indirect intuitionistic truth-table. Such tables don’t only offer counter-models. They also indirectly prove which formulae are IPL tautologies. Let’s take Frege’s theorem (A→(B→C))→((A→B)→(A→C)) for this example:

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h & i \\ \hline & A & B & C & B \to C & A \to d & A \to B & A \to C & f \to g & e \to h \\ \hline 1 & 0 & 0 & 0 & 2 & 2 & 1 & 1 & 1 & 0 \\ 2 & 0 & 0 & 0 & 2 & 2 & 2 & 1 & 0 & 0 \\ 3 & 2 & 0 & 0 & 2 & 2 & 0 & 0 & 1 & 0 \\ \hline \end{array} \end{array} \)

The initial validation shows that two rows — 2 and 3 — need the reintroduction stage to attempt to validate them.

\(\def\Da{\Downarrow} \begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h & i \\ \hline & A & B & C & B \to C & A \to d & A \to B & A \to C & f \to g & e \to h \\ \hline 1 & 0 & 0 & 0 & 2 & 2 & 1:(f,3) & 1:(g,3) & 1:(h,2) & 0 \\ 2 & 0 & 0 & 0 & 2 & 2 & 2 & 1:\emptyset & 0 & 0 \\ 3 & 2 & 0 & 0 & 2 & 2 & 0 & 0 & 1:\emptyset & 0 \\ \hline \end{array} \end{array} \)

Neither row has a consistent validator row, so we mark both for deletion.

\(\def\Da{\Downarrow} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h & i \\ \hline & A & B & C & B \to C & A \to d & A \to B & A \to C & f \to g & e \to h \\ \hline \xcancel{2} & 0 & 0 & 0 & 2 & 2 & 2 & 1:\emptyset & 0 & 0 \\ \hline 4 & \{0,2\} & \{0,2\} & \{0,2\} & 2 & 2 & 2 & 0 & \{0,1,2\} & \{0,1,2\} \\ \Da \\ 4 & 2 & \{0,2\} & 0 & 2 & 2 & 2 & 0 & 0 & \{0,1,2\} \\ \Da \\ 4 & 2 & 0 & 0 & 2 & 2 & 2 & 0 & 0 & 0 \\ \Da \\ \xcancel{4} & 2 & 0 & 0 & 2 & 2 & \cancel{2}~0 & 0 & 0 & 0 \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h & i \\ \hline & A & B & C & B \to C & A \to d & A \to B & A \to C & f \to g & e \to h \\ \hline \xcancel{3} & 2 & 0 & 0 & 2 & 2 & 0 & 0 & 1:\emptyset & 0 \\ \hline 5 & 2 & \{0,2\} & \{0,2\} & 2 & 2 & \{0,1,2\} & \{0,1,2\} & 0 & \{0,1,2\} \\ \Da \\ 5 & 2 & \{0,2\} & \{0,2\} & 2 & 2 & 2 & \{0,1\} & 0 & 0 \\ \Da \\ 5 & 2 & 2 & 0 & 2 & 2 & 2 & \{0,1\} & 0 & 0 \\ \Da \\ \xcancel{5} & 2 & 2 & 0 & \cancel{2}~0 & 2 & 2 & \{0,1\} & 0 & 0 \\ \hline \end{array} \end{array} \)

We may naïvely want to reduce the table immediately.

\(\def\Da{\Downarrow} \begin{array}{c} Reduce \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h & i \\ \hline & A & B & C & B \to C & A \to d & A \to B & A \to C & f \to g & e \to h \\ \hline 1 & 0 & 0 & 0 & 2 & 2 & 1:\cancel{(f,3)} & 1:\cancel{(g,3)} & 1:\cancel{(h,2)} & 0 \\ \hline \end{array} \end{array} \)

But, doing that without keeping a record of the invalidated rows means we’d have to reintroduce each former validator, and then invalidate it, which is needlessly repetitive. If we instead keep track of those invalidated rows, and if a reintroduced validator for a 1-valued cell is identical to one that we’ve invalidated, we can infer that the reintroduced row and the checked row are invalid. The example illustrates this during the reintroduction stage for (h,1):

\(\def\Da{\Downarrow} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h & i \\ \hline & A & B & C & B \to C & A \to d & A \to B & A \to C & f \to g & e \to h \\ \hline \xcancel{1} & 0 & 0 & 0 & 2 & 2 & 1:\emptyset & 1:\emptyset & 1:\emptyset & 0 \\ \hline 6 & \{0,2\} & \{0,2\} & \{0,2\} & 2 & 2 & \{0,1,2\} & \{0,1,2\} & 0 & \{0,1,2\} \\ \Da \\ 6 & \{0,2\} & \{0,2\} & \{0,2\} & 2 & 2 & 2 & \{0,1\} & 0 & 0 \\ \Da \\ 6 & \{0,2\} & \{0,2\} & 0 & 2 & 2 & 2 & \{0,1\} & 0 & 0 \\ \Da \\ 6 & \{0,2\} & 0 & 0 & 2 & 2 & 2 & \{0,1\} & 0 & 0 \\ \Da \\ 6 & 0 & 0 & 0 & 2 & 2 & 2 & \{0,1\} & 0 & 0 \\ \Da \\ \xcancel{6} & 0 & 0 & 0 & 2 & 2 & 2 & 1 & 0 & 0 \\ = \\ 2 & 0 & 0 & 0 & 2 & 2 & 2 & 1 & 0 & 0 \\ \hline \end{array} \end{array} \)

Once we’ve invalidated every row that assumes 0 at |x|, reducing the indirect intuitionistic truth-table clears it, which means the formula is a tautology of IPL.

The proof of this follows from the direct intuitionistic truth-table procedure. When any column contains only 1- or 2-valued cells, it’s a tautology, because there is no cell (x,y) that satisfies the first criterion to validate the 1-valued cells, which forces us to delete them during the reduction stage of the direct method. That leaves only the 2-valued cells at |x|, which indicates a tautology for a formula via the direct method.

Optimization 3: Adding the Gilvenko Switch

We saw from the intuitionistic truth-table for the contradiction A∧¬A that it, too, evaluates to a fully 0-valued column deterministically, just as it does with classical truth-tables. However, direct intuitionistic truth-tables do not guarantee this for every contradiction.

\(\begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \to \neg A & \neg A \to A & c \wedge d \\ \hline 1 & 0 & 1:(b,6) & 1:(c,6) & 1:(d,5) & 0 \\ 2 & 0 & 1:(b,6) & 1:(c,6) & 2 & 0 \\ \xcancel{3} & 0 & 1:\emptyset & 2 & 1:(d,5) & 0 \\ \xcancel{4} & 0 & 1:\emptyset & 2 & 2 & 2 \\ 5 & 0 & 2 & 2 & 0 & 0 \\ 6 & 2 & 0 & 0 & 2 & 0 \\ \hline \end{array} \end{array}\)

The validation stage had to remove row 4 during the validation stage, and due to column a, not column e. Yet, when the deterministic classical valuations accompany the non-deterministic intuitionistic ones, the evaluation of the composite formula ends with the analogous Gilvenko switch, which justifies the reduction of row 4 before the validation stage begins:

\(\begin{array}{c} Validate~(with~Switch) \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & \neg A & A \to \neg A & \neg A \to A & c \wedge d \\ \hline 1 & [0,0] & [2,1] & [2,1] & [0,1] & [0,0] \\ 2 & [0,0] & [2,1] & [2,1] & [0,2] & [0,0] \\ 3 & [0,0] & [2,1] & [2,2] & [0,1] & [0,0] \\ \xcancel{4} & [0,0] & [2,1] & [2,2] & [0,2] & [0,\cancel{2}] \\ 5 & [0,0] & [2,2] & [2,2] & [0,0] & [0,0] \\ 6 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] \\ \hline \end{array} \end{array}\)

This Gilvenko switch allows us to remove all [0,1]- and [0,2]-valued rows for any column that is a classical contradiction, a classical contradiction being any column x where all cells (x,y) take the values [0,n∈{0,1,2}].

We can also use the Gilvenko switch during the build stage for any column of a direct intuitionistic truth-table, and it can perform mid-build revisions to any superformula containing the contradictory column, so long as every row for the contradictory column is filled. Thus, the known simplifications for falsum (⊥) and verum (⊤) apply:

\(\begin{array}{c|c} \begin{array}{rcl} \neg \bot & \equiv & \top \\ A \vee \bot & \equiv & A \\ \bot \vee B & \equiv & B \\ A \wedge \bot & \equiv & \bot \\ \bot \wedge B & \equiv & \bot \\ A \to \bot & \equiv & \neg A \\ \bot \to B & \equiv & \top \\ \end{array} & \begin{array}{rcl} \neg \top & \equiv & \bot \\ A \vee \top & \equiv & \top \\ \top \vee B & \equiv & \top \\ A \wedge \top & \equiv & A \\ \top \wedge B & \equiv & B \\ A \to \top & \equiv & \top \\ \top \to B & \equiv & B \\ \end{array} \end{array}\)

A column for ⊥ is a column where its every cell is [0,0], and a column for ⊤ is thus a column where its every cell is [2,2].

This Gilvenko switch works for indirect intuitionistic truth-tables only after failing to reintroduce a [2,_] row consistently for an intermediate column consisting only of [0,n∈{0,1,2}]. Instead of removing the intuitionistic 1-valued rows upon an inconsitent reintroduction, we remove the inconsistent attempted row (x,|y|+1) and all [0,1]- and [0,2]-valued rows at column x. Since the direct and indirect classical truth-table decision procedures are deterministic, it’s normally a much shorter check.

I’ll illustrate the indirect reintroduction stage for the switch with an example of the principle of explosion (A∧¬A)→B.

Here’s how it works directly:

\(\begin{array}{c} Build \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & \neg A & A \wedge \neg A & d \to B \\ \hline 1 & [0,0] & [0,0] & [2,1] & [0,0] & \\ 2 & [0,0] & [0,0] & [2,2] & [0,0] & \\ 3 & [2,2] & [0,0] & [0,0] & [0,0] & \\ \hline \end{array} \end{array}\)

\(\begin{array}{c} Switch~and~Simplify \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & \neg A & \bot & \top \\ \hline 1 & [0,0] & [0,0] & [2,1] & [0,0] & \\ 2 & [0,0] & [0,0] & [2,2] & [0,0] & \\ 3 & [2,2] & [0,0] & [0,0] & [0,0] & \\ \hline \end{array} \end{array}\)

And here’s how it works indirectly (tacitly skipping the deletion that would happen given the forced reassignment between (a,1) and (c,1)):

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & \neg A & A \wedge \neg A & d \to B \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [\{0,2\},\{0,2\}] & [0,0] & [\{0,2\},\{0,1,2\}] & [\{0,2\},2] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [0,0] & [\{0,2\},2] & [\{0,2\},2] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [0,0] & [0,2] & [\{0,2\},2] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [0,0] & [0,2] & [0,2] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [0,0] & [0,2] & [0,2] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & \neg A & A \wedge \neg A & d \to B \\ \hline \xcancel{1} & [2,2] & [0,0] & [0,2] & [0,2] & [2,0] \\ \hline 2 & [\{0,2\},\_] & [\{0,2\},\_] & [\{0,2\},\_] & [2,\_] & [\{0,2\},\_] \\ \Da \\ 2 & [\{0,2\},\_] & [\{0,2\},\_] & [\{0,2\},\_] & [2,\_] & [\{0,2\},\_] \\ \Da \\ 2 & [2,\_] & [\{0,2\},\_] & [2,\_] & [2,\_] & [\{0,2\},\_] \\ \Da \\ \xcancel{2} & [2,\_] & [\{0,2\},\_] & \cancel{[2,\_]}~[0,\_] & [2,\_] & [\{0,2\},\_] \\ \hline \end{array} \end{array}\)

We can further justify skipping contradiction checks for columns b and c, since they are columns for atomics and literals, and neither formula contains verum or falsum.

Optimization 4: Pre-Simplification

Pre-simplifying a formula applies the covered equivalencies, but in different orders:

• Those for negation simplify a formula in superformula-to-subformula order.

• Those for verum and falsum simplify a formula in subformula-to-superformula order.

We obviously simplify formulae containing verum and falsum to reduce the number of its operators and operands. Our doing so sometimes yields a simplified formula with no two common atomic formulae and neither verum nor falsum. If the simplification meets those three criteria for an independent formula, we can forgo any decision procedure. No IPL formulae with that syntactic structure are tautologies or contradictions.

The simplifications that push negations to literals are harder to justify. Two-thirds of the outputs of negations are non-deterministic in the intuitionistic truth-table, so double-negating every single atomic formula greatly increases the row count of the table we make in the decision procedure. But, there are still some advantages to this negation normal form. The main one is that it makes the indirect intuitionistic truth-table function better, so we can prevent the creation of many other rows by permitting more columns. Another is that all literal operands to binary formulae take the form A, ¬A, or ¬¬A. Because of this, we can exploit other known IPL equivalencies that simplify IPL formulae.

While there are infinitely many such equivalencies, we should at least check formulae with common-literal operands and a single binary operator, since they are available to check during a subformula-to-superformula simplification.

\(\def\eq{&\equiv&} \begin{array}{c} \text{Where }n\text{ is the number of negations comprising the literal} \dots \\\\ \begin{array}{c|c|c} \begin{array}{rcl} A_n \to A_n \eq \top \\ A_{n} \to A_{n+1} \eq A_{n+1} \\ A_{n+1} \to A_{n} \eq A_{n+2} \\ A_n \to A_{n+2} \eq \top \\ \end{array} & \begin{array}{rcl} A_n \vee A_n \eq A_n \\ A_{n} \vee A_{n+2} \eq A_{n+2} \\\\\\ \end{array} & \begin{array}{rcl} A_n \wedge A_n \eq A_n \\ A_{n} \wedge A_{n+1} \eq \bot \\ A_n \wedge A_{n+2} \eq A_n \\ \\ \end{array} \end{array} \end{array}\)

Involving more complex composite formulae for simplification invite some tradeoffs, though. There are vanishingly many returns on the number of unique simplifications as the complexity of composite formulae grows. At this one-binary-formula check for simplifications, 20 of the 23 formulae (discounting commutative equivalents) have simplifications, but this success rate plummets with two-binary-formulae, and it practically vanishes once it’s powerful enough to handle the real bugbears of IPL (e.g., ((A→B)→A)∧¬B≡¬¬A∧¬B). Where that tradeoff lies is more an empirical than proof- or model-theoretic question, and there is already plenty of sequent-based IPL solver research on that topic, so I will forgo it here.

Implementation and Appendix

Leme built an implementation for his and others’ intuitionistic truth-tables in Coq, but I’ll be partly translating that and implementing these ideas in Go, since I’m interested in implementing such tables into a compiler for a programming language where true, false, and unsure are logical primitives whose truth-values and control flow obey the proved-disproved-unproved triad as Brouwer described it. That work is forthcoming, but I’ll place the link to the code for that decision procedure here.

Some additional tables below utilize all of the optimizations to let readers of both papers compare the direct method against the indirect method, and to invite complexity theorists to flesh out what proofs that they may want for these optimizations in that domain. The selected tautologies⁴ are equivalent to a standard Hilbert axiomatization of IPL, as well, so any future additions to this appendix will only cover IPL non-tautologies of common interest.

A→(B→A) — Weakening

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|} \hline & a & b & c & d \\ \hline & A & B & B \to A & A \to c \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1\}] & [\{0,2\},0] \\ \Da \\ \xcancel{1} & [2,2] & [\{0,2\},\{0,2\}] & \cancel{[\{0,2\},\{0,1\}]}~[\{0,2\},2] & [\{0,2\},0] \\ \hline \end{array} \end{array} \)

(A→(B→C))→(B→(A→C)) — Permutation

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [0,0] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1\}] & [\{0,2\},2] & [\{0,2\},\{0,1\}] & [\{0,2\},0] \\ \Da \\ 1 & [\{0,2\},\{0,2\}] & [0,0] & [0,0] & [2,\{1,2\}] & [\{0,2\},\{0,1\}] & [2,2] & [2,1] & [2,0] \\ 2 & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,2] & [2,0] & [2,0] \\ \Da \\ 1 & [0,0] & [0,0] & [0,0] & [2,\{1,2\}] & [2,1] & [2,2] & [2,1] & [2,0] \\ 2 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [2,2] & [2,1] & [2,0] \\ 3 & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,2] & [2,0] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline 1 & [0,0] & [0,0] & [0,0] & [2,\{1,2\}] & [2,1] & [2,2] & [2,1] & [2,0] \\ 2 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [2,2] & [2,1] & [2,0] \\ 3 & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,2] & [2,0] & [2,0] \\ \Da \\ 1 & [0,0] & [0,0] & [0,0] & [2,1] & [2,1] & [2,2] & [2,1] & [2,0] \\ 2 & [0,0] & [0,0] & [0,0] & [2,2] & [2,1] & [2,2] & [2,1] & [2,0] \\ 3 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [2,2] & [2,1] & [2,0] \\ 4 & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,2] & [2,0] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline 1 & [0,0] & [0,0] & [0,0] & [2,1]:(d,4) & [2,1]:(e,3) & [2,2] & [2,1]:(g,4) & [2,0] \\ 2 & [0,0] & [0,0] & [0,0] & [2,2] & [2,1]:(e,3) & [2,2] & [2,1]:\emp & [2,0] \\ 3 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [2,2] & [2,1]:\emp & [2,0] \\ 4 & [0,0] & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,2] & [2,0] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline \xcancel{2} & [0,0] & [0,0] & [0,0] & [2,2] & [2,1]:(e,3) & [2,2] & [2,1]:\emp & [2,0] \\ \hline 5 & [\_,\{0,2\}] & [\_,2] & [\_,2] & [\_,2] & [\_,\{0,1\}] & [\_,2] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{5} & [\_,\{0,2\}] & [\_,2] & [\_,2] & [\_,2] & \cancel{[\_,\{0,1\}]}~[\_,2] & [\_,2] & [\_,0] & [\_,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline \xcancel{3} & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [2,2] & [2,1]:\emp & [2,0] \\ \hline 6 & [\_,2] & [\_,2] & [\_,2] & [\_,2] & [\_,\{0,1\}] & [\_,2] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{6} & [\_,2] & [\_,2] & [\_,2] & [\_,2] & \cancel{[\_,\{0,1\}]}~[\_,2] & [\_,2] & [\_,0] & [\_,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline \xcancel{4} & [0,0] & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,2] & [2,0] & [2,0] \\ \hline 7 & [\_,2] & [\_,2] & [\_,0] & [\_,0] & [\_,0] & [\_,2] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{7} & [\_,2] & [\_,2] & [\_,0] & [\_,0] & [\_,0] & \cancel{[\_,2]}~[\_,0] & [\_,0] & [\_,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & B \to C & A \to C & A \to d & B \to e & f \to g \\ \hline \xcancel{1} & [0,0] & [0,0] & [0,0] & [2,1]:\emp & [2,1]:\emp & [2,2] & [2,1]:\emp & [2,0] \\ \hline \xcancel{8} & [\_,0] & [\_,2] & [\_,0] & [\_,0] & [\_,1] & [\_,2] & [\_,0] & [\_,0] \\ = \\ 4 & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,2] & [2,0] & [2,0] \\ \hline \end{array} \end{array} \)

(A→(A→B))→(A→B) — Conditional Contraction

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & (A \to c) & d \to c \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [\{0,2\},\{0,2\}] & [0,0] & [\{0,2\},\{0,1\}] & [\{0,2\},2] & [\{0,2\},0] \\ \Da \\ 1 & [0,0] & [0,0] & [2,1] & [2,2] & [2,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & (A \to c) & d \to c \\ \hline 1 & [0,0] & [0,0] & [2,1]:\emp & [2,2] & [2,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \to B & (A \to c) & d \to c \\ \hline \xcancel{1} & [0,0] & [0,0] & [2,1]:\emp & [2,2] & [2,0] \\ \hline 2 & [\_,2] & [\_,0] & [\_,0] & [\_,2] & [\_,0] \\ \Da \\ \xcancel{2} & [\_,2] & [\_,0] & [\_,0] & \cancel{[\_,2]}~[\_,0] & [\_,0] \\ \hline \end{array} \end{array} \)

(A→B)→((B→C)→(A→C)) — Conditional Transitivity

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [0,0] & [\{0,2\},2] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,1\}] & [\{0,2\},\{0,1\}] & [\{0,2\},0] \\ \Da \\ 1 & [0,0] & [\{0,2\},\{0,2\}] & [0,0] & [2,2] & [\{0,2\},\{0,1,2\}] & [2,1] & [\{0,2\},\{0,1\}] & [\{0,2\},0] \\ 2 & [2,2] & [2,2] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,0] \\ \Da \\ 1 & [0,0] & [0,0] & [0,0] & [2,2] & [2,\{1,2\}] & [2,1] & [2,\{0,1\}] & [2,0] \\ 2 & [0,0] & [2,2] & [0,0] & [2,2] & [0,0] & [2,1] & [2,1] & [2,0] \\ 3 & [2,2] & [2,2] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline 1 & [0,0] & [0,0] & [0,0] & [2,2] & [2,\{1,2\}] & [2,1] & [2,\{0,1\}] & [2,0] \\ 2 & [0,0] & [2,2] & [0,0] & [2,2] & [0,0] & [2,1] & [2,1] & [2,0] \\ 3 & [2,2] & [2,2] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,0] \\ \Da \\ 1 & [0,0] & [0,0] & [0,0] & [2,2] & [2,1] & [2,1] & [2,1] & [2,0] \\ 2 & [0,0] & [0,0] & [0,0] & [2,2] & [2,2] & [2,1] & [2,0] & [2,0] \\ 3 & [0,0] & [2,2] & [0,0] & [2,2] & [0,0] & [2,1] & [2,1] & [2,0] \\ 4 & [2,2] & [2,2] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline 1 & [0,0] & [0,0] & [0,0] & [2,2] & [2,1]:(e,3) & [2,1]:(f,4) & [2,1]:(g,2) & [2,0] \\ 2 & [0,0] & [0,0] & [0,0] & [2,2] & [2,2] & [2,1]:\emp & [2,0] & [2,0] \\ 3 & [0,0] & [2,2] & [0,0] & [2,2] & [0,0] & [2,1]:Skip! & [2,1]:\emp & [2,0] \\ 4 & [2,2] & [2,2] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline \xcancel{2} & [0,0] & [0,0] & [0,0] & [2,2] & [2,2] & [2,1]:\emp & [2,0] & [2,0] \\ \hline 5 & [\_,2] & [\_,2] & [\_,0] & [\_,2] & [\_,2] & [\_,0] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{5} & [\_,2] & [\_,2] & [\_,0] & [\_,2] & \cancel{[\_,2]}~[\_,0] & [\_,0] & [\_,0] & [\_,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline \xcancel{3} & [0,0] & [2,2] & [0,0] & [2,2] & [0,0] & [2,1]:Skip! & [2,1]:\emp & [2,0] \\ \hline 6 & [\_,\{0,2\}] & [\_,2] & [\_,2] & [\_,2] & [\_,2] & [\_,\{0,1\}] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{6} & [\_,\{0,2\}] & [\_,2] & [\_,2] & [\_,2] & [\_,2] & \cancel{[\_,\{0,1\}]}~[\_,2] & [\_,0] & [\_,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline \xcancel{4} & [2,2] & [2,2] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,0] \\ \hline 7 & [\_,2] & [\_,2] & [\_,2] & [\_,2] & [\_,2] & [\_,\{0,1\}] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{7} & [\_,2] & [\_,2] & [\_,2] & [\_,2] & [\_,2] & \cancel{[\_,\{0,1\}]}~[\_,2] & [\_,0] & [\_,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \to B & B \to C & A \to C & e \to f & d \to g \\ \hline \xcancel{1} & [0,0] & [0,0] & [0,0] & [2,2] & [2,1]:\emp & [2,1]:\emp & [2,1]:\emp & [2,0] \\ \hline \xcancel{8} & [\_,0] & [\_,0] & [\_,0] & [\_,2] & [\_,2] & [\_,1] & [\_,0] & [\_,0] \\ = \\ 2 & [0,0] & [0,0] & [0,0] & [2,2] & [2,2] & [2,1] & [2,0] & [2,0] \\ \hline \end{array} \end{array} \)

(A∨B)→((A→C)→(C∨B)) — Disjunctive Distribution

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \vee B & A \to C & C \vee B & e \to f & d \to g \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1] & [2,0] \\ \hline \end{array} \end{array}\)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \vee B & A \to C & C \vee B & e \to f & d \to g \\ \hline 1 & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|c|c|c|} \hline & a & b & c & d & e & f & g & h \\ \hline & A & B & C & A \vee B & A \to C & C \vee B & e \to f & d \to g \\ \hline \xcancel{1} & [2,2] & [0,0] & [0,0] & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,0] \\ \hline 2 & [\_,2] & [\_,0] & [\_,0] & [\_,2] & [\_,0] & [\_,0] & [\_,0] & [\_,0] \\ \Da \\ \xcancel{2} & [\_,2] & [\_,0] & [\_,0] & [\_,2] & [\_,0] & [\_,0] & \cancel{[\_,0]}~[\_,\{1,2\}] & [\_,0] \\ \hline \end{array} \end{array}\)

(A∨A)→A — Disjunctive Contraction

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|} \hline & a & b & c \\ \hline & A & A \vee A & b \to A \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [0,0] & [0,2] & [0,0] \\ \Da \\ \xcancel{1} & [0,0] & \cancel{[0,2]}~[0,0] & [0,0] \\ \hline \end{array} \end{array}\)

A→(A∨B) — Addition

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|} \hline & a & b & c & d \\ \hline & A & B & A \vee B & A \to c \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [\{0,2\},\{0,2\}] & [0,0] & [\{0,2\},0] \\ \Da \\ \xcancel{1} & [2,2] & [\{0,2\},\{0,2\}] & \cancel{[\{0,2\},0]}~[\{0,2\},2] & [\{0,2\},0] \\ \hline \end{array} \end{array} \)

(A∧B)→A — Simplification

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|} \hline & a & b & c & d \\ \hline & A & B & A \wedge B & e \to A \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [0,0] & [\{0,2\},\{0,2\}] & [\{0,2\},2] & [\{0,2\},0] \\ \Da \\ \xcancel{1} & [0,0] & [\{0,2\},\{0,2\}] & \cancel{[\{0,2\},2]}~[\{0,2\},0] & [\{0,2\},0] \\ \hline \end{array} \end{array} \)

A→(B→(A∧B)) — Conjunction

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} (Indirectly)~Build \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \wedge B & B \to c & A \to d \\ \hline 1 & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1,2\}] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,2\}] & [\{0,2\},\{0,1\}] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [\{0,2\},\{0,2\}] & [\{0,2\},0] & [\{0,2\},\{0,1\}] & [\{0,2\},0] \\ \Da \\ 1 & [2,2] & [0,0] & [0,0] & [2,1] & [2,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \wedge B & B \to c & A \to d \\ \hline 1 & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,0] \\ \hline \end{array} \end{array} \)

\(\def\Da{\Downarrow} \def\emp{\emptyset} \begin{array}{c} Reintroduce~and~Validate \dots \\ \begin{array}{|c|c|c|c|c|c|} \hline & a & b & c & d & e \\ \hline & A & B & A \wedge B & B \to c & A \to d \\ \hline \xcancel{1} & [2,2] & [0,0] & [0,0] & [2,1]:\emp & [2,0] \\ \hline 2 & [\_,2] & [\_,2] & [\_,0] & [\_,0] & [\_,\{0,1,2\}] \\ \Da \\ \xcancel{2} & [\_,2] & [\_,2] & \cancel{[\_,0]}~[\_,2] & [\_,0] & [\_,\{0,1,2\}] \\ \hline \end{array} \end{array} \)

If the subjects of logic, linguistics, programming, and their interplay interest you, I encourage you to subscribe here:

If you’d like to comment on this post, feel free:

1. Some texts refer to such decision procedures as “deterministically compositional”. I borrow the jargon instead from linguistic syntax, where parsing is the process of recursively breaking up a sentence into its immediate child nodes to form a syntax tree, halting at defined terminal nodes, whereas synthesis is the process of building up a syntax tree from its terminal nodes to the constituent whole. In computer science, the nomenclature is even more confusing, since synthesis is often called “bottom-up parsing”.

2. This is not to say parsing decision procedures cannot work under such constraints. Rather, the storage of the remaining open branches of a tableau would be onerous for something as basic as model searches.

3. Transforming an IPL formula to its S4 modal companion and using the simplified or full Grätzean tables offers neither a more efficient nor a simpler IPL decision procedure, due to the sheer number of boxes that the translation entails and that the Grätzean tables have more non-deterministic outputs (7) than the intuitionistic truth-tables do (6).

4. I omit the indirect truth-table for Disjunctive Distribution for the right disjunct — (A∨B)→((B→C)→(A∨C)) — because it’s repetitive. I also omit the Explosion — ⊥→A — because I covered it in sufficient detail prior to this appendix and because it pre-simplifies to ⊤.