×

Light affine set theory: A naive set theory of polynomial time. (English) Zbl 1048.03041

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.

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
PDFBibTeX XMLCite
Full Text: DOI