> but I don't think that's a total pipe dream You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a mode

> but I don't think that's a total pipe dream You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a model and its proof theory aesthetically unappealing (not that I find everything in formal FO set theories appealing). Of course, it may have other advantages. > Would that really be enough to make you say that these are functions now while they previously weren't? Yes, provided that `id` wouldn't be a function that could operate on that type. But any operator with a truly universal domain cannot be, itself, a quantifiable object without introducing a Russell paradox (perhaps constructiveness can save it, but assuming the system allows non-computable objects, too). As it is, `id` is universal, but it isn't a function. This isn't just a philosophical or even a purely syntactic difference. Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. > so not having a specific universe isn't an issue. Does that require forbidding full recursion, or can you still introduce non-computable objects?