Terui, Kazushige Light affine set theory: A naive set theory of polynomial time. (English) Zbl 1048.03041 Stud. Log. 77, No. 1, 9-40 (2004). Summary: J.-Y. Girard [“Light linear logic”, Inf. Comput. 14, 175–204 (1998; Zbl 0912.03025)] introduced a naive set theory based on a polynomial-time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL. In this paper, we consider a naive set theory based on Intuitionistic Light Affine Logic (ILAL), a simplification of LLL introduced by A. Asperti [“Light affine logic”, 13th annual IEEE symposium on logic in computer science. Proceedings, 300–308 (1998; Zbl 0945.03533)], 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. Cited in 14 Documents MSC: 03E70 Nonclassical and second-order set theories 03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) 03F52 Proof-theoretic aspects of linear logic and other substructural logics Keywords:naive set theory; polynomial time; linear logic; light logic; substructural logics Citations:Zbl 0912.03025; Zbl 0945.03533 PDFBibTeX XMLCite \textit{K. Terui}, Stud. Log. 77, No. 1, 9--40 (2004; Zbl 1048.03041) Full Text: DOI