Well, that depends on what you take to be decent. In the sibling, shinoteki has pointed (via Nik Weaver) to J_2. As Weaver argues, this is plenty strong enough to do ordinary mathematics: the mathematics that most mathematicians work on, and the mathematics that (almost always, perhaps absolutely always) is used in real-world applications. On the other hand, I find it difficult to work with, and prefer explicit reasoning about sets (but I’m a mathematician, so maybe I’m just used to that). That said, I think that properly limiting the impredicativity of set-based constructions should allow one to create a set-like theory that corresponds to something like J_2. (I’m being vague here because I don’t know better; it’s possible, I’d even say likely, that other mathematicians know better responses.)
Well, that depends on what you take to be decent. In the sibling, shinoteki has pointed (via Nik Weaver) to J_2. As Weaver argues, this is plenty strong enough to do ordinary mathematics: the mathematics that most mathematicians work on, and the mathematics that (almost always, perhaps absolutely always) is used in real-world applications. On the other hand, I find it difficult to work with, and prefer explicit reasoning about sets (but I’m a mathematician, so maybe I’m just used to that). That said, I think that properly limiting the impredicativity of set-based constructions should allow one to create a set-like theory that corresponds to something like J_2. (I’m being vague here because I don’t know better; it’s possible, I’d even say likely, that other mathematicians know better responses.)