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.
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.
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.