To any model of computation, such as lambda calculus or Turing machines, there is an associated "effective topos". This is an alternate mathematical universe in which—for reasons related to computability not the usual laws of logic hold.
For instance, for some models, anti-classical dream axioms like "any function ℝ → ℝ is continuous" and "any function ℕ → ℕ is computable" hold. The law of excluded middle however, "any proposition is either true or not true", is falsified in those toposes.
The effective topos has especially wondrous properties in case we employ models of hypercomputation, where computers can perform infinitely many calculational steps in finite time: Andrej Bauer proved that then the effective topos contains an injection ℝ → ℕ.
We can also employ physical models about the real world. In this case, statements which are in classical mathematics simply true become non-trivial statements about the nature of the physical world when interpreted in the effective topos.
Topos theory therefore provides an apt vehicle to study computation and alternative axioms of logic. Other applications include mechanical extraction of programs from proofs and a reconciliationcof platonism with formalism.
The talk strives to give an accessible introduction to this circle of ideas, also resolving any apparent paradoxes in this abstract. No prerequisites in topos theory or the theory of computation are needed. |