Light Affine Set Theory: A Naive Set Theory of Polynomial Time

Abstract

In this paper, we consider a naive set theory based on intuitionistic light affine logic (ILAL), a simplification of LLL introduced, and call it light affine set theory (LAST). The simplicity of LAST allows us to rigorously verify its polytime character. In particular, we prove that a function over (0, 1) is computable in polynomial time if and only if it is provably total in LAST. (edited)