Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
431078 | The Journal of Logic and Algebraic Programming | 2008 | 20 Pages |
Abstract
A formulation of naïve set theory is given in Lafont’s Soft Linear Logic, a logic with polynomial time cut-elimination. We demonstrate that the provably total functions of this set theory are precisely the PTIME functions. A novelty of this approach is the representation of the unary/binary natural numbers by two distinct sets (the safe naturals and the soft naturals).
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics