Buddhist Four-Fold Logic (Catuṣkoṭi) with Lean 4

I've been reading Graham Priest's The Fifth Corner of Four: An Essay on Buddhist Metaphysics, which is a beautiful book, and I thought it would be fun to formalize some of his ideas in an automated theorem prover.

Classical logic operates on a strict dichotomy: statements are either True or False. However, some philosophical traditions, notably Buddhist logic utilize a larger framework known as the Catuṣkoṭi (चतुष्कोटि in Sanskrit), translated as the "four corners" or "tetralemma".

This framework suggests that for a given proposition (P), there might be four possibilities regarding its status:

1. It is: P is true.
2. It is not: P is false (or ¬P is true).
3. It is and is not: P is simultaneously true and false (P ∧ ¬P). This often applies to paradoxical situations or descriptions of phenomena that defy simple categorization.
4. It is neither nor is not: P is neither true nor false (¬(P ∨ ¬P)). This can apply to questions with invalid premises (e.g., "Is the present King of France bald?"), concepts considered transcendent or beyond conventional predication (like the ultimate nature of reality, śūnyatā), or situations where the categories of true/false simply don't apply.

For brevity, we will use the following abbreviations:

• T = is
• F = isNot
• B = isAndIsNot
• N = neitherIsNorIsNot

It's important to note that in Buddhist logic, is not necessarily proposing these are all "true" in the conventional sense simultaneously, but rather serves as an analytical tool to explore the limits of concepts, language, and dichotomous thinking, especially when examining the ultimate nature of phenomena.

Unlike classical logic which treats contradictions as logical errors to be avoided, the Buddhist framework handles "contradictions" and "category errors" as first class citizens in the logical system. The third state (isAndIsNot) explicitly acknowledges contradictory situations where something can simultaneously be and not be, while the fourth state (neitherIsNorIsNot) provides a formal way to represent category errors or questions that transcend the binary true/false distinction. This approach allows Buddhist logic to reason about paradoxes, ineffable concepts, and statements with faulty presuppositions in a structured way, rather than simply rejecting them as invalid or meaningless.

By incorporating these traditionally problematic states directly into the logical framework, Buddhist logic offers an interesting approach to reasoning that can accommodate the complexities and ambiguities often encountered in philosophical discourse, particularly when discussing ultimate reality, consciousness, or other phenomena that resist conventional categorization or involve meta-language.

Analyzing the algebraic structure formed by the set of truth values \(S = \{T, F, B, N\}\) under the operations of Negation (\(¬ᵇ\)), Conjunction (\(∧ᵇ\)), and Disjunction (\(∨ᵇ\)), we find several key characteristics. The conjunction \(∧ᵇ\) and disjunction \(∨ᵇ\) operations satisfy the necessary properties (commutativity, associativity, idempotency, absorption) to establish that \((S, ∧ᵇ, ∨ᵇ)\) forms a lattice. Furthermore, this lattice is bounded, possessing a bottom element \(\bot = F\) and a top element \(\top = T\), as evidenced by the identities \(F ∧ᵇ x = F\), \(F ∨ᵇ x = x\), \(T ∧ᵇ x = x\), and \(T ∨ᵇ x = T\).

The interactions between the elements under \(∧ᵇ\) (specifically \(N ∧ᵇ B = N\), \(N ∧ᵇ T = N\), \(B ∧ᵇ T = B\)) reveal a total ordering rather than the diamond shape of some other four-valued logics like Belnap-Dunn's. The resulting lattice structure is actually a simple chain: \(F ≤ N ≤ B ≤ T\), where \(∧ᵇ\) corresponds to taking the minimum element according to this order.

A notable feature of this particular lattice is that the operations induce a total order, or chain, among the elements: \(F < N < B < T\). This linear ordering implies that the lattice is necessarily distributive, satisfying laws such as \(A ∧ᵇ (B ∨ᵇ C) = (A ∧ᵇ B) ∨ᵇ (A ∧ᵇ C)\). The meet (\(∧ᵇ\)) corresponds to taking the minimum element in this chain, and the join (\(∨ᵇ\)) corresponds to taking the maximum.

When considering the negation operation \(¬ᵇ\), we observe it acts as an involution, satisfying \(¬ᵇ(¬ᵇ A) = A\) for all elements \(A\) in the set. However, this involution does not serve as a proper complement operation for the lattice. While \(T\) and \(F\) are complements of each other under \(¬ᵇ\), the elements \(B\) and \(N\) are fixed points of the negation (\(¬ᵇ B = B\) and \(¬ᵇ N = N\)). Consequently, neither \(B\) nor \(N\) has a complement, as neither \(B ∧ᵇ B = F\) nor \(N ∧ᵇ N = F\) holds. The lattice is therefore not complemented.

Because the lattice lacks complements for all elements, it cannot be classified as a Boolean algebra. Additionally, despite having an involution, the structure fails to satisfy De Morgan's laws. For instance, \(¬ᵇ(B ∧ᵇ N) = ¬ᵇ(N) = N\), whereas \((¬ᵇ B) ∨ᵇ (¬ᵇ N) = B ∨ᵇ N = B\). Since \(N \ne B\), De Morgan's laws do not hold universally, and thus the structure \((S, ∧ᵇ, ∨ᵇ, ¬ᵇ)\) is also not a De Morgan algebra.

One interesting aspect of four-valued logic is how it handles the principle of explosion (ex falso quodlibet). In classical logic, from a contradiction, anything follows—once you accept both P and ¬P as true, you can derive any arbitrary statement. But in our Catuṣkoṭi system, contradictions are explicitly represented by the isAndIsNot state and contained within the logical framework itself. This effectively "tames" the explosion by giving contradictions a stable truth value (B) rather than letting them collapse the entire system. Compare this also to the much-studied paraconsistent logics, which allow some contradictory statements to be proven without affecting the truth value of (all) other statements

This four-valued logic defines a specific algebraic structure: a four-element, bounded, distributive lattice forming a chain, equipped with an involutive unary operator that fails both complementation and De Morgan's laws for certain elements. We can represent these four distinct logical states using Lean inductive type feature. This allows us to define a type BState (for Buddhist State) that has exactly four possible constructors, corresponding to the four corners of the Catuṣkoṭi.

Here is the Lean module that runs in the Lean Live editor.

namespace BLogic

inductive BState where
  | is | isNot | isAndIsNot | neitherIsNorIsNot
  deriving Repr, DecidableEq, Inhabited

Here, is, isNot, isAndIsNot, and neitherIsNorIsNot are the unique constructors for our BState type. The deriving clause automatically generates useful helper functions: Repr for a printable representation, DecidableEq to allow equality checks (==), and Inhabited to provide a default value if needed.

To work with these states more easily and print results, we define a function to convert a BState value into a descriptive string. We then create a ToString instance, which tells Lean how to automatically convert BState values to strings when needed (e.g., during printing).

def bStateToString (state : BState) : String :=
  match state with
  | .is                => "It is"
  | .isNot             => "It is not"
  | .isAndIsNot        => "It is and is not"
  | .neitherIsNorIsNot => "It is neither nor is not"

instance : ToString BState where
  toString := bStateToString

How does negation work in this system? While classical logic simply flips True to False and vice-versa, defining negation for the isAndIsNot and neitherIsNorIsNot states requires an interpretation. Here's a plausible approach:

• Negating "Is" yields "Is Not".
• Negating "Is Not" yields "Is".
• Negating the paradoxical "Is And Is Not" state yields itself (negating a paradox might still be paradoxical).
• Negating the inapplicable "Neither Is Nor Is Not" state also yields itself (negating inapplicability might still result in inapplicability).

We implement this negation function as bNeg and define a convenient prefix notation ¬ᵇ for it.

def bNeg (state : BState) : BState :=
  match state with
  | BState.is                => BState.isNot
  | BState.isNot             => BState.is
  | BState.isAndIsNot        => BState.isAndIsNot
  | BState.neitherIsNorIsNot => BState.neitherIsNorIsNot

prefix:75 "¬ᵇ " => bNeg

A fundamental property in classical logic is the law of double negation: ¬(¬P) is equivalent to P. Does this hold true in our four-valued Catuṣkoṭi system with our defined negation ¬ᵇ? We can use Lean's theorem proving capabilities to verify this.

We state the theorem: for any state s of type BState, applying our negation twice (¬ᵇ (¬ᵇ s)) results in the original state s.

theorem b_double_negation (state : BState) :
    ¬ᵇ (¬ᵇ state) = state := by
  cases state
  all_goals simp [bNeg]

end BLogic

The proof proceeds as follows:

1. cases state: Since BState is an inductive type, this tactic breaks the proof down into four separate goals, one for each possible constructor (is, isNot, isAndIsNot, neitherIsNorIsNot). We must prove the property holds for each case.
2. all_goals simp [bNeg]: This command applies the simp tactic to all generated sub-goals. The simp [bNeg] part tells the simplifier to unfold the definition of our negation function (bNeg). For each specific case (e.g., when state is BState.is), simp calculates the result of the double negation (¬ᵇ (¬ᵇ BState.is) becomes ¬ᵇ BState.isNot, which becomes BState.is) and sees that it equals the right-hand side of the equation (BState.is). It verifies this for all four cases.

Lean confirms that the property ¬ᵇ (¬ᵇ state) = state holds true for all possible values within our formalized system, given our definition of negation.

The truth tables for the four operations defined on the BState type are as follows:

Negation (¬ᵇ)

Conjunction (AND - ∧ᵇ)

Disjunction (OR - ∨ᵇ)

Exclusive OR (XOR - ⊕ᵇ)

Finally, let's derive the truth table for material implication (denoted \(P → Q\)) in this specific four-valued logic. The standard definition in classical logic is \(P → Q \equiv \neg P \lor Q\). We will apply this definition using our previously defined negation (\(¬ᵇ\)) and disjunction (\(∨ᵇ\)) operations for the states \(S = \{T, F, B, N\}\).

We need to calculate \(¬ᵇ P ∨ᵇ Q\) for all 16 combinations of P and Q.

• When the antecedent \(P\) is False (F), the implication is always True (T), mirroring classical logic.
• When the antecedent \(P\) is True (T), the implication takes the value of the consequent \(Q\), also mirroring classical logic.
• When the antecedent \(P\) is Both (B) or Neither (N), the result is more complex, often reflecting the value of \(P\) or \(Q\) based on the disjunction table, but notably yielding True (T) when the consequent \(Q\) is True (T).

Of course, all this is just for fun, but it does make one wonder about "practical" applications. Perhaps if the engineers down at Intel could just isolate that elusive 'paradoxium' or 'maybe-silicon' semiconductor—one that isn't strictly 'on' or 'off' but can also be 'both on and off' and 'neither on nor off'—we could finally build truly enlightened circuits. Imagine logic gates that escape the cycle of suffering, refusing to commit to a definite state, or processors that handle infinite loops not as errors but as just empheremal passing states.