Hello Venerables, I’m glad that you’ve found this OP fruitful!
Venerable Vaddha, I take your response as indicative that you’ve taken the time to study constructive logic a bit with the reference to the King of France. And having some experience with how studious and careful you can be I dare hazard a guess that you’ve gone quite beyond a bit 
Which pleases me to no end I might add.
Venerable Sunyo, yes, that is precisely what I was trying to point out. SA 72 would seem to be a straightforward case of the Teacher not being silent 
I’m keenly curious to know what the two of you think of my post trying to render the Tetralemma in constructive type-theoretic language. In particular, I want to know what you think of the point I made near the beginning of that post:
A crucial subtlety in constructive type theory is the difference between:
- Simply lacking a proof of P (or ¬P, etc.), which is a state of ignorance.
- Actually proving that P is uninhabited, i.e. constructing a term of type P→⊥.
The Teacher denying the four corners explicitly in SA 72 I think proves beyond a reasonable doubt that the Teacher was not assuming LEM in his reasoning. Assuming he was using some form of constructive logic instead of a paraconsistent logic, the subtlety pointed out above becomes paramount.
So what do you think? Did the Teacher intend to convey a state of ignorance for any of the four corners or did he intend to prove that the four corners were uninhabited by means of showing the contradictions they lead to?
@Dogen as someone else who has taken the time to learn about the formal logical ‘grammar’ we’re discussing here I’m also keenly curious to know your opinion!
