If you consider the Curry-Howard correspondence in connection with Gödel's Incompleteness Theorems, the fractal nature of the universe seems inevitable.
What does that have to do with fractals or the physical universe?
What it seems to me (could be totally wrong, would love to know if so) that Gödel's conclusions can then tell us about our universe/computer/executing-program/mathematical-proof (please excuse the fumbly wording) is that it has to have an external universe in which to exist/run/be-consistent-in, which presumably depends upon its own, ad infinitum. In other words, it would have to be universe-program-computer-proofs all the way "out".
Citation for the first point: https://en.wikipedia.org/wiki/Digital_physics
> According to this theory, the universe can be conceived of as either the output of a deterministic or probabilistic computer program, a vast, digital computation device, or mathematically isomorphic to such a device. > "Within each universe all observable quantities are discrete, but the multiverse as a whole is a continuum. When the equations of quantum theory describe a continuous but not-directly-observable transition between two values of a discrete quantity, what they are telling us is that the transition does not take place entirely within one universe. So perhaps the price of continuous motion is not an infinity of consecutive actions, but an infinity of concurrent actions taking place across the multiverse." - David Deutsch
Also, some concepts helpful for bridging the gap:
- Programs (and their states) are graphs
- Graphs are just relationships between quantities
- Every program is an instance of the general pattern `fold(f, input)` [1]
- Imperative programs are just inputs to functional programs
- Computers can be emulated in functional languages
- Traversal of a state graph is equivalent to time travel in the universe described by the states (or travel between the universes described by the states)
- Temporal/causal reasoning is actually spatial reasoning (traversal through the mental representation of state graph edges, i.e. executing a mental program)
- Correspondence between numbers, vector spaces, matrices, objects, closures, programs, functions, graphs, simulations, proofs, mappings, categories
From the above, I believe one can reasonably conclude that:
a) computers are programs
b) computers/programs are subsets of our universe
c) all computers/programs exist inside other computers/programs
d) computers/programs exist in our universe
e) our universe exists in a computer/program, which itself does as well, etc
Again, I haven't had this verified so I'd love to hear why/how this is wrong.
Gödel's first incompleteness theorem that "In any consistent formal system with [enough arithmetic to make a Gödel encoding], there is a proposition P such that neither P nor ¬P have a proof." translates as:
"In any type system that does not allow construction of functions from inhabited types to the empty type ⊥ (this corresponds to consistency), with [enough types and functions to make a Gödel encoding], there is a type T such that neither a program of type T, nor a program of type T → ⊥ (this corresponds to negation), can be constructed."
The semantics of the programs involved don't matter, only the way they manipulate types do. Commutativity of conjunction, for example, is encoded by a function of type (A, B) → (B, A). That this function swaps the values in its input tuples is, for the Curry-Howard correspondence, just an unimportant side effect.
