I have a vague idea on the tip of my mind that I can only convey through examples.
Gödel's theorem states that some systems (ZFC, for example) are always incomplete in the sense that new axioms (which are not derivable from the old axioms) can be added to them without making them inconsistent. As we remember, proofs can be formalized and run on a computer.
My idea is that formalized systems like ZFC and their theorem proving processes have some inherent "irreducible complexity" or, if you prefer, "computational entropy". To clarify what I'm talking about: let's imagine several graphic files: the first one is completely filled with turquoise. The second is a simple desktop wallpaper. The third shows people against the backdrop of buildings. The fourth is noise generated by a quantum random number generator.
Intuitively, for each of these files there is a certain "irreducibility threshold", when it's impossible to completely restore the file, having information available less than some threshold value. It's intuitively clear that for a uniform background the threshold is very low, while for noise this threshold is close to the maximum. That is why when we remove the redundancy from the image, only noise remains, the difference is only in the "amount of noise" for each particular file.
Let's move on to the halting problem. Indeed, there is no function capable of determining whether another function passed to it as a parameter halts. However, let's try to prove "manually" for some functions whether they halt or not using the lambda calculus. Take, for example, the term \x -> x. Since it contains no redexes, it's already in normal form, hence it halts. Now take the term (\x -> x x) (\x -> x x). The expression contains only one redex, after the reduction we have the same expression that was at the beginning. Thus, if we build a reduction diagram, we can see that it completely closes on itself. Therefore, the term (\x -> x x) (\x -> x x) never halts.
What's important is that the terms I have chosen above are quite simple. There are much more complex terms with very long and branched reduction diagrams. For at least some terms, we can prove whether they halt or not just by running them, but this will require a different amount of computing resources! Proving that \x -> x halts and (\x -> x x) (\x -> x x) doesn't, took quite a bit of reasoning, but for some terms I would have to reason very, very long. The same is true in strongly normalizing typed varieties of the lambda calculus like Coq: proofs can vary in their "irreducible computational complexity".
My intuition is that the halting function fails because it tries to determine if another function halts in one step of reduction, whereas we need different "amount of reasoning" to analyze different terms - due to different "irreducible complexity" of different functions! When we (or a machine) are reasoning about something that inherently very complex, the reasoning structure itself must be very complex, otherwise we fall into contradictions. For the same reason, a function that tries to "inspect" itself falls into a contradiction.
But how then can we reason about systems that are more complex than our brains? Of course, we can do this by breaking them down into its component parts and reasoning step by step, however, even in this case, we will need some kind of "overhead complexity" in the form of additional reasoning and / or extra time. The same thing will happen if we try to examine, for example, our own brain - when we start to inspect the processes taking place in it, the very processes in our brain will change due to the fact that reasoning (computation) is itself a process in the brain! This attempt by the system to inspect itself in real time is like a vacuum cleaner trying to suck itself in. Just as a vacuum cleaner will never complete such an action to the end, so in the reasoning that inspects the system, there will always be no less "irreducible complexity" than there is in the system being inspected. (Perhaps even always more, but I cannot say this with certainty).
The above, however, does not mean in the least that we cannot understand how the brain works in principle! If understanding means knowing how things work, then we don't have to "chase our own tail forever," as Dennett suggested. For example, the spectral gap problem was proved in 2015 to be undecidable, and more recently, in 2020, the proof was generalized to the one-dimensional case. This proof does not tell us at all that the problem is unsolvable in the absolute sense, it only establishes that quantum systems can increase in complexity indefinitely. For individual systems, it's quite possible to prove the presence or absence of a spectral gap simply by constructing it or by simulating it! (Which, of course, will require "irreducible" computing resources).
Thus, in my opinion, all "fixpoint" theorems tell us that no matter how complex the system we consider, there will always be a bigger fish. It's for this reason that we can add more and more new axioms to ZFC indefinitely, making fishes bigger and bigger. I will make another hypothesis: the reason why most of the mathematical constructions can be expressed in systems that are much simpler than ZFC is that these constructions themselves have very low complexity.
My question is: do we have a universal mathematical tool capable of "natural" expressing unbounded structural/informational/computational complexity, whether in the form of formulas, expressions or diagrams? If not, are there even hints of the (im)possibility of such a tool?
Of course, you can call any Turing complete system, however, for example, Turing machines have significant drawbacks: the Turing machine not only accepts some information (programs and data) to work with it, but it itself has an internal structure, thus it has a kind of "contextual/mutual complexity", that is need to be isolated to represent structures in more "natural" way. For example, when two numbers are added on Turing machine, it's difficult to understand what exactly is happening.
In pure lambda calculus, however, it's much easier to understand how the same addition function (in Church encoding) works, also the lambda calculus has only two components: constructing functions and applying it to another functions, and in a certain sense these are two sides of the same coin: the notion of a function, by definition, implies its application to an argument, as well as we can apply only to a function, so it's closer to what I need.
There's been a lot of talk about category theory as a possible mathesis universalis, so it might be the answer, however I haven't seen any work on "categorical informational/computational complexity". If there are, please leave a link to them.
Thanks in advance.
