Tetralemma: a type theoretic perspective

[yeshe.tenley]

Continuing the discussion from Anatta: type theory, formal logic and mathematics can help us understand each other better:

@axkirillov

Can we have new one about the tetralema though? Cause I’m intrigued.

Abstract

The tetralemma is not a problem from the type-theoretic perspective. Especially not how it was used by the Teacher where all four corners were denied in many cases. The tetralemma is difficult to reconcile if you harbor one underlying axiom, but people often fail to grasp that this axiom is not necessary. Here we analyze the Tetralemma from a type theoretic perspective using the curry-howard isomorphism to shed light on this hidden axiom and provide a new perspective on the catuṣkoṭi.

Discussion

Recall the discussion here by way of introduction. The four “corners” of the catuṣkoṭi in type-theoretic form are:

1. Corner #1 P
   An inhabitant of P is a “proof” of P.

2. Corner #2 ¬P
   An inhabitant of ¬P is a function f:P→⊥.

3. Corner #3 P∧¬P
   An inhabitant is a pair (p,f) with p:P and f:P→⊥.

   • This directly gives a contradiction, because applying f to p yields ⊥.
   • So in a consistent system, #3 has no inhabitants.

4. Corner #4 ¬(P∨¬P)
   An inhabitant of #4 is a function g ⁣:[P+(P→⊥)] → ⊥.

Where P is a type/proposition. Let’s look at some details:

• inhabit: a type is said to be inhabited if there exists one or more terms of that type. The type of irrational numbers is inhabited by the number pi for instance. The number pi is a term of type ‘irrational number.’ In proof-theoretic language we say a term inhabiting a type is a proof of that type. The number pi is a proof that the type of irrational numbers is inhabited.

• ¬P is inhabited means you have a function P→⊥ that turns proposed inhabitants of P into absurdity/contradiction.

• P∧¬P is inhabited means you simultaneously have a valid proof for P and a function turning any valid proof of P into ⊥; that yields a direct contradiction.

• ¬(P∨¬P) is inhabited means you have a function (P∨¬P)→⊥ ; i.e.\ “if someone gives me either a proof of P or a proof of ¬P, I can produce a contradiction."

Crucially, it can be the case that none of these types is inhabited. For a type not to be inhabited means that no term has been constructed as a “proof” for that type. In the case of the catuṣkoṭi, to deny the four corners is just to say that no proof has been constructed that inhabits any of those four types.

A crucial subtlety in constructive type theory is the difference between:

1. Simply lacking a proof of P (or ¬P, etc.), which is a state of ignorance.
2. Actually proving that P is uninhabited, i.e. constructing a term of type P→⊥.

In plain english, lacking a proof is weaker than having a refutation.

Hidden Axiom: So then why does this trip so many people up? The problem is with an underlying axiom that most take for granted. Here it is:

• ∀(P:Prop), P+(P→⊥).

For all propositions of type P, either P must be inhabited or P→⊥ must be inhabited. When this axiom is adopted, then denying all four corners of the tetralemma becomes problematic. Why? Because it automatically makes it so that either corner #1 OR corner #2 MUST be inhabited.

This axiom has a name that you’ve probably heard of before: LEM (the Law of the Excluded Middle) It is this axiom that makes it so difficult to understand the catuṣkoṭi because so many people just assume it to be the case.

Four ways to deny the four corners

So what could it mean to deny the four corners? I can think of four possible explanations:

1. Constructive ignorance (no proofs in either direction)
   You have no inhabitant for each corner, but also no proof that each corner is impossible. This is a benign, non-contradictory state of affairs in ordinary constructive type theory. This is not a problem because LEM is simply not assumed as an axiom.

2. Rejection of LEM
   Denying the four corners could imply that you don’t assume LEM and for the purposes of the P under discussion pointing out that a logic with LEM does not handle that particular P well. It could mean that you find P so ill-defined as to be impossible to treat with a formal logical system that includes LEM.

3. Alternative type-theoretic representation
   It is also possible to give an alternative type-theoretic representation where ¬P is not defined as function turning P into an absurdity. This would break the curry-howard isomorphism, but it is possible. In this representation, ¬P would be considered a “thing” and not a function. Combined with LEM you would still get a classical logic. It could be that this was the ancient indian form of logic (and there is some evidence this is the case) in which case a denial of the four corners would be a rejection of this logical system much like #2.

4. Paraconsistent logic
   Denying the four corners could indicate that you are using a multi-valued logical system and advocating for a fifth corner. This is an avenue explored by Graham Priest in many papers.

Conclusion

We’ve (hopefully) given a formal type-theoretic grounding for discussions of the tetralemma to ground further debate so as to mitigate risks of talking past each other.

[Vaddha]

@yeshe.tenley

• Corner #2 ¬P
  An inhabitant of ¬P is a function f:P→⊥.

I don’t think this is the one in the Āgama/Nikāya literature.

@yeshe.tenley

Alternative type-theoretic representation

I think this is closer.

For example:

1. The universe is bounded/limited.
2. The universe is unbounded/unlimited.
3. The universe is both.
4. The universe is neither.

A concrete example of #3 is that the universe is boundless horizontally but limited in space vertically. This doesn’t make sense if #3 is a contradiction. I take it rather to be referring to parts or aspects.

Entirely P. Entirely opposite of P. Mix. Neither.

Another example would be

1. The soul and body are identical
2. the soul and body are different

The Buddha does deny that they are identical (see SN 12.36). But that is not equal to proposition 2, which is a separate idea. He also denies (negates) that. Meaning that if non-identity of soul and body were simply the negation of their identity, then the Buddha would have declared the second point. But he denies both.

Unless I’ve misunderstood the logic language.

[yeshe.tenley]

Hello Venerable!

@Vaddha

@yeshe.tenley

• Corner #2 ¬P
  An inhabitant of ¬P is a function f:P→⊥.

I don’t think this is the one in the Āgama/Nikāya literature.

@yeshe.tenley

Alternative type-theoretic representation

I think this is closer.

I also share this hypothesis, but the evidence is weak I’m afraid. I haven’t found anything that is completely convincing.

@Vaddha

For example:

1. The universe is bounded/limited.
2. The universe is unbounded/unlimited.
3. The universe is both.
4. The universe is neither.

A concrete example of #3 is that the universe is boundless horizontally but limited in space vertically. This doesn’t make sense if #3 is a contradiction. I take it rather to be referring to parts or aspects.

Ah, but the confusion here is about not clearly defining propositions and predicates. To adopt the third corner I think in just about every instance would be a critique of the ill-defined proposition/predicates.

The above is using a vague or multi-aspect notion of boundedness, effectively referencing different predicates that shift meaning across contexts/dimensions. That may not be a contradiction but a matter of changing the proposition from P to P1, P2,… So adopting #3 here would be a way of vaguely pointing out that the predicates are shifting or ill-defined.

In translating human speech representing propositions and so on into formal language careful attention needs to be paid to getting the propositions and predicates (both stated and unstated) correct.

It would be good to look at cases where the Teacher specifically adopts one of the four corners and put them into formal language to draw out what he may have intended.

[yeshe.tenley]

@Vaddha

Another example would be

1. The soul and body are identical
2. the soul and body are different

The Buddha does deny that they are identical (see SN 12.36).

Let P be #1.
Let #2 be ¬P; f :P→⊥.

These are the two corners. Four possibilities as I stated in the OP:

1. Normal constructive logic says that neither #1 or #2 has been demonstrated or inhabited. No valid “proof” has been given for either. This is not a problem much less a contradiction.
2. It could be a straightforward rejection of LEM with an implicit critique of the ill-defined P. P assumes the existence of two predicates: body and soul and the proofs for them have not been demonstrated or inhabited.
3. Alternative rejection of LEM where #2 is not a function, but a “thing” and pointing out that the system of logic doesn’t deal with it well much like the above.
4. Pointing at a multi-valued logic.

It is important to note that the Teacher doesn’t deny the two corners here. He says that if someone were to assume one of these two corners was inhabited there would be, “no living of the spiritual life.” That is what I think he means by ‘view’ here. That in the absence of proof you assume that one of the two corners must be inhabited. Without first overturning that assumption one can not set out on the spiritual life.

Whaddya think?

[thistle]

Thanks for the input. It certainly is interesting.

@yeshe.tenley

In translating human speech representing propositions and so on to formal language careful attention needs to be paid to getting the propositions and predicates (both stated and unstated) correct.

But isn’t that the problem in the first place? That when trying to map formal language to natural language, you’ll end up having to define every notion to the nth degree? I’m having difficulties to see how it can be applied to discussing anatta- atta. Predicates are legion.

[yeshe.tenley]

@thistle

But isn’t that the problem in the first place? That when trying to map formal language to natural language, you’ll end up having to define every notion to the nth degree? I’m having difficulties to see how it can be applied to discussing anatta- atta. Predicates are legion.

Disagreements or misunderstandings often arise when making logical arguments in natural language because multiple predicates or context shifts get conflated into a single proposition.

As you alluded to one can certainly get caught in an infinite regress of definitions with natural language translation. It is also true that translations will be context dependent - cultural, historical, situational.

However, we can still choose a finite slice of discourse - a particular sutta or point of doctrine - and try to translate just that piece into formal language to suss out the subtleties or locate any non-shared assumptions.

In practice, a layered approach is often taken—defining some concepts more rigorously, leaving others as partially open parameters, and acknowledging that certain aspects exceed neat formalization.

[christie]

@yeshe.tenley

An inhabitant of ¬P is a function f:P→⊥.

With all due respect, I don’t believe this is what the Buddha meant.

Using a different notation scheme, my interpretation would be

Let p = {the notion of a self}

Assertion: p = sum(a) + sum(b) + sum(c) + sum(d) + sum(e)

Let the symbol ‘0’ denote annihilation, or cessation

Let p⁰ = nibbāna(p)

If we use the symbol != to denote inequality,

Then the Buddha claims

(p⁰ → 0) != p (this is clear because p⁰ != p)
(p⁰ → 0) != (p → 0) (the progress of p⁰ is different from p, again because p⁰ != p)
(p⁰ → 0) != p & (p → 0) (this is not as silly as it sounds, the Buddha is disclaiming the quantum superposition of p and (p → 0))
(p⁰ → 0) != p | (p → 0) (this is also not silly, the Buddha is claiming neither p nor (p → 0) exist in alternate universes)

where → is “becomes”, & is logical AND, | is logical OR

It is important to note → denotes a process, so (p → 0) is not just 0 but the resultant state from the process, which is the cessation of p. The process itself could generate other artefacts and I think that is the question - the Buddha has never articulated what these artefacts may be, or if they exist at all. He suggested that it is unproductive to speculate on the process.

[Radius]

I know the scholarly explorations are important, and yet…

@Viveka

There is an expectation in our culture that intellect alone can surmount this and that if knowledge and logic are powerful enough everything can be understood. Now the Buddha explicitly said that this did not apply to the Dhamma.

[yeshe.tenley]

@christie

@yeshe.tenley

An inhabitant of ¬P is a function f:P→⊥.

With all due respect, I don’t believe this is what the Buddha meant.

Since the type-theoretic interpretation is very new (20th century) this would not surprise me

This comes from the type-theoretic interpretation of logic via the curry-howard isomorphism. The curry-howard isomorphism is a fabulous result that provides a map between different formal languages: type theory, mathematics, and logic. You can think of it as a kind of rosetta stone. The direct implication of the isomorphism is that computer science, mathematics and logic share very deep connections or are all aspects of the same underlying human conceptual framework.

So you can’t just deny or get rid of the negation type without giving it a replacement or you risk breaking your logic system into something that is unsound, trivial or inconsistent.

I alluded to this in the OP when talking about #3 an alternative type-theoretic representation that replaces the negation function with a “thing” + LEM. This breaks the isomorphism but would maybe provide something like a classical logic.

Is that what you intend by saying the above?

@christie

Using a different notation scheme, my interpretation would be

Let p = {the notion of a self}

Assertion: p = sum(a) + sum(b) + sum(c) + sum(d) + sum(e)

Let the symbol ‘0’ denote annihilation, or cessation

Let p⁰ = nibbāna(p)

Woah, woah, woah. If you’re not using the traditional negation operator in the type-theoretic formulation, then you need to tell me what you intend to replace it with. Then you need to tell me other aspects of the formal language or alternative type-theoretic interpretation looks like - axioms, type operators, etc - and then maybe I could start breaking down the above.

[christie]

@yeshe.tenley

So you can’t just deny or get rid of the negation type without giving it a replacement or you risk breaking your logic system into something that is unsound, trivial or inconsistent.

Wow, Neo, wow.

I am just pointing out that your “type-theoretic interpretation of logic” does not seem to represent what I think the Buddha has said. The rest is up to you, I was trying to provide a simpler representation using my own notation. If you don’t understand the notation, then let it go.

[Vaddha]

@yeshe.tenley

That in the absence of proof you assume that one of the two corners must be inhabited. Without first overturning that assumption one can not set out on the spiritual life.

Whaddya think?

I think that he’s saying someone who holds to the view cannot progress, yes. But it also seems in some places that he implies that if the view itself were true, then the spiritual life would not be possible.

If the soul and body were identical in substance (Indian materialist view), then the Buddhist path would be defunct. If the soul and body were separate in substance (Indian eternalist view), then it would be impossible for suffering to cease. Of course there are many, many other problems that would arise if physicalism or substance dualism were true also.

@yeshe.tenley

In translating human speech representing propositions and so on into formal language careful attention needs to be paid

Yes. I think that likely the tetralemma in the suttas is a bit more organic and broad of a system. But if we take it as I said before of “entirely X” vs. “X in some sense and Y in another sense,” then it doesn’t seem to be

@yeshe.tenley

using a vague or multi-aspect notion of boundedness, effectively referencing different predicates

, no? Because the predicate is ‘entirely limited,’ ‘entirely limitless,’ ‘somewhat limited and somewhat limitless,’ and neither.

Another example is with colors.
Is Bob’s shirt black, white, both, or neither?

‘Black’ meaning ‘entirely black, and ‘white’ entirely white. If his shirt is a black-and-white checker pattern, it’s both. If his shirt is green or red it’s neither. This doesn’t seem to be vague if defined properly, though the types of ‘both’ and ‘neither’ are broader. For example, grey could be considered ‘both’ as well, and ‘neither’ can be many different types of colors, not just one.

@yeshe.tenley

It would be good to look at cases where the Teacher specifically adopts one of the four corners

One is in the four types of kamma. Bright kamma, dark kamma, mixed kamma, and kamma leading to the end of kamma.

Bright kamma = entirely pleasant result. Dark kamma = entirely unpleasant result. Mixed = mix of pleasure and pain. Kamma leading to the end of kamma = neither. AN 4.238

Similarly with the types of sensations, such as with the post-mortem soul theorists. The soul experiences entirely pleasure. Entirely pain. Sometimes pleasure sometimes pain. Or neither pleasure nor pain (i.e. neutral sensation). SN 24.41-44

Here’s one where he adopts a specific option: AN 4.24

[yeshe.tenley]

@Vaddha

If the soul and body were identical in substance (Indian materialist view), then the Buddhist path would be defunct. If the soul and body were separate in substance (Indian eternalist view), then it would be impossible for suffering to cease. Of course there are many, many other problems that would arise if physicalism or substance dualism were true also.

The problem I have with this is it does too much

“If the soul and body were identical in substance (Indian materialist view), then the Buddhist path would be defunct.”

can be simplifed to:

“If the soul [was a] substance (Indian materialist view), then the Buddhist path would be defunct.”

That is, I see no reason to bring “the body” into it because presumably the body is a given that we both assume, but soul is not. In type theory, both terms should be proven before the product is introduced.

[Vaddha]

But the soul being independent isn’t necessarily materialism. Dualism is also the view of a substantial soul. The reason there is reference to ‘body’ is because it’s either a substance dualism or monism.

I think ‘jīva’ can also be taken here not as utterly unreal, but as a term for the sentience of beings, implying a kind of ‘soul’ or self because that’s generally the only way people think about it. The idea being that sentience and the body are interrelated, not reducible to the other or into separate categories.

But the materialists identifying the soul and the body don’t necessarily think there’s some special soul substance, just that sentience/life is a feature of material things. Like an emergent property or epiphenomenon. At least that seems like it was (and is) a major way they thought about it.

[yeshe.tenley]

@yeshe.tenley

“If the soul [was a] substance (Indian materialist view), then the Buddhist path would be defunct.”

Okay, I can simplify this further:

“If the soul …, then the Buddhist path would be defunct.”

And again ask for ‘the soul’ to be demonstrated. In type theory, all terms need to be constructed or proven. We can of course agree beforehand to assume a given term for purposes of trying to learn something about the implications that would follow if a term were so demonstrated or proven. But in this case, I think I’d just decline to stipulate that ‘soul’ has been demonstrated.

I won’t act as if I know the Teacher would agree to my simplified formulation above, but it certainly is my working hypothesis. For me to know something is for it to be proven and to actually grok and understand that proof.

Take ‘pi is an irrational number’ for example. Most people will say they know that pi is an irrational number… why? Because people they trust say it is so. However, very few have actually gone through the proof from first principles and understood each step and verified for themselves that pi is indeed an irrational number.

The proof of pi being irrational is not a simple proof. It requires a good deal of advanced mathematics. So while people say they know that pi is irrational I think the Teacher might describe this as overreaching. Claiming faith as fact and thus not safeguarding the truth.

PS: I do try and be careful, but I’m also guilty of claiming I know something from time to time which I don’t actually know but just accept on faith. I’m not claiming here that I’m perfect in my usage of ‘know’ because I’m far from it.

[Vaddha]

@yeshe.tenley

But in this case, I think I’d just decline to stipulate that ‘soul’ has been demonstrated.

But what about the sense of ‘sentience/vitality’ I mentioned? Aren’t we all sentient and alive? Is there something there which is other than our body and will not end when the body ends, or is that sentience a mere bodily function like coughing is?

Merriam-Webster for ‘soul’ says:
“the immaterial essence, animating principle, or actuating cause of an individual life”
“the spiritual principle embodied in human beings, all rational and spiritual beings, or the universe” etc.

Also, are you saying the body can be found and proven as a genuine fact? Seems unlike you!

For example, in the undeclared points about ‘Tathāgata,’ it’s not that the Buddha is utterly unreal in every sense of the word. It’s just that he doesn’t have some kind of substantial essence or identity. Likewise, the questions around the universe. Conventionally we do experience the universe, as well as spacetime. And so the questions of the body and jīva could be taken as reifying conventional things, like our sentience, into substantialist categories with a ‘self.’

[yeshe.tenley]

@Vaddha

“the immaterial essence, animating principle, or actuating cause of an individual life”
“the spiritual principle embodied in human beings, all rational and spiritual beings, or the universe” etc.

Yeah, I decline to stipulate or assume any of that. It isn’t demonstrated to my satisfaction or I don’t understand the skillful motivation for which I might assume or stipulate it. I will stipulate consciousness to my fellow brothers and sisters , but I don’t think consciousness is an, “immaterial essence, animating principle” or “spiritual principle embodied…” etc.

[yeshe.tenley]

@yeshe.tenley

The proof of pi being irrational is not a simple proof. It requires a good deal of advanced mathematics. So while people say they know that pi is irrational I think the Teacher might describe this as overreaching.

BTW, going over a complex logical proof from first principles and understanding and really meditating on each step involved so that one ‘groks’ the point is what I think ‘non-conceptual direct mental perception’ is on about. At least that is my hypothesis.

With the caveat that I’m talking about a constructive proof and not an indirect one. Any proof that relies upon LEM and hence is an indirect proof I don’t think it counts. You can’t have a ‘non-conceptual direct mental perception’ of a proof that necessarily invokes LEM.

[Vaddha]

@yeshe.tenley

non-conceptual direct mental perception

Are you referring to Dharmakīrti’s concept of ‘yogic perception’? It’s interesting how he uses the example of a vivid hallucination in an emotionally distraught person to defend his claim of non-conceptual mental perception within his system. But that seems to be another topic! He was certainly a bold thinker!

[yeshe.tenley]

I’m not familiar enough with Dharmakīrti to know if it originated with him, but I’m talking about the Gelug (so via the lineage of Je Tsongkhapa) that a direct and non-conceptual understanding of emptiness is when one embarks on the path of seeing aka becomes an Ariya being. And again, for me emptiness is a function that takes propositions of ‘essence’ and renders them into absurdity. Mind you I’m making no claims of such seeing! It is just my hypothesis that this is what they’re on about.

[yeshe.tenley]

@Vaddha

Also, are you saying the body can be found and proven as a genuine fact?

No, I’m saying I’m willing to stipulate/assume ‘the body’ as a proven term in order to draw out the implications of what that might mean, but I’m unwilling to do that with ‘soul’