Soft linear logic (SLL) is a fragment of Linear logic, due to
Lafont, whose Curry-Howard isomorphism is with the polynomial-time
computable functions. We show that by extending SLL with unrestricted
comprehension we obtain a consistent presentation of Naive set theory.
In this system (soft set theory) the provably total functions are
precisely the polynomial time functions.
A particular novelty of this approach is that two distinct
representations of the naturals and
strings are necessary; these representations correspond closely to the
safe/normal distincion introduced by Bellantoni and Cook, and so the
work presented draws a bridge between the proof-theoretic and
function-algebra characteristaions of polynomial time.