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.