Comment by fmap | Hacker News Reader

Comment by fmap | Hacker News Reader

Parent Full thread

> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true.

I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with Loeb's theorem). It's true that you cannot show that, say, second order arithmetic is consistent in the same system. In fact, every soundness proof (for a sufficiently strong logic) will have to be carried out in a stronger system.

There is a standard way around this, which has existed for a long time. You stratify the system by introducing universes. E.g. in type theory, a universe is a type of (codes for) small types. This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe.

In the concrete example of Martin-Loef type theory (MLTT) you can show that MLTT with n+1 universes contains a model of MLTT with n universes. On the other hand, adding more universes seems to be harmless as far as anyone knows.

Under the assumption that MLTT with a countably infinite number of universes is consistent and you restrict your formal system to only use a bounded number of universes, it is still possible to show that it is "reliable". It is "at least as reliable" as MLTT with countably many universes.

I will read the article later and update this post if there is something compelling in the paper. At the moment I'm just confused what the problem is, and would really appreciate it if you could expand on this.

> This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe.

As you say, this isn't quite self-trust. Another natural move is to relax the criterion of self-trust away from "it proves itself consistent" (impossible by incompleteness) towards "it assigns high probability that it has good beliefs". (Formalizations of this are in the paper.)

> At the moment I'm just confused what the problem is

In short, it would be nice to have a model of "good reasoning under deductive limitation", where "good reasoning" means something like "has accurate beliefs about all questions of interest" (for example, facts about the outputs of long-running computations), and where "deductive limitation" rules out the reasoning process "just wait for your theorem prover to decide the question".

Examples of long-running computations that are hard to compute exactly, but that we can sometimes still have reasonable beliefs about: optimal moves in chess, go, etc.; the accuracy of some ML system after a given training regimen; a weather-forecasting program that runs a gigantic series of simulations; and so on.

So by now I've actually read the (abridged) paper and skimmed the full paper. And the paper has nothing to do with consistency problems, since they only consider boolean propositional logic... Assigning consistent probabilities in the limit is indeed a much more interesting problem anyway.

Self-trust seems like a problem on paper, but the reality is that normal mathematics uses very few universes. Concretely, the proof of the Feit-Thompson theorem in Coq, with all the related theories, uses 4 universes. If you have a system certified in type theory, then you can still reason about it. Possibly one universe higher, but that is not a problem (as far as anybody knows).

>Self-trust seems like a problem on paper, but the reality is that normal mathematics uses very few universes.

Self-trust (broadly construed) is interesting to me because it seems relevant to designing goal-based agents that are "stable", in the sense that they trust that future versions of themselves will have accurate beliefs (and therefore don't have an incentive to mess around with their systems for forming beliefs). If we try to formalize this intuition with "beliefs" as theorems proven by a formal system, we run into reflection problems; having your theorem prover assert that it will keep outputting only true statements feels awfully close to asserting its own soundness. So even if your agent can perform all the usual mathematical reasoning it needs, it still can't do all the useful reasoning about itself (it would need another large cardinal... and then another...).

The self-trust property in the paper says that it's possible to "learn from experience" that your future self is probably going to have pretty good beliefs. Specifically, a logical inductor P_n learns (roughly speaking) that "if P_f(n) thinks Phi is likely, then Phi is likely", where f(n) can be a fast-growing computable function. That is, on day n, P_n believes a sort of "probabilistic soundness" condition for its future self P_f(n). This is weaker than full soundness in at least two ways, but it is fully "reflective" in the sense that P believes this of itself.

The expressiveness of the tower of universes limits to that of Peano arithmetic, correct? Otherwise, there would exist a universe k that contain theorems that could not be computably proven in universe k+1.

On a separate matter, are there any principled meta-universal rules for incrementing the universe index? That is, if one suspects that one's current universe lacks proving power, is it possible to generate the axioms for a more powerful universe?

Peano arithmetic, as in classical first-order logic with the peano axioms is a small subsystem of MLTT with natural numbers and no universes. If you come from a set theory background, then universes are really akin to Grothendieck universes, or large cardinal axioms. You start out with a powerful theory and then improve it by repeatedly adding statements of the form "and the theory so far is consistent", by giving an internal model of "the theory so far".

There are type theories with universe variables, which essentially allow you to add an arbitrary (but finite) number of additional universes. The rules for this are straightforward, even though a consistency proof is of course only possible relative to type theory or set theory with more universes...

In set theory, one typically adds an axiom scheme that states something like "There is a Grothendieck universe containing this set". Iterating this gives you a similar tower of universes.

There are a lot more constructions that go beyond this and the funny thing is that as far as anyone knows they are all consistent. For instance, type theories with induction-recursion allow you to generate internal universes closed under certain operations while staying in the same universe. So one universe with induction-recursion allows you to show MLTT with an arbitrary finite number of universes consistent.

[ For some work formalizing a reflection principle in HOL, see https://intelligence.org/files/ProofProducingReflection.pdf ]

Reply on news.ycombinator.com