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.
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.
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 (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.
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?
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.
There is always an external context that runs the computation. A computation never exists in "abstract space", it always happens on a physical level. Any computation is only good if it runs in the context that it was designed for.
What I mean is that the AI can never "know" if it's still following the "righteous goals", because a new environment may have grown around it, that "transforms" its inputs and outputs so that to the core machine it seems like nothing has changed, but actually its real-world effects have become very different. And at this point you could actually also say that this part of the environment has grown onto the AI machine and it now effectively has new goals that are incompatible with the ones designed into the core part of the machine.
My point is, there is no isolated system, reasoning by itself in an isolated fashion. Subject and environment are not clearly divided.
> at this point you could actually also say that this part of the environment has grown onto the AI machine
No, you cannot, if the environment is part of the definition of the machine, as you put it, A computation never exists in "abstract space", because if the environment changed, you'd have a new machine and all bets are off. You had that right at first.
Of course, that definition is unwieldy and we define interfaces as abstract and general as possible, to separate concerns. With involved machinery, that separation is not that clear cut, as their always two sides of the coin, to put it trivially.
This implies second order logic. It is not clear to me, whether the loss of consistency is warranted. Type Theories are tried to avoid inconsistence. However high the order of the processing logic is, its only reason to exist is to output first order theorems, those we can prove decidable.
> But with this article, the hope is that a formal system can show that the statement about itself is probably true.
Probabilty is not good enough. The Bayesian Conspiracy sure is strong, but I'd prefer to stay with first order logic and finite state machines that are provably correct.
> > The short answer is that this theorem illustrates the basic kind of self-reference involved when an algorithm considers its own output as part of the universe
Isn't that what differential equations are for? I'm tired of the liars paradoxon. Intuitively, I've settled on the presumption that paradoxa always rest on wrong assumptions.
I'm no mathematician, but I refuse the notion that I am inherently unable to be certain. That's why algorithms are by my preferred definition bound to be deterministic. I'd like to be able to tie this in with the Chomsky Hierarchy, albeit I am not that advanced. I'm no mathematician and I'm impressed by quines. I guess, the halting problem implies that quines cannot always be predicted. Heuristics help there and that's what stochastic is all about.
Let me be clear. The paradoxon "this sentence is a lie" is neither a sentence, nor a lie. That's a question of definition. Of course I'm in no position to say a similar thing about Goedels incompleteness theorem, and I even referred to it's result in higher order logics, but I still doubt the relevance, as many seem to be ignorant of his former completeness theorem.
The higher order logic and self reference is related to recursively enumerable grammars low in the Chomsky Hierarchy. Though, if ordered by magnitude, I'd call it higher. I hope, if the goal is natural language, we don't need to aim that high. If you want a computer that computes computers, though, go for it.
> A formal system cannot achieve this by simulating itself.
The type of self similarity used in quines or the liars paradox seems to play an important role in what we perceive as intelligent. Although, I stipulate, the intelligence involved is the ability to tell the difference between a misleading liars paradox and constructively provable quines. Of course, a machine that doesn't need verification from the supervising developer would be akin to a perpetuum mobile.
It is easy to supervise the AGI's output by the less intelligent machines that have to do the output. The focus is on optimizing the processes, not the inability to assert safety guidelines.
Edit: mixed up the order of the Chomsky Hierarchy.
No, it does not. The second incompleteness theorem is provable in first-order Peano Arithmetic.
> Of course I'm in no position to say a similar thing about Goedels incompleteness theorem, and I even referred to it's result in higher order logics, but I still doubt the relevance, as many seem to be ignorant of his former completeness theorem.
I have no idea what you're trying to say, but I assure you that people who do this kind of research are aware of the completeness theorem.
> A formal system cannot in general prove that it is reliable
I hadn't noticed when I wrote that, formal system is an idiom - even more specific in this specific context. How confusing.
Because there will always be statements that are true which the original system is oblivious to, and thus the corresponding questions will be outside its scope (incompleteness theorem).
The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified.
A formal system cannot achieve this by simulating itself.
A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true. http://intelligence.org/files/lob-notes-IAFF.pdf
But with this article, the hope is that a formal system can show that the statement about itself is probably true.