Matthew Scherf has successfully verified the logical consistency of Śaṅkara’s Advaita-Vedānta metaphysical system. For that work he used the Lean 4 proof assistant, a functional programming language and theorem prover built for formalizing math and for formal verification. The Advaita-Vedānta was successfully verified with 0 logical inconsistencies. Here’s a nice presentation of that work.
Abstract. We present a first-order axiomatization of Advaita Vedānta metaphysics, formalized and verified in the Lean 4 proof assistant. The system comprises 69 primitive axioms organized into ten modules, capturing the core doctrines of non-dual Śaṅkara Vedānta including the identity of Ātman and Brahman, the three levels of reality, the theory of superimposition (adhyāsa), and the three-state analysis (avasthā-traya) from the Māṇḍūkya Upaniṣad. All proofs are machine-verified.
I just wonder if Buddhas Teachings could be axiomatized using high-order mathematical language and verified using Lean 4, just like they did with Advaita-Vedānta. If Buddha’s Teachings passes the test of logical consistency, this would be a great news for the Buddhist world.
Factor of faith in Buddhism:
Not logic but wholesome experience. So, no verification through logic but instead only through practice.
Moreover, range of Wisdom beyond logic.
Dhamma is for one who feels. Suffering isn’t logical category. As well entire experience. Certain descriptions are valid only within particular aspect of experience, so sometimes it is possible to encounter logically opposite descriptions, which most probably would be classified as lack of consistency, while it would be enough to order them hierarchically to see that inconsistency appears merely on verbal level.
A syllogism can be logically valid even if one or more of its premises are false. This logical validity, however, does not mean the conclusion(s) are true.
Secondly, some conclusions/knowledge(s) may be true but are beyond formal logic. For example, the knowledge of rebirth in Buddhism.
Reminds me of the well-known, yet still eyebrows-raising bit in AN3.65:
Please, Kālāmas, don’t go by oral transmission, don’t go by lineage, don’t go by testament, don’t go by canonical authority, don’t rely on logic, don’t rely on inference, don’t go by reasoned train of thought, don’t go by the acceptance of a view after deliberation, don’t go by the appearance of competence, and don’t think ‘The ascetic is our respected teacher.’ But when you know for yourselves: ‘These things are unskillful, blameworthy, criticized by sensible people, and when you undertake them, they lead to harm and suffering’, then you should give them up.
In other words, ‘practice/experience’ as a couple of people upstream commented.
Also, I notice that several of the views in DN1 were held by ascetics or brahmins who “speak of what they have worked out by logic”, yet the views contradict each other. Even if the Buddha’s teachings could be proven to be logically consistent using software, I personally guarantee that another religions apologist would be all like “nuh-uhh, our teachings are the best-est and here’s why…”.
Interesting. I’m looking forward to downloading the files and reviewing the code after I run it. I think proving that the canon is consistent would be a monumental and futile effort, but for those who believe the Atthakavagga and the Parayanavagga are the oldest Buddhist texts, there is hope.
Regardless of possible logical consistency of the Canon, those of us who practice Buddha’s methods know that they bring promised results. Practicing Buddha’s meditative practice of mettā-sādhana has reduced my suffering tremendously.
Maybe Buddha’s Teachings teaching was never meant to be a logically consistent system of thought. Buddha compared his teaching with a raft. It’s purpose is crossing the flood of suffering and reaching the far shore of peace, Nibbāna. One we get there, the need for the raft ceases and we can let go of the raft, the teachings.
