From the introduction to Jean-Louis Krivine's paper,
Realizability Algebras: A Program to Well-Order $\mathbb{R}$:
Indeed, when we realize usual axioms of mathematics, we need to introduce, one after the other, the very standard tools in system programming: for the law of Peirce, these are continuations (particularly useful for exceptions); for the axiom of dependent choice, these are the clock and the process numbering; for the ultrafilter axiom and the well ordering of $\mathbb{R}$, these are no less than read and write instructions on a global memory, in other words assignment.
A better example of
consilience I cannot imagine!
No comments:
Post a Comment