If you look at where lambda comes from, it comes out of this same project of metamathematics that originates in the 19th century with people like Frege - how do you describe math in terms of math? Then it was discovered that this project could be repurposed as a definition of computing. Reusing old standards is a thing that happens, but sometimes you'd come up with a different approach if you were starting from scratch. As I've pointed out elsewhere on this thread, the shared theoretical foundation of lambda does not lead to a family of languages that are compatible in any meaningful sense.
It was probably a bad decision to make 0 true and 1 false, but not for mathematical reasons. There is always a lot of C coupled to Urbit, and what ends up happening is that the easiest way to handle this problem is to write C in a sort of dialect in which 0 is true and 1 is false. This is slightly cumbersome, and the perceived elegance of 0 == true isn't at all worth it. However, it's also nowhere near awful enough to revisit the question, which would be quite tricky considering the self-compiling nature of the system!
For instance, if you've got anything like regular expressions, then you've got something with a structure where the "unit" (trivial match) is an identity for sequencing, and the "zero" (failed match) is an identity for disjunction and a zero for sequencing. It's not exactly a formal argument for preferring booleans to loobeans, but a failed regex match sure feels like a "false" to me.
I don't doubt that it's not worth changing at this point, but don't throw the semiring baby out with the lambda bathwater.
S: λxyz.xz(yz)
K: λxy.x
I: λx.x
From there, you can express anything from the lambda calculus, and vice-versa. So I think it's reasonable to say that Nock is just a machine-friendly way of expressing the lambda calculus.
SKI is obviously a lot simpler mathematically, but I wouldn't want to try to use it as a compiler target...
You can go simpler still: Iota.