> Worse - strong claims about mathematical provability immediately fall apart because of Godel

incompleteness means true but unprovable propositions in specific forms of higher order logic, but Kurt also proved the completeness of first order logic. However, the scheme of induction used to lower peano arithmetic to first order logic (Presburger Arithmetic e.g.). Likewise, an incomplete higher order logic can (ostensibly - I couldn't) be proved in a logic of even higher degree, which is again incomplete, so again that's an argument ad infinitum. Obviously that's abstract nonsense, but the question shouldn't be whether the universe can be predicted up to infinity. The question at face value is rather, whether quantitative analysis can solve any given qualitative problem. It's the syntax semantics duality - what comes first?

For someone who's on a first-name basis with Gödel, you should review your logic.

The incompleteness theorems hold for any formal system whatsoever, regardless of order. They are simple corrolaries of the halting theorem. First order logic is indeed complete in the following sense: A sentence of FOL is provable iff it's valid, i.e. true in all interpretations. But according to the incompleteness theorem, logical theories (sets of axioms) of a certain richness would always yield sentences that are true in some interpretations and false in others, or, alternatively, that are neither provable nor disprovable (and first-order Pano arithmetics and obviously all formal set theories are among them).

Order and other particulars of a formal system are irrelevant, and indeed Gödel was only fully satisfied with his incompleteness theorems after he read Turing's famous paper on computability, and regarded it a "miracle" (as it applies to any formal system, and depends on none).

Obviously, many quantitative problems are unsolvable as a direct result of the halting theorem, and more generally the time-hierarchy theorem (which states that there are problems of any arbitrary difficulty), as many decidable problems are still unsolvable due to intractibility.

see, the halting problem is much more appropriate for this audience :)

However, there is the calculus of constructions, which, as far as I can tell, tries to be provable in all admissible formulas. It's a totally functional language. So, is the universe totally functional, will it halt? I'm not sure that's the actual question, neither whether the universe is beyond our understanding, that's out of the question, only, does the universe follow rules or is it deterministic and not only in the quantum sense.

> all computable mathematical structures (in Gödel's sense) exist - en.wikipedia/wiki/Mathematical_universe_hypothesis

That's trivially true, because they exist in the heads of the mathematicians constructing them.

> However, there is the calculus of constructions, which, as far as I can tell, tries to be provable in all admissible formulas. It's a totally functional language. So, is the universe totally functional, will it halt?

Total programming languages (or more precisely, their term language), is not Turing complete, and is not universal (although such languages, like Agda, are Turing complete, but not in their terms; i.e. their expressions are not Turing complete, but they allow simulating Turing machines using an interaction with the runtime using something called codata). If the universe is finite, then it, too, cannot fully simulate a Turing machine (and the formalism, or language, used to desrcibe it is completely irrelevant; total functional languages aren't just formalisms, and the universe is a true system).

> That's trivially true, because they exist in the heads of the mathematicians constructing them.

Well, it's not so simple. First, we have to philosophically determine what we mean by "exists". Platonists believe that there exists a world of abstract forms. If we restrict existence to physical existence, we still need to determine what it means for an abstract mathematical structure to exist in the mathematician's mind. Brouwer believed that for those structures to "exist", the mathematicians should be able, at least in principle, to construct them. So only constructive math "exists". On the other hand, Hilbert, also a finitist, said that math is made of two parts: "real" propositions (finite, about the physical universe), and ideal propositions (finite expressions but infinitary objects, those don't "exist" as anything other than the finite formulas that express them). But even in Hilbert's formulation, there are many inifinitary mathematical objects for which no finite description could exist (by a simple cardinality argument). Do those exist? For Hilbert, probably not, but for Platonists, they still do.

> Physics may be mathematical, but that doesn't mean you can start from the Big Bang and use mathematical physics to predict the contents of this particular thread on Hacker News.

Only because the only available approaches for even beginning to do anything of that sort are constrained by being embedded in that same universe.

It's unsurprising that a system cannot exist, and at the same time embed a calculation which calculates all of itself.

(We cannot even use mathematics to predict simple N-body problems; we have to switch to numerical techniques which have limited precision. Once you have floating-point in there, it's no longer the math, but an approximation.)

Which has nothing to do with my point, which was that the grandparent was assuming the MUH wasn't true as evidence that it isn't.

I didn't assume it is not true nor claimed it is not true, simply pointed out that it is not obviously justified as the simplest explanation to the fact that that math can explain the universe.