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

Continuing the discussion from The experience of "Anatta":

Abstract: The quote above came from a thread where the meaning of anatta was being debated. There have been many such threads on these forums. Often times I see people arguing past eachother with different unstated assumptions, unstated logical systems, logical errors, imprecise language leading to disagreement and so on. This often derails discussion leaving all parties dissatisfied. If we disagree it would be best for those disagreements to have a foundation of mutual understanding rather than a shaky foundation of miscommunication, imprecise language, non-shared unstated assumptions and so on. I propose that those who argue doctrine on this forum would do well to study some formal languages: type theory, logic, and mathematics. I will try to illustrate this with a dissection of the above in more formal terms.

Discussion:

The quote above talks about mutual exclusion, but mutual exclusion in mathematics, logic, and type theory can come in many varieties. In type theory, saying two types are mutually exclusive usually means that there is no value that inhabits both the type A and the type B. The ‘type of rational numbers’ and the ‘type of irrational numbers’ is an easy to understand example. There is no number that inhabits both of these types.

In logic, saying that two statements (or propositions) are mutually exclusive means that they cannot both be true. Mutual exclusion carries the same generalized conceptual meaning in both type theory and logic, but there are important differences in how they are formalized. Luckily, there is a conceptual bridge between the two called the curry-howard isomorphism. Roughly speaking, propositions or statements in logic correspond to types in type theory. A logical proof is analogous to a well-typed program that constructs an inhabitant of the type/proposition.

With this in mind let’s look at the simple logical proposition P and its negation ~P. These two are mutually exclusive and in terms of type theory they are expressed as the type of P and the function type from P to the empty type (⊥). Let’s talk about the empty type for a second.

The empty type (⊥) has no inhabitants and it represents falsehood or contradiction in logical terms. So ~P is the type of a function that takes the type/proposition P and turns it into a falsehood or contradiction. In simple english it just says, “If I assume P, then I can derive contradiction.”

So now we have two examples of mutually exclusive types. There is A and B, where A is the type of rational numbers and B is the type of irrational numbers. There is P and ~P which is a logical proposition and its negation. Both examples are mutually exclusive in that there is no inhabitant of both of these types in the pair.

However, there is an important distinction between these two examples! In the first case of A and B … both A and B actually have inhabitants. The number 5 is an example of an inhabitant of A and the number pi is an example of an inhabitant of B.

The second example is not like this! Either P is inhabited or ~P is inhabited. They both can’t have an inhabitant or this leads to contradiction.

I call attention to this fact because it shows that having a mutually exclusive pair of types does not necessarily mean that both types must have an inhabitant. Disjointness (mutual exclusivity) only says “there can’t be a single inhabitant in both types at once.” It doesn’t say anything about whether one (or both) of those types actually has inhabitants.

In fact, any logical system (western or eastern or whatever) must account for falsehood or contradiction and in that case it would correspond to the empty type above. If it doesn’t have this, then it will suffer from exfalsoquodlibet.

Main result: keeping this discussion in mind let’s talk about the quote above and anatta. One big controversy on this forum repeated many times is whether anatta should be viewed as no-self or not-self. The above discussion does not settle this question. Let me repeat, the above does not inform an answer to this question.

However, I do think it can give us a new language to frame this question and to be very precise what we’re actually arguing about without talking past each other. In the language above the question is basically do the types of the mutually exclusive pair of attā and anattā look like A and B or P and ~P. Are both attā and anattā inhabited but mutually exclusive? Or is only one of attā and anattā inhabited and mutually exclusive? BTW, if neither is inhabited then they aren’t really mutually exclusive.

Conclusion:

I think attā and anattā are like P and ~P. That is only one of them is inhabited and it is ~P aka anattā. So what is anattā? It is the type of the function that takes ‘attā’ and derives ⊥. Importantly, it simply isn’t the case that just because attā and anattā are mutually exclusive that they are necessarily both inhabited. If you think that is the case, then this reveals that you’re using an unsound system of logic.

I will end with my proposal that those who argue doctrine on this forum would do well to study some formal languages: type theory, logic, and mathematics if for no other reason than it will help ensure our disagreements have a foundation of mutual understanding.

:pray:

4 Likes

I believe your intent is good @yeshe.tenley but I feel it is also a qualtity to make things concrete, personal, related to our own experience. The initial threat was also about the experience of anatta. Meanwhile it derails into a discussion about logic, type theory, mathematics, pi.

Why not do an attempt to describe what anatta really means for you personally, in an experiential way? And talk with eachother this way?

Not meant to offend you, but to me, but that is me, you are making things so abstract and i do not want to be there. I do not care about it.

But sorry, i am not gonna study logic, type theory and mathematics to be able to discuss things on such a very abstract level. I like to make Dhamma as concrete as possible. And if it leads to disagreements, that is fine too.

So … there is logic in ancient Buddhist texts that considers P and ~P as an option and also ~[P and ~P] as a fourth option. And typically, all four options P, ~P, P and ~P and ~[P and ~P] are said to be untrue.

Hmm!

4 Likes

Yes, the tetralemma can be handled just fine in the language of the above. I can explain in more detail if others care… But for the purpose of this thread, it’s important to understand that in the language of type theory ~P is typed not as a thing but a function that takes proposed inhabitants of type P as input and returns absurdity/contradiction ⊥. :pray:

Let`s start with what we know from the EBTs. The catuṣkoṭi (tetralemma) is never used in the context of ātman and anātman. So here we are left with A and ~A as the only options, where ~A (anātman) is by definition whatever ‘A (ātman) is not’. In a similar vein, what is not sukha is duḥkha, and what is not nitya is anitya. The triad of anitya, dukkha and anātman is collectively a feature of all objective reality (i.e. everything that can be seen, heard, tasted, smelt, touched or thought). So if you are moving away from the territory of the samsāric triad (duḥkham, anitya & anātman), you are moving towards the nirvāṇic triad (which by definition is what samsāra is not).

So applying the catuṣkoṭi (tetralemma) to ātman and anātman would detract from the EBT’s conception of it.

2 Likes

This makes a lot of sense.

1 Like

The tetralemma are ontological categories applied to the atta. The Buddha said none of these apply.

This topic is not specifically about the tetralemma although I see the thread veering in that direction. I’d like to keep this thread about using formal languages with doctrine … so if you want to discuss the tetralemma please do so in the context of formal languages. Thanks. :pray:

2 Likes

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

I suppose you mean the tetralemma explained via formal language? Okay, I can write it up but would you prefer it as part of this thread or a sep one? :pray:

Yes, I always found that one confusing, although not sure if using formal language will make it clearer.
I will be happy to read it in any thread! :rainbow:

So would your interpretation of the tetralemma be ~(P) + ~(~P) + ~(P + ~P) + ~(~(P + ~P))?

Sorry, couldn’t resist. I’ll go back to hiding now.

2 Likes

Oops, I just realised the tetralemma only applies to P0 where

P0 = nibbāna(P)

This is assuming P is the aggregate of the 5 khandhas:

P = A + B + C + D + E

I think the primary issue why people debate P is that there are postulating the existence of Q where

Q = ~( A + B + C + D + E)

And the people who argue against Q say that

Q0 = ~(Q) + ~(~Q) + ~(Q + ~Q) + ~(~(Q + ~Q))

In fact, the Buddha seems to be implying that the tetralemma applies to an infinite series of P, Q, R, …

1 Like

6 posts were split to a new topic: Tetralemma: General Discussion

Please read the post more carefully. I’ve explained in the original post what this means and gave examples of the number pi being an inhabitant of the type of irrational numbers.

:pray:

PS I’ll ask again that this thread remain on-topic about using formal languages (type theory, mathematics, logic) to clarify disagreements over doctrine. It has nothing to do with the tetralemma per se. I’m writing up a new thread for that topic as expressed in type-theoretic language, but even that one won’t be about generic debates around a point of doctrine without using formal languages.

1 Like

Yes, I get that, so what do you think of the following

Ātman can never be anātman, and anātman can never be ātman. So if you want to call things belonging to type anātman as inhabited by x,y & z - that is ok, those (x, y & z) cannot inhabit the type ātman. But the same thing holds good for ātman as well, what is ātman can never inhabit the type anātman. Ātman is not just a type but also the inhabitant of its type, it is not empty by its very definition. It is only because it is not empty that what is not-ātman is a type that can meaningfully exclude the ātman from itself, otherwise there is nothing excluded in reality and not-atman is not really “not-atman”

What if 0 contains 1 and 1 contains 0 on a level of mathematics we are yet to understand?

1 Like

This is just another restating that they are mutually exclusive. Which is the subject of this post. Again, I agree that they are mutually exclusive. But I don’t think that means what you think it means.

If you insist that Ātman is an inhabited type by its very definition, then Ātman is an axiom of your system that you never prove but just assume. I have my doubts that such a system is going to be very powerful, consistent or useful. It would be like insisting on the axiom, ‘Unicorns exist!’ Okay. And?

However, I don’t have to assume this definition and/or axiom and so I decline.

No, you’ve mistaken mutual exclusion for the idea that any two mutually exclusive types must both be inhabited. It isn’t true and was one of the key points of my post. An easy example is the proposition, “pi is a rational number.”

Let P be that proposition. It is mutually exclusive with f :P→⊥. It has been shown that the latter is inhabited. In the 1760’s Lambert wrote that function which is a difficult function to write. P is not inhabited.

These two are mutually exclusive, but they are not both inhabited. :pray:

1 Like

From what I can tell, @srkris has been seen using old Brahmanical cards to play against Buddhism. Their statements in other comments about anattā have been derivative of the well-known Adi Sankara comment: “Who is it that …?” For Sankara, this ‘who’ was necessary and was the ātman; he considered it non-sensical otherwise. He denied the emptiness of Buddhism.

Similarly, Srkris is currently using what I believe is a Mimamsa argument. I’m not very familiar, but it reminds me of what I’ve learned of Dignāga/Dharmakīrti. These two (and others in their school of thought) denied universals and said that the mind perceives them by collecting a group of particulars and contrasting it to what does not fit in that category.

For example, if someone perceives a cow, they would say that it is not that there is a universal ‘cowness,’ but rather that the mind groups a set of particulars simply by excluding whatever is not-cow. So it is a mental function/imputation via negation. What I’ve read is that some brahmins took issue with this, as you would need a category of ‘cow’ in the first place to delimit what is ‘not-cow.’

Someone correct this if mistaken.

2 Likes

Well, if that is the case, then in this thread at least I’d like those cards to be played using formal language :joy: It seems that srkris wishes to define Ātman as an inhabited type as an axiom of the system he wishes to use. I decline to share that axiom.

From a type-theoretical perspective it is completely out of the cards to define an inhabited type out of the gate with no proof. The motivation for doing so would have to be compelling. Here I see no motivation explained so far at least.

It would be another step much much further to insist that this Ātman axiom is necessary and that I must adopt it. To prove it was necessary would be tantamount to proving that classical logic, constructive logic, all known logics are inconsistent/unsound/not-powerful enough without it. I very highly doubt any such proof would be possible. That is understatement btw :joy:

:pray:

2 Likes