[bvssvni]

> 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]

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.

[bvssvni]

> 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.

Naming things is hard. Given how constrained Propositional Language is as a language, I do not think there is much risk of misinterpreting it. I needed something to associate with "superposition" but also fit with "quality". Both "qubit" and "quality" starts with "qu", so I liked the name.

It does not bother me if people find another better name for it.

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

I do not want to create a controversy around Provability Logic by making too strong claims for some people's taste. What I meant is that this section is explaining HOOO EP and my interest is in communicating what it is on its own sake, without needing to compare it to Provability Logic all the time. However, since HOOO EP is so similar to Provability Logic, it requires some clarification. I hope you found the section useful even though you were not able to see how it is an alternative notion of provability from its definition.

> 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.

I think this is trying to think about logic as a peculiar way. HOOO EP was not developed to reason about consistency. It has its own motivation that makes sense. However, once you have HOOO EP, you can start discussing how it relates to consistency of theories.

It makes sense, in a sense of consistency, from the perspective where an inconsistent theory is absurd. Absurd theories can prove anything, so there is no distinction between true and false statements. Now, if you interpret `□false` as an assumption that one can prove false, then of course, one can prove false. `□false => false` is the same as `!□false`. Does this mean that it proves its own consistency? No, because you made the assumption `□false`. You have only talked about what you can prove in the context of `□false`. From this perspective, `□false => false` is trivially true.

Provability Logic does not allow you to think of `□false` as meaning "I can prove `false`". Instead, it is interpreted as "this theory is inconsistent" but without assigning this statement a particular meaning. This means, there is a gap between "I can prove `false`" and "this theory is inconsistent". Now, if you ignore the gap, then you are just making an error of interpretation. You have to respect the formal sense, where Provability Logic can have two different notions of absurdity while naturally you would think of them as one. However, if you want to have one instead of two, then you need HOOO EP.

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

It sounds like you are assuming HOOO EP is inconsistent? Why are you speculating about my motivations in a such context?