There is a direct link between our ability to define "truth" and our ability to form a decentralized automated platform.
An automated platform is one which can execute future task based on rules set in the past or present without future intervention. Such platform is crucial in order to realize the idea of smart contracts. However decentralizing such platform means that there is zero tolerance for "bugs" since there is no central authority to roll back any faulty function. This means that we must trust our computers to deliver the exact result it was designed deliver. We place our trust in the proof which this computer can produce regarding its future action. A proof that is based on it (the computer) being a total rational logical machine.
The most ambitions project in the blockchain ecosystem which aims at decentralizing not only the code by which the platform is running but also the rules by which the code can be changed is Tauchain . This project is running now into the heart and soul of that yet unresolved paradox which will be programmed as a solution on the Tauchain once created.
As explained by Ohad Asor one of the two founder/developer of the Tauchain on his blog IDNI
The paradox of self amendment and its implication when trying to answer similar questions in the world of numbers and mathematical objects
Not only laws cannot be understood in an absolute way, but cannot even trivially be made by an absolute process. Laws have to be changed with time and therefore we also need laws of changing the laws. But then we’ll need laws-of-changing-the-laws-of-changing-the-laws, ad infinitum. We therefore remain without any logical basis for the process of rulemaking, not only the crisis of deciding what is legal and what is illegal. This paradox was described on the online-available book The Paradox of Self Amendment by Peter Suber. Suber’s solution is summarized on the appendix of that book that describes the game Nomic. He offers a two-tier system in which we have mutable and immutable rules, including rules of transmuting a rule (namely to make immutable rule mutable or vice versa). This way one can avoid the infinite hierarchy of amendment-schemes, but we still remain with the “crisis of truth” in which there is no one truth, especially when you desperately need it, and despite the very purpose of laws to have a certain social order rather disinformation and chaos.
When stepping back from the world of legalities and trying to answer similar questions in the world of numbers and mathematical objects, the task doesn’t become easy but arguably easier. Logicians have contemplated those ideas for centuries and came up with the notion of Decidability. A language is decidable if every expressible statement on this language can be decided whether it follows from rules expressed in that language as well. An astonishing example would be Godel’s theorem: if our language is able to express Peano arithmetic, namely, it contains the natural numbers 1,2,3,... equipped with addition and multiplication and their rules (that indeed determine them uniquely), then there will always be some true statements about Peano arithmetic that cannot be proved from the definitions. Infinitely many axioms will therefore be required in order to be able to decide the correctness of every statement. An example of decidability would be Presburger arithmetic: if we give up multiplication and define numbers with addition only (in a certain way), we are then back to decidability and every expressible statement could be decided in a finite process to be either true or false. Same applies to the 2000 years old Euclid geometry which is a decidable theory indeed.
Ohad which have been working along side with HMC on the project in the past two years came to believe that the original design regarding the logic of the language of tauchain is wrong.
His conclusion, as stated in the blogpost, is not shared with HMC : "If we would like Tau to give a real contribution to the world, it must use a decidable language. The initial Tau design was aiming to answer those requirements, but recently I’ve found out that I was wrong, and the initially chosen language is simply undecidable. Martin-Lof Type Theory (MLTT) has only certain decidable aspects (specifically, equality). But it is not the case that everything expressible is decidable. This situation led me to a conclusion that MLTT was a wrong choice, and another logic should be considered."
For sometime they both have been arguing their points on the IRC channel and only a few days ago they both organized it into comments on the Tauchain thread on bitcointalk
HMC comment https://bitcointalk.org/index.php?topic=950309.msg16384133#msg16384133
Ohad Asor comment https://bitcointalk.org/index.php?topic=950309.msg16393718#msg16393718
The argument details which they both bring up are far beyond my knowledge, (I am not a developer or a mathematician) thus I can not make a judgement on any of it. However as I expressed in my last few entries the issue in stake "the truth" is a matter of many theoretical considerations. I also believe that the resolution which will emerge is going to involve some of the deeper realizations I tried and will continue to verbalize and express here.