2 ms·

I found this by Knuth on Iverson's notation interesting: https://www.maa.org/sites/default/files/images/images/upload_library/22/Ford/knuth403-422.pdf https://w

• practal 4y ago
  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.