Fwiw, this is called the BHK or Brouwer–Heyting–Kolmogorov interpretation. It's a way of providing a model of intuitionistic logic in the same way that "sets" p

Fwiw, this is called the BHK or Brouwer–Heyting–Kolmogorov interpretation. It's a way of providing a model of intuitionistic logic in the same way that "sets" provide a model of classical logic. Intuitionistic logic this should hold some kind of meaning independent of BHK, but BHK can help in your examination of Intuitionistic logic. https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...