Hacker News Reader

I was with you until here:

> which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd...

Why did you randomly shoehorn in homotopy type theory? Maybe I’m overreacting to this, but the only person I’ve ever known to shoehorn homotopy type theory into largely unrelated discussion has left quite a poor impression for me.

View on HN

Why not? Why do you think it's irrelevant? The reason why I included that is very simple: it models the situation I want to express exceptionally well. In "mathematics" we learn in school none of the discussion relevant to the "Halting Problem" really is relevant, which is very confusing to students who even paid attention in school. To make the situation even relevant, we need to start assuming (or realizing, accepting, whichever one you want) that there are relations in mathematics that are undecidable. If you have a model of computation, which will internally be constructive, in order to freely apply our knowledge of mathematics onto this model, we need to go back to grade school and replace every instance of "is true" with "is constructible in your model of computation/programming language" (or more traditionally "is provable"). Which means you need an entirely different reasoning framework. So, to "go back" to classical math from having understood the existence of undecidability as "home", we need to unassume this, which will be identical to assuming all relations are "decidable" within your computational model. It's not like they actually are (at least not to the extent you can compute within). Homotopy theory is the exact thing that's developed to explain situations such as this one. Why not just use it? I apologize if anything I say is wrong or misleading, I'd be happy if you can clarify.

Reply on news.ycombinator.com