Logic seminar

Unearthing the Feasible World: A Proposal

The decades-long practice of complexity theory and bounded arithmetic provided some strong clues for the existence of an alternative yet rich feasible world, where for instance all the functions are feasible and the polynomially and exponentially bounded sets are the new finite and infinite, respectively. The situation is similar to the so-called computable and continuous worlds whose traces first unearthed in constructive mathematics and later realized by the forcing-style model constructions that elevated to a general and conceptual theory called the topos theory. In this talk, imitating the main ideas of topos theory, we propose a program to provide a general machinery for the feasible forcing in order to prove some independence results for weak arithmetic, on the one hand and find a conceptual understanding of the low complexity computation, on the other.

As we will see, any fulfillment of that proposal needs a certain (geometric) form of structural theory and one canonical base model. We will report some of our partial results to find these two ingredients. For the first, we will present our structural theory for the low complexity versions of the inductive objects like the natural numbers, binary strings, ordinals and sets. For the latter, we will explain our imitation of Hyland's construction of the computable world (effective topos) for the feasible functions and the problematic role of the intuitionistic implication there that leads to our general theory of implication and its inherent non-geometricity. Despite what it appears at the first glance, we will not assume any familiarity with category theory and topos theory and the talk will be rather informal in this respect.