Intuitionistic Mathematics and Realizability in the Physical World
- 04 March 2014
- Computation, Publications
This is a draft version of my contribution to “A Computable Universe: Understanding and Exploring Nature as Computation”, edited by Hector Zenil. Consider it a teaser for the rest of the book, which contains papers by an impressive list of authors.
Abstract: Intuitionistic mathematics perceives subtle variations in meaning where classical mathematics asserts equivalence, and permits geometrically and computationally motivated axioms that classical mathematics prohibits. It is therefore well-suited as a logical foundation on which questions about computability in the real world are studied. The realizability interpretation explains the computational content of intuitionistic mathematics, and relates it to classical models of computation, as well as to more speculative ones that push the laws of physics to their limits. Through the realizability interpretation Brouwerian continuity principles and Markovian computability axioms become statements about the computational nature of the physical world.
Download: real-world-realizability.pdf
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
Very nice paper. I like it a lot.
Minor grammar comment: On page 10, you say "how many digits of x suf?ce to compute the ?rst n digit of f(x)." You are missing an "s" after "digit".
What fun! Reminds me a bit of the also quite fun quant-ph/0502072.
This is a very awesome, friendly, short paper; I'm using it to get some of my curious friends introduced to higher math. However, one thing worries me. Let $h(x) = 1/x$. This should certainly be definable for $x > 0$. Then micro-affinity implies the existence of a unique $k$ such that for all infinitesimal $dx$, $h(1+dx)-h(1) = k \, dx$. Now, $h(1+dx) - h(1) = 1/(1+dx) - 1 = - dx/(1+dx) = k \, dx$. This worries me. I'm not quite sure I can get a contradiction from it, because not every infinitesimal is invertible, but it still makes me feel uncomfortable. This probably stems from me not knowing synthetic differential geometry and making a logic error somewhere. The paper is (mercifully!) not explicit about how the reals are constructed, maybe the problem is hiding in there somewhere? Or maybe this is all correct and it's my intuition that's wrong? Anyways, thanks for the clear exposition.
@Luke: we have $1/(1 + dx) = 1 - dx$ because $(1 + dx) (1 - dx) = 1 - dx^2 = 1$. Thus, your calculation can be continued: $h(1 + dx) - h(1) = -dx / (1 + dx) = -dx (1 - dx) = -dx + dx^2 = -dx$ and so clearly $k = -1$.
Note that from $k \, dx = -dx / (1 + dx)$ you cannot conclude $k = -1/(1 + dx)$ because the law of cancelation does not apply. Recall the law of cancelation: "if $a, b \in R$ such that $a \, dx = b \, dx$ for all $dx \in \Delta$ then $a = b$." In our case we have a problem: we can take $a = k$, but $b$ cannot be $-1/(1 + dx)$ because it is supposed to be a fixed real, independent of $dx$.
Does this dispell the mystery?
@Andrej: Very much so! I felt that cancellation probably didn't apply because the thing to be cancelled wasn't independent of dx, and I realized that I hadn't done any simplification yet using that dx^2 = 0, which seemed wrong. This clears everything up quite nicely. Thanks!