Comment by bvssvni

2 years ago

One thing I would like point out with Gödel's incompleteness theorems, is that there are different notions of provability. Gödel uses the notion of "provability" you get from Provability Logic, which is a modal logic where you introduce terms from e.g. Sequent Calculus.

Recently I found another notion of "provability" where Löb's axiom, required in Provability Logic, is absurd. It turns out that this notion fits better with Intuitionistic Propositional Logic than Provability Logic. This allows integrating the meta-language into object-language. This is pretty recent, so I think we still have much to learn about the foundations of mathematics.

14 comments

bvssvni

Reply
drdeca  2 years ago

This makes it kind of sound as if Löb's axiom is used in the proof of Gödel's incompleteness theorems, but Gödel was working in (I think) PA, not in Provability Logic?

I guess you just meant "the notion of provability is the same as the one that would later be described in Provability logic" ?

I viewed the page you linked, but I don't see anywhere where you describe the alternate notion of "provability" you have in mind.

"Provability" in the sense of Gödel's incompleteness theorems, is just, "There exists a proof of it in [the chosen system of axioms + rules of inference]", yes? I don't see how any other notion would be fitting of the name "provability". "provable" , "possible to prove", "a proof exists", all the same thing?

Oh, I guess, if you want to use "there exists" in a specifically constructive/intuitionistic way? (so that to prove "[]P" you would have to show that you can produce a proof of P?)

I think I've seen other people try to do away with the need for a meta-language / make it the same as the object-language, and, I think this generally ends up being inconsistent in the attempts I've seen?

edit: I see you have written 'Self quality a ~~ a is equivalent to ~a, which is called a "qubit".'

I don't know quite what you mean by this, but, _please_ do not call this a qubit, unless you literally mean something whose value is a vector in a 2d Hilbert space.

  • bvssvni  2 years ago

    > I guess you just meant "the notion of provability is the same as the one that would later be described in Provability logic" ?

    yes

    > I viewed the page you linked, but I don't see anywhere where you describe the alternate notion of "provability" you have in mind.

    See section "HOOO EP"

    >Oh, I guess, if you want to use "there exists" in a specifically constructive/intuitionistic way? (so that to prove "[]P" you would have to show that you can produce a proof of P?)

    This would be `|- p` implies `□p`, which is the N axiom in modal logic (used by Provability Logic).

    In Provability Logic, you can't prove `□false => false`. If you can prove this, then Löb's axiom implies `false`, hence absurd. `□p => p` for all `p` is the T axiom in modal logic. In IPL, if have `true |- false`, then naturally you can prove `false`. So, you can only prove `□false => false` if you already have an inconsistent theory.

    Provability Logic is biased toward languages that assume that the theory is consistent. However, if you want to treat provability from a perspective of any possible theory, then favoring consistency at meta-level is subjective.

    > I think I've seen other people try to do away with the need for a meta-language / make it the same as the object-language, and, I think this generally ends up being inconsistent in the attempts I've seen?

    I have given this some thought before and I think it is based on fix-point results of predicates of one argument in Provability Logic. For example, in Gödel's proof, he needs to encode a predicate without arguments in order to create the Gödel sentence. In a language without such fix-points, this might not be a problem.

    > I don't know quite what you mean by this, but, _please_ do not call this a qubit, unless you literally mean something whose value is a vector in a 2d Hilbert space.

    The name "qubit" comes from the classical model, where you generate a random truth table using the input bit vector as seed. So, the proposition is in super-position of all propositions and hence behaves like a "qubit" in a classical approximation of a quantum circuit.

    • drdeca  2 years ago

      Something being random and/or undetermined is not sufficient for it to be like a qubit. You need the linear algebra aspect for the name to be appropriate, IMO.

      > See section "HOOO EP"

      I have looked through that section, and afaict, nowhere in it do you define an alternative notion of “provability”?

      > In Provability Logic, you can't prove `□false => false`. If you can prove this, then Löb's axiom implies `false`, hence absurd.

      Why do you expect to be able to prove `□false => false` ? I.e. why do you expect to be able to prove `not □false`, i.e. prove the consistency of the system you are working in.

      > Provability Logic is biased toward languages that assume that the theory is consistent. However, if you want to treat provability from a perspective of any possible theory, then favoring consistency at meta-level is subjective.

      I’m not really sure what you mean by “favoring [...] is subjective.” . Also, if you want to do reasoning from within an inconsistent theory, then I’d hope it is at least paraconsistent, as otherwise you aren’t going to get much of value? Or at least, nothing with any guarantee. If you aren’t aiming at a paraconsistent logic, I don’t follow your point about not wanting to favor the assumption that the system is consistent.

      4 replies →

deltasepsilon  2 years ago

I'm attempting to understand you, so:

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?

How so, and/or, what are the axioms, or derived properties, of this new notion of provability you have uncovered?

  • bvssvni  2 years ago

    > 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  2 years ago

      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`?

      1 reply →

    • aeonik  2 years ago

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