Very interesting. I did never really look at the "Concrete Mathematics" book, so I missed this take by Knuth on turning a formula F into a term [F] by defining it as 1 if F is true, and 0 if F is false. Note that this cannot be done in first-order logic, as a formula cannot be part of a term. But it is not a problem in simply-typed higher-order logic, for example, and it is not a problem in abstraction logic, either.
Thank you so much for this!!
The bit on "avoid ambiguity, or introduce useful ambiguity" is especially fascinating.