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.
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.
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.
> 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.
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?
“It is provable in system X that False” and “system X is inconsistent” are the same statement. That’s what it means for a system to be inconsistent: there is a proof in the system of the statement False.
So, no, you’re wrong: in probability logic, []False can be interpreted as “it is provable (in this system) that False”.
> It sounds like you are assuming HOOO EP is inconsistent?
While I do suspect it to be, that isn’t why I said that. I was saying that because you were seemingly saying that probability logic has a bias favoring reasoning from within a consistent system. And, I was saying, “why would you want to be reasoning within an inconsistent system? Shouldn’t something be suited for reasoning within a consistent system, seeing as reasoning in an inconsistent system gives you nonsense?”
> 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.
It didn’t provide me with the answer I was seeking, and so I will instead ask you directly again: what alternative notion of probability do you have in mind?
Asking "why do you want to be reasoning within an inconsistent system?" is like facing a dead end, because you are supposing a bias that was never there in the first place. As if, logic cares about what you want. You only get out what you put in. Bias in => bias out.
I am speculating about the following: If we don't bias ourselves in favor of consistency at the meta-level, then the correct notion of provability is HOOO EP. If we are biased, then the correct notion is Provability Logic.
In order to see HOOO EP as a provability notion, you have to interpret the axioms as a theory about provability. This requires mathematical intuition, for example, that you are able to distinguish a formal theory from its interpretation. Now, I can only suggest a formal theory, but the interpretation is up to users of that theory.
A notion can generally be prior to a particular formalization. If you have an alternative notion of probability in mind, you should be able to express it.
> Now, I can only suggest a formal theory, but the interpretation is up to users of that theory.
Ok, well, it has no users other than yourself, so if you want to communicate how it could be useful, I recommend you find a way of expressing/communicating an interpretation of it.
—- Also, I think your idea of a “bias towards consistency” is unclearly described at best.
Any pointers to that alternative notion?
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?
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
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.
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.
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
I suppose my followup to that is, why is this a problem? Does it lead to bad mathematics? (For what definition of “bad”?) Would we be able to solve unsolved problems if we tied things back to foundations more? Mathematicians have never really done much mathematics that ties back to the foundational axioms — why change? Rigor is not really much of an end in itself - surely people do mathematics because it is useful or beautiful, or both?
1. More formalized training data makes the math AI better
2. Better math AI helps us formalize more known mathematics
But right now math AI is not very useful. It isn't at the point where ChatGPT is for programming, where the AI is really helpful for a lot of programming tasks even if it isn't superhuman yet. So the virtuous cycle hasn't started yet. But I think we will get there.
So in theory, with a solid foundation for mathematics, and new work rigorously tied back to it, this sort of thing should be both easier and more efficient.
If somebody makes a proposition and nobody is able to properly vet it, or if you just get a bunch of white heads to nod sagely and endorse it, very little prevents there existing a flaw that invalidates the whole thing which might go unnoticed for decades and ruin anything anyone tries to build atop of the result.
It's the same as security hardening in code, or checking for med interactions at the pharmacists. Or checking to make sure that the absolutely correct pill is being dispensed and not mixed up "Buttle/Tuttle" style with some other similar looking pill.
Formal rigor paved all the way from the proposition to the axioms is not 100%, nothing is 100%. But formal rigor paved over that entire distance redistributes all potential for error to the proof chain itself which is now far easier for a non-AI computer to verify, and to the strength of the axioms themselves which have had more scrutiny paid to them than any other statements in the history of mathematics.
Another important point is that you do not have to go all the way back to the axioms if someone else has already formally proved other complex statements you can rely upon instead, then you only have to pave the length of your driveway to the nearest communal road.
The definition of a valid mathematical proof that I've heard mathematicians use is if it convinces other mathematicians. I think there's integrity in depth in mathematical proofs for lots of reasons, tying back to an axiomatic basis is a lot of extra work for likely no benefit.
On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.
1. I only need normal congruence
2. I only need perfect information games
Under problems that are solvable using these two assumptions, there is little benefit in tying proofs back to an axiomatic basis. Once you drop one of these two assumptions, proofs get much harder and a solid foundation gets more important.
But this is very different to suggesting that most regular mathematics will switch to using formal proofs. There's a big ergonomics gap at the moment.
An analogy could be to look how pure mathematicians look down on applied mathematicians' work, the applied mathematicians don't care, they just get on with their own standards. You need regular mathematicians to choose to switch over en masse, what will compel them to do that?
Which is happening right now — and the younger mathematicians who are supporting those efforts (and more broadly, things like Lean libraries) are gaining the experience while making the ergonomic changes.
That is, the person you’re replying to isn’t unaware of the historic problems: they’re pointing out that migration is starting now with early adopters like Tao and Scholze.
But let's say they make huge amounts of progress - they might improve the ergonomics enough that the formal foundations of mathematics will be brought into mathematics departments as a standard, legitimate and popular subject. But I still can't see how this would affect most mathematics.
It won't, in the same way that introducing physics didn't affect philosophers. They were still free to do philosophy. But most new innovation and innovators came up doing physics instead - and that's been where all the growth had been for centuries.
In the end ungrounded theory is better than nothing. But grounded theory beats out ungrounded theory hands down.
In the old days there were philosophers. They sought truth through thought and wisdom. Some started to measure reality and compare thought against that measurement, but real philosophers paid little heed for it didn't matter.
Testing their theory became known as physics. It turned out the testing against reality can be used without the theory, which we call engineering. We still have philosophers and they still pay little heed to measurement.
There is a similar disaster inbound for mathematicians. Formal mathematics is tedious and mostly only shows things that you were pretty sure were true anyway, so why bother.
It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.
> It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.
Formalized mathematics is just a very small subset of what mathematicians work on: in my observation people who work on (computer) formalized proofs often rather sit in CS departments.
Social Processes and Proofs of Theorems and Programs
Well, if you want them to be. I’m quite fascinated by the field of inconsistent mathematics, which attempts to show one can do real and useful mathematics given foundations which are at least tolerant of inconsistency (or even actually inconsistent)
https://plato.stanford.edu/entries/mathematics-inconsistent/
https://ir.canterbury.ac.nz/server/api/core/bitstreams/d6722...
Your assertion about the inevitability is true only under specific axioms. If you are willing to drop the notion that infinity exists, or the law of excluded middle (and maybe others), the problems that arise from Gödel's incompleteness theorems don't necessarily apply.
I'm very far from mathematician circles so I don't know how they actually interpret Gödel, but the idea of being "fairly confident" that math foundations are consistent while knowing that either there are true statements that we can't prove, or that the foundations aren't consistent, feels like a pretty weird thing to me.
I always thought most mathematicians just looked at Gödel like he discovered an interesting novelty, then ignored him and went back to doing whatever math they were already doing, instead of losing sleep over what his theorem implied.
Also, is it true that constructive mathamtics actually escapes Godel's theorems? My understanding was that any system strong enough to contain regular arithmetic is subject to it. Either way, constructive math is more limited in what it accepts as proofs, so there will be more, not fewer statements that are true but unprovable with such a system.
Biologists don't model behaviors based on the four fundamental forces of physics.
It seems like it should be possible, in theory, but it takes too much work.
i guess that a point can be made that, even though chemistry is just applied quantum electrodynamics, people seldom derive it from first principles
IMHO the problem now is that the foundations of mathematics are impractical. Most mathematicians don't actually do mathematics that can be tied back to the foundational axioms. It seems like it should be possible, in theory, but it takes too much work. So most mathematicians prefer communicating their proofs in PDFs rather than in a more rigorous format.