[bvssvni]

> Does `a^b` mean `a` is provable in all worlds in which `b` is valid, i.e. taken as an axiom in the underlying proof theory, or something like that?

Yes. You can also think of it as a function pointer `b -> a`. Unlike lambdas/closures, a function pointer can not capture variables from the environment. So, if you have a function pointer of type `b -> a`, then you can produce an element of type `a` from an element of type `b`.

This sounds almost like the same thing as with lambdas/closures. The difference is that a lambda can capture variables from the environment, such that `b => a` is possible "at run-time" in a way that does not hold for every possible world. So, the distinction between function pointers and lambdas/closures can be thought of as different notions of provability at static compile-time and dynamic run-time.

> One more thing, what are you calling `N`?

N is the name of the axiom in Modal Logic. It is called the "Necessitation Rule". See https://en.wikipedia.org/wiki/Modal_logic#Axiomatic_systems