[bvssvni]

> Are you saying that Löb's axiom, which states that the provability of "the provability of p implies p" implies the provability of p, necessarily prejudices some implicit assumption of consistency to the meta-language?

Yes. One way to put it: Provability Logic is balancing on a knife-edge. It works, but just barely. However, you can turn it around and say the new notion is balancing on a knife-edge by requiring DAG (Directed Acyclic Graph) at meta-level. They way I see it, is that both approaches have implicit assumptions and you have to trade one with another.

I am working on an implementation of the new notion of provability (https://crates.io/crates/hooo), after finding the axioms last year (it took several months):

    pow_lift : a^b -> (a^b)^c

    tauto_hooo_imply : (a => b)^c -> (a^c => b^c)^true

    tauto_hooo_or : (a | b)^c -> (a^c | b^c)^true

As a modal logic the difference is surprisingly small, by swapping Löb's axiom with T. `tauto_hooo_imply` is slightly stronger than K.

The major difference is that `|- p` equals `p^true` instead of implying, if you treat `|-` as internal. If you treat it as external, then you can think of it as N + T.

I needed this theory to handle reasoning about tautological congruent operators.

However, once you have this, you can perfectly reason about various modal logical theories by keeping separate modality operators, including Provability Logic, e.g. `modal_n_to : N' -> all(a^true => □a)`.

So, it is not a tradeoff that loses Provability Logic. Instead, you get a "finalized" IPL for exponential propositions. This is why I think of as a natural way of extending IPL with some notion of provability.

[deltasepsilon]

Thanks for your response. I'm not very familiar with reasoning in modal logic so I'm finding it hard to get an intuition for your `^` operator. Yes, it does seem like some kind of generalized provability. 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?

This is very interesting, but unfortunately I have more mundane things to get to. Hopefully I'll find some time to play with your axioms and relearn whatever modal logic I once knew.

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

[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

[aeonik]

This reminds me of Heisenberg's uncertainty principle but at a much deeper and more generalized level.