answering the last comment by hmc, i'll try to shorten and focus in the main parts of the discussion and restructure it for the sake of clarity for the technical reader:
you mix decidability with consistency.
Not at all, and I stand by my statement. If agda/coq/idris et al had the particular properties that you claim they do then there would be cases where you could trivially send them off into an infinite loop in type-check/termination-check.
this ensapculates two repeated misconceptions. the first one is "why agda/idris/coq" are useful, and from their logical properties point of view, it's thanks to their expressiveness and consistency. they are proof helpers, not fully automatic provers, and as such they're very useful tools even though they don't offer a complete logic, and the proofs generated by them (once found) can be trusted. it doesn't mean that they fit tau's environment.
in practice people use dependent types as for today, because higher order model checking using msol is a very new technique (couldn't begin before 2006) and highly active area of research (some of the interesting results are from this year 2016), and i was referring to the academic world looking for new methods rather deptypes, partially due to the problems i mentioned.
the second one is the repeated request (here and on irc dozens of times) of something that takes agda to infinite loop, while i explain time and again that i never claimed that they can be inflooped, but that some terminating programs must be rejected and there is no human/machine way to pass totality check for all terminating programs.
These tools, which are so easy and approachable that they've been compared to the interface of video games (quite an accomplishment for such a complex software) are somehow actually much less usable than they seem?
playing a video game is easy, but winning it is hard. indeed it's easy to write in agda/idris, but it's hard to pass the checks.
just getting from mltt to mltt+tfpl would require a possibly infinite procedure....
Someone should really let the agda/coq devs know... XD I don't think that they're aware that they've been doing the impossible this whole time...
possibly infinite *human* procedure.
Sure, but this doesn't change the fact that this case of (semi/un/partial)-decidability is irrelevant, as it is an offline, user-interactive process and not a part of the network consensus process.
NO! that's one of your big mistakes. tau will need to detect cases of matching/breaking the rules without necessarily the user knowing about it! and that's what makes a nomic game sound. a context can set a rule, which is basically a type. such rule is set for future purposes, namely, terms that come after the rule is set will try to typecheck. but they will not necessarily typecheck out-of-the-box even if they're well-typed, as typecheck is undecidable, therefore sometimes restructuring the term/type will be required. (such restructuring may be beyond adding postulates, and is a manual process in agda/idris)
Your "complete and consistent" MSO is (necessarily) not computationally complete. It is simply not possible to have a complete, consistent logic which is also computationally complete, as being computationally complete implies being able to express and reason over full arithmetic axioms. Any logic which is both consistent and computationally complete will necessarily be incomplete.
it's easy to restrict a language into a terminating one (eg by primitive recursion) and keeping it computationally complete, as finite turing completeness can be achieved even with QBF which is not even arithmetic (far to mention MSOL), a fact that collapses your argument against msol.
no total language is computationally complete, as it can never interpret itself.
Double nonsense. Self-interpretation is not a requirement for computational completeness. Even if it were, your argument still doesn't stand up as total languages *can* self interpret (contrary to conventional wisdom) as established recently by Brown-Palsberg. (Why you'd even make this claim is strange, since both Brown-Palsberg's self interpretation and Bauer's self interpreter for System T were discussed several times on the IRC....)
Note from stoopkid: "the conventional proof only says that there can be no total computable universal function for the total computable functions, and that any such universal function must be strictly partial, but that if a rewrite system is strongly normalizing then it necessarily cannot be this universal function, because a strongly normalizing rewrite system is equivalent to some total function, not any strictly partial function, and thus can't be a universal function for the total computable numbers, so the conventional diagonalization proof doesnt say anything about the expressibility of the total functions defining strongly normalizing rewrite systems in regards to whether or not they can be their own universal function which corresponds to not saying anything about the existence of self-interpreters in strongly normalizing rewrite systems."
total languages cannot self-interpret, and brown&palsberg is only a weak interpreter. this impossibility can easily be proved by diagonalization, eg here
http://math.andrej.com/wp-content/uploads/2016/01/self-interpreter-for-T.pdfGreat, so go get to it.... it has actually been many (>6) months, now, since you originally decided MLTT isn't the way
no, only less than 2 months since i found out regarding mltt.
Of course it would be self-contradictory for you to claim that multiplication is possible in your hypothetical complete & consistent "somehow MSO-like but not really MSO" logic. As you rightly elaborate in your blog post, this would contradict Godel. If tau is to be built with a complete and consistent logic, then it will necessarily omit some portion of basic arithmetic - meaning there will be some math which it *cannot* do in its rules - meaning there will be some routing/topology rules which it *cannot* employ - meaning it will *not* meet the original goal of a fully general, decentralized network. (This is inescapable without accepting an incomplete logic.)
no. not-being-arithmetic doesn't necessarily require to give up either mul or add, but can restrict certain quantifications, negations etc. while keeping both operations. one example is monotone multivariate polynomials.
If you don't know what a general product is, (and why GADTs are important for programming in a typed functional setting) or the difference between a product type and an intersection type, then you are certainly still a *long* way (another year or two, maybe?) from being ready to build a tau, using *any* logic.
Note from stoop: "you might explain why exactly MSO prevents the definability of the general product, even without appeal to godel; mso rules out quantification over functions of arity greater than 1,
Let's just ignore the fact that MSO predated MLTT by quite a bit, and is certainly well set in "the old ways" of the days of Frege and Quine...
these are two examples of a repeated misunderstanding of you, mixing msol with stlc+y. you can happily quantify higher order multi-parameter functions, as they're stlc+y creatures, which modern msol-over-trees speaks about. like taking mltt and adding it an msol meta-logic, but that'd be undecidable, so we restrict mltt in one hand to simple higher order types, and enrich it on the other hand with an unrestricted Y combinator whether safe or not (which implies non-normalizing terms of course, yet normalization is decidable via the mso metalogic). and this is (msol over stlc+y far from being strict subset of mltt) part of why you're all so wrong in your ""understanding"" of msol, as you wrote:
"you might also note that everybody on our team probably has a better understanding of MSO than he does at this point. since we understand it completely fully as just a specific and not very expressive subset of MLTT. and are seeing a more complete picture that illuminates exactly why MSO has the specific properties it does and how those actually relate to the rest of MLTT."
last:
just like human intuition works when it comes to formalism. and just like the vast majority of mathematicians in all eras hold.
Our intuition must certainly work differently. That is OK. "Agree to disagree" and all.
As to how the "vast majority" of intuitions work, I won't be so arrogant as to assume.... and I don't think that there's been anything like a census... Feel free to show some statistics on the matter, however, if you know of such a poll!
look all over the mathematical history, when did people consider non-LEM Euclid geometry? i pick this specific example as it's the oldest fully-axiomatic theory (axiomatized by Euclid himself) that was never stopped to be studied and written about.
