Quote from: ohad on October 03, 2016, 05:41:51 PM

Quote from: redfish64 on October 03, 2016, 11:37:49 AM

1. Ohad seems to think that all proofs must be automatic for Tau to prevent malicious actors from attacking Tau.
Couldn't the rules of the P2P nodes just require a proof of certain properties to be handed along with the rules for them to be acceptable? Be solvable in a certain amount of cycles using a given Resoner?

the proofs being automatic comes from the theory being decidable, and the manual requirements in idris/agda stem exactly from the undecidability problem. and indeed tau must be decidable as it must be a sound nomic game: the network should know when someone obey or break a rule, with no false positives or false negatives. under idris/agda, due to the undecidability, you can obey the rules yet not necessarily be able to prove it.

Quote from: redfish64 on October 03, 2016, 11:37:49 AM

Yes, the alternatives described would also work with a Turing-complete language, as well, but so what if it did? If using MLTT or MSOL isn't substantially better than a Turing-complete language, then a Turing complete language should be used.

msol is substantially better as it is decidable (which also imples automatic proofs).

Quote from: redfish64 on October 03, 2016, 11:37:49 AM

2. Just because MSOL can be solved automatically, this doesn't mean it can be done quickly enough to be useful in Tau, isn't it? I mean that if it takes an exponential amount of time to automatically solve a question proposed in MSOL (and it seems from what I'm read that it is N-EXPTIME), then it might as well be true that some expressions aren't solvable in MSOL, right? And if that is the case, you have the very same problems of MLTT.

complexity of proof is pretty much the same in both systems (i.e. unlimited complexity). it doesn't mean that even easy tasks will take very long time, it only means that it's able to solve even very hard problems. in addition, k-exptime for example is just a worst case bound. it is commonly said (e.g. by Ong) that this worst case should be achieved quite rarely, and not in common human programs.

Yes, but if a malicious actor attempts to add a rule to the system which, within the context of the system, can only be determined valid after an inordinate period of time, wouldn't this be a problem for a MSOL based Tau? It would be, for all intents and purposes, be undecidable, correct?

An undecidable system, such as Idris/Agra has false negatives (a valid program is not accepted), but not false positives (an invalid program is accepted), correct?

So, both systems, for all intents and purposes, have a false negative problem. When using Idris/Agra and the user inputs a program that is undecidable, the user is just asked to clarify. Similarly, it would seem, if after a certain period of processing, validity can't be determined by MSOL based Tau, then it would also need to ask the user to clarify, or reject the rule outright.