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.