A doesn’t need B to believe that the logic is sound. Even if you decide to present “logic L plus metalogical beliefs” as a larger logic L’ (and assuming you manage to do this in a way that doesn’t lead to inconsistency), the semantic map is defined on L, not on L’.
My problem is that I still don’t understand how you propose for the agent to reason/behave differently than what I’ve described; so, your statement that it does in fact do something different doesn’t help me much, sorry.
The semantic map is defined on L, not L’—sure, this makes some sense? But this just seems to reinforce the idea that our agent can only “understand” the internal logic of agents who restrict themselves to only use L (not any meta-logical beliefs).
Even if you decide to present “logic L plus metalogical beliefs” as a larger logic L’ (and assuming you manage to do this in a way that doesn’t lead to inconsistency), [...] I didn’t understand this remark; please could you clarify?
Seems like you missed my point that the meta-logical belief could just be “L is sound” rather than “L plus me is sound”. Adding the first as an axiom to L is fine (it results in an L’ which is sound if L was sound), while adding the second as an axiom is very rarely fine (it proves soundness and consistency of the whole system, so the whole system had better be too weak for Godel’s incompleteness theorems to apply).
Does that make sense?
You were talking about the second sort of situation (where adding the meta-logical belief as an axiom would result in an inconsistent system, because it would claim its own soundness); I wanted to point out that we could also be in the first sort of situation (where adding the meta-logical belief would result in a perfectly consistent system, but would only let you trust L, not L’).
>I don’t understand why you would put truth on the “ought” side of the is/ought divide, or if you do, how it helps us out here.
To put soundness in is/ought form, the belief that A must hold is that “if phi is provable in L, the interpretation of phi (via the semantic map) ought to be true”.
To me, this “ought” in the sentence reads as a prediction (basically an abuse of ‘ought’, which is in common usage basically because people make is/ought errors). I would prefer to re-phrase as “if phi is provable in L, then the interpretation of phi will be true” or less ambitiously “will probably be true”.
Is your proposal that “X is true” should be taken as a statement of X’s desirability, instead? Or perhaps X’s normativity? That’s what it means to put it on the “ought” side, to me. If it means something different to you, we need to start over with the question of what the is/ought divide refers to.
Truth can’t be moved to the other side, because as I’ve tried to explain (perhaps unsuccessfully) the logic doesn’t include its own semantics, and it’s always possible to take contrarian semantics which fail to be sound applications of L. (see also final point below)
I agree that (by Tarski’s undefinability theorem) a logic can’t know its own semantic map (provided it meets the assumptions of that theorem). At least, if we’re on the same page about what a semantic map is.
However, Tarski’s analysis also shows how to build a stronger logic L’ which knows the semantic map for L. So if “move to the other side” means represent via more formal axioms (which is what I take you to mean), you seem to be wrong.
The interpretation which results in the Löbian Obstacle is “Löb’s theorem tells us that a logical agent can’t trust its own reasoning, because it can’t prove that reasoning is sound,” and under that interpretation it seems that extreme measures must be taken to make formal logic relevant to AI reasoning, which is counterintuitive since we humans employ formalizable reasoning every day without any such caveats. In this post I’m saying “Löb’s theorem reminds us that a logical agent cannot make a priori claims about the soundness of its own reasoning, because soundness is a statement about a semantic map, which the logic has no a priori control over”.
My problem with the general format of this argument is, the other interpretation of Lob’s theorem is still valid even if you re-interpret it. That is: Eliezer et al show that the assumptions of Lob’s theorem apply, and thereby, they conclude a formal result. No amound of re-interpreting the theorem changes that; one might as well suggest that we solve the Lobstacle by forgetting Lob’s theorem.
That is what I meant when I said I don’t get how it helps.
It seems to me like your post is missing a step where you design an alternative agent based on your improved thinking. Probably the alternative agent is supposed to be obvious from what you wrote, but I’m not getting it.
No, the agent doesn’t change its reasoning.
So how do you escape the conclusion from the paper??
Assume that the agent A is reasoning soundly about their environment, which is to say that their semantic mapping is sound. Then A’s belief in the soundness of their reasoning is justified.
Justified, perhaps, but also non-existent, right? You say the agent doesn’t change its reasoning. So the reasoning is exactly the same as the lobstacle agent from the paper. So it doesn’t conclude its own soundness. Right??
The change is that we don’t require A to prove that their semantic mapping is sound, because A cannot do that, and I’m claiming that this doesn’t break anything.
I have a couple of possible interpretations of what you might mean here, all of them really poor:
You’re saying that we allow the agent to conclude its own soundness without going through anything involving the semantic map, since it can’t possibly do that. But this seems to just result in an inconsistent agent, by Godel’s second theorem. Probably you don’t mean this.
You’re saying that we don’t change anything about the agent design; but we, as designers, don’t worry about the agent being able to reason about its own semantic map. Here, the question is, how does this help us? We still have the same bad agent designs. Probably this isn’t what you mean either.
If you want me to make it more formal, here: suppose I have a logic L and a universe U. For simplicity, let’s say U is a set. The semantic mapping is a map from the collection of formulas of L to the collection of concepts in U; it may be the case that symbols in L get mapped to collections of objects, or collections of collections, but for argument’s sake we can assume the codomain to be some number of applications of the powerset operation to U, forming a collection C(U) of “concepts”. So it’s a mapping S: L --> C(U). The crucial thing is that S is not a member of C(U), so it can’t be the image of any symbol in L under S. That is, S is outside the realm of things described by S, and this is true for any such S! Since “phi is provable in L means phi is true under S” is a statement involving S (even if the ‘under S’ is usually left implicit), it cannot be the interpretation under S of any formula in L, and so cannot be stated, let alone proved.
Right, so, we seem to be on the same page about what the semantic map basically is and Tarski’s undefinability theorem and such.
But what I need is a sketch of the agent that you claim solves the Lobstacle.
Most of the logics we encounter in mathematical practice are built with an intended semantics. For example, Peano Arithmetic contains a bunch of symbols which are often informally treated as if they are “the” natural numbers, despite the fact that they are no more than formal symbols and that the standard natural numbers are not the only model of the theory. In the context of logic applied to AI, this results in a conflation between the symbols in a logic employed by an agent and the “intended meaning” of those labels. This happens in the logical induction paper when discussing PA: the formulas the agent handles are assumed to carry their intended meaning in arithmetic.
Actually, that’s misconstruing the formal results of the paper, since logical inductors have formal systems as their subjects rather than any fixed semantics. However, it’s clear from the motivation and commentary (even within the abstract) that the envisaged use-case for inductors is to model an agent forming beliefs about the truth of formal statements, which is to say their validity in some specific model/semantics.
Sure, but logical induction doesn’t know anything about the intended semantics. It doesn’t make a lick of difference to the algorithm whether you believe that PA refers to the standard model. Nor does it feature in the mathematical results.
So I would put it to you that logical induction does a good job of capturing what it means to reason in a semantics-ignorant way. If it also works well as a model of reasoning for semantic-ful things, well, that would seem to be a happy accident. And perhaps it doesn’t: perhaps logical induction is missing an aspect of rationality around “semantics”.
Thus, logical induction would appear to be precisely what you call for at the end of your post: a theory of rationality which reasons in a semantics-independent way.
Seems like you missed my point that the meta-logical belief could just be “L is sound” rather than “L plus me is sound”. Adding the first as an axiom to L is fine (it results in an L’ which is sound if L was sound), while adding the second as an axiom is very rarely fine (it proves soundness and consistency of the whole system, so the whole system had better be too weak for Godel’s incompleteness theorems to apply).
Aha! I knew I must be missing something, thanks for the clarification. That makes things easier. I’ll continue to use L’ to mean “L + Sound(L,S)”, where S is a particular semantic map.
> A doesn’t need B to believe that the logic is sound. Even if you decide to present “logic L plus metalogical beliefs” as a larger logic L’ (and assuming you manage to do this in a way that doesn’t lead to inconsistency), the semantic map is defined on L, not on L’.
My problem is that I still don’t understand how you propose for the agent to reason/behave differently than what I’ve described; so, your statement that it does in fact do something different doesn’t help me much, sorry.
The semantic map is defined on L, not L’—sure, this makes some sense? But this just seems to reinforce the idea that our agent can only “understand” the internal logic of agents who restrict themselves to only use L (not any meta-logical beliefs).
The Löbian obstacle is about trust in the reasoning performed by a subordinate agent; the promise of subsequent actions taken based on that reasoning are just a pretext for considering that formal problem. So if A constructs B to produce proofs in L, it doesn’t matter what B’s beliefs are, or even if B has any beliefs; B could just be manipulating these as formal expressions. If you insist that B’s beliefs be incorporated into its reasoning, as you seem to want to (more on that below), then I’m saying it doesn’t matter what extension of L the agent B is equipped with; it can even be an inconsistent extension, as long as only valid L-proofs are produced.
To me, this “ought” in the sentence reads as a prediction (basically an abuse of ‘ought’, which is in common usage basically because people make is/ought errors). I would prefer to re-phrase as “if phi is provable in L, then the interpretation of phi will be true” or less ambitiously “will probably be true”.
Is your proposal that “X is true” should be taken as a statement of X’s desirability, instead? Or perhaps X’s normativity? That’s what it means to put it on the “ought” side, to me. If it means something different to you, we need to start over with the question of what the is/ought divide refers to.
The word “normative” sticks out to me as potential common ground here, so I’ll use that language. The specified semantic map determines what is “actually” true, but its content is not a priori knowledge. As such, the only way for A’s reasoning in L to have any practical value is if A works under the (normative) assumption that provability implies/will imply truth under S.
If this sounds farfetched, consider how police dramas employ the normative nature of truth for dramatic effect on a regular basis. A rogue detective uses principles of reasoning that their superiors deem invalid, so that the latter do not expect the detective’s deductions to yield results in reality… Or perhaps the practice of constructive mathematics would be a more comfortable example, where the axiom of choice is rejected in favour of weaker deductive principles. A dedicated constructivist could reasonably make the claim that their chosen fragment of logic determines what “ought” to be true.
However, Tarski’s analysis also shows how to build a stronger logic L’ which knows the semantic map for L. So if “move to the other side” means represent via more formal axioms (which is what I take you to mean), you seem to be wrong.
A compromise which was suggested to me this past week is to work with a two-level logic. It seems to me disingenuous that “A reasons in L” should mean “actually, A reasons in the stronger logic L’ which incorporates all the axioms it needs to ensure that provability in L implies truth”, as the Tarskian construction suggests. After all, if A attempts to justify that decision to itself, it seems to me to trigger an infinite regress of more and more powerful logics. Identifying and segregating the axioms which refer to the semantic map S as “meta-logical beliefs” is enough to avoid such an existential crisis, just as we only need to employ PA + Sound(PA,N), where N is our favourite model of the natural numbers, to use PA to reason about those natural numbers.
Justified, perhaps, but also non-existent, right? You say the agent doesn’t change its reasoning. So the reasoning is exactly the same as the lobstacle agent from the paper. So it doesn’t conclude its own soundness. Right??
You seem exasperated that I’m not incorporating the meta-logical beliefs into the formal system, but this is because in practice meta-logical beliefs are entirely implicit, and do not appear in the reasoning system used by agents. If I build a chess-playing robot, its program will not explicitly include the assumption that the rules of chess it carries are the correct ones, nor will it use such assumptions in determining its moves, because such determinations are made without any reference to a semantic map. This is why I said the agent doesn’t change its reasoning.
The metalogical beliefs thus are only relevant when an agent applies its (completed) reasoning to its environment via the semantic map. We can formalize that situation via the extended logic L’ if you like, in which case this is probably the answer that you keep demanding:
Both A and B “reason” in L’ (B could even work in a distinct extension of L), but will only accept proofs in the fragment L. Since the axioms in L’ extending L are identifiable by their reference to the semantic mapping, there is no risk of “belief contamination” in proofs, if that were ever a concern.
I expect there is more I should say to justify how this avoids the obstacle, but I will wait for your feedback first.
Sure, but logical induction doesn’t know anything about the intended semantics. It doesn’t make a lick of difference to the algorithm whether you believe that PA refers to the standard model. Nor does it feature in the mathematical results.
Thus, logical induction would appear to be precisely what you call for at the end of your post: a theory of rationality which reasons in a semantics-independent way.
Without an intended semantics, what the probabilities assigned to formulas can only be interpreted as beliefs/levels of certainty about provability of statements from axioms (which it also believes with more or less certainty). This is great, but as soon as you want your logical inductor to reason about a particular mathematical object, the only way to turn those beliefs about provability into beliefs about truth in the model, you need to extend the inductor (explicitly or implicitly) with meta-logical beliefs about the soundness of that map, since it will update its beliefs based on provability even if its proof methods aren’t sound.
As such, I feel you’ve misunderstood me here. I don’t want semantics-independent reasoning at all, if anything the opposite: reasoning that prioritises verifying soundness of a logic wrt specified semantic maps in an empirical way, and which can adapt its reasoning system when soundness is shown to fail. A logical inductor isn’t equipped with the capacity to work in mere fragments of its logic (it could be modified to do so, but that’s certainly not the main point of this algorithm, as I understand it), so can only go as far as identifying when its reasoning is not sound by observing that it believes a contradiction, without being able to do anything about it besides modifying the beliefs it holds in its axioms indefinitely.
The Löbian obstacle is about trust in the reasoning performed by a subordinate agent; the promise of subsequent actions taken based on that reasoning are just a pretext for considering that formal problem. So if A constructs B to produce proofs in L, it doesn’t matter what B’s beliefs are, or even if B has any beliefs; B could just be manipulating these as formal expressions. If you insist that B’s beliefs be incorporated into its reasoning, as you seem to want to (more on that below), then I’m saying it doesn’t matter what extension of L the agent B is equipped with; it can even be an inconsistent extension, as long as only valid L-proofs are produced.
I’m not insisting on anything about the agent design; I simply remain puzzled how your proposal differs from the one in the paper, and so, continue to assume it’s like the one in the paper except those differences which I understand. Your statements have been reading almost like you think you’ve refuted formal arguments in the paper (implying you don’t think the formal agent designs do what I think they do), rather than providing a new agent design which does better. This contributes to my feeling that you are really just wrestling with Lob’s theorem itself. Nor do I recall you saying much to dissuade me of this. In your OP, you use the language “Under the belief that the Löbian Obstacle was a genuine problem to be avoided”, as if the original idea was simply mistaken.
So, to be absolutely clear on this: do you accept the mathematical proofs in the original paper (but propose some way around them), or do you think they are actually mistaken? Do you accept the proof of Lob’s theorem itself, or do you think it is mistaken?
So if A constructs B to produce proofs in L, it doesn’t matter what B’s beliefs are, or even if B has any beliefs;
But using proofs in L is precisely what I understood from “belief”; so, if you have something else in mind, I will need clarification.
The word “normative” sticks out to me as potential common ground here, so I’ll use that language. The specified semantic map determines what is “actually” true, but its content is not a priori knowledge. As such, the only way for A’s reasoning in L to have any practical value is if A works under the (normative) assumption that provability implies/will imply truth under S.
If this sounds farfetched, consider how police dramas employ the normative nature of truth for dramatic effect on a regular basis. A rogue detective uses principles of reasoning that their superiors deem invalid, so that the latter do not expect the detective’s deductions to yield results in reality… Or perhaps the practice of constructive mathematics would be a more comfortable example, where the axiom of choice is rejected in favour of weaker deductive principles. A dedicated constructivist could reasonably make the claim that their chosen fragment of logic determines what “ought” to be true.
I think I haven’t understood much of this.
As such, the only way for A’s reasoning in L to have any practical value is if A works under the (normative) assumption that provability implies/will imply truth under S.
I would argue that the only way for A’s reasoning in L to have practical value is for A to act on such reasoning. The only way for A’s reasoning to have practical value for some other agent B is for B to be working under the assumption that provability-in-L implies truth under S. Indeed, this seems in line with your detective drama example. If the superiors were put in the position of the rogue detective, often they would have come to the same conclusion. Yet, looking at the problem from a removed position, they cannot accept the conclusion. But this is precisely the lobstacle: the condition for reasoning to have value to an agent A is different from the condition for A’s reasoning to have value to another agent B.
Let me therefore make a (not totally formal) distinction based on the alief/belief idea:
The aliefs of a logic-based agent are the axioms/theorems which inform action;
The beliefs of a logic-based agent are the axioms/theorems which the agent explicitly endorses.
This is also a version of the distinction between tacit knowledge (eg knowing how to ride a bike) vs explicit knowledge (eg being able to explain scientifically how bike-riding works). To say that an agent “alieves” a logic L is to say that it tacitly knows how to reason in L.
Roughly, I think you have been talking about beliefs, where I have been talking about aliefs.
Now, a “naive logical agent” (ie the simple agent design which falls prey to the Lobstacle, in the paper) has a few important properties:
Goedel’s incompleteness theorems tells us that aliefs cannot equal beliefs; a logic never explicitly endorses itself, but rather, only explicitly endorses weaker logics.
An agent constructed based on the logic L alieves L, but does not believe L (this is a re-statement of the lobstacle).
An agent can only trust another agent if it believes that agent’s aliefs.
An agent therefore cannot belief its own aliefs. (This is another restatement of the lobstacle.)
These statements are not necessarily true of logical agents in general, of course, since the paper gives some counterexamples (agents who can trust the same logic which they base their actions on). But those counterexamples all have some oddities. I presume your goal is to get rid of those oddities while still avoiding the lobstacle.
You seem exasperated that I’m not incorporating the meta-logical beliefs into the formal system, but this is because in practice meta-logical beliefs are entirely implicit, and do not appear in the reasoning system used by agents.
The thing I’m exasperated by is, rather, that I don’t understand what you are doing with the meta-logical beliefs if you aren’t including them in the formal system. It’s fine if you don’t include them in the formal system; just tell me what you are doing instead! This was the point of my “I have the semantic map here in my back pocket” argument: fine, I’m willing to grant that the agent ‘has’ these meta-logical beliefs, I just don’t yet understand how you propose the agent use them.
I mean, I’m particularly exasperated because you explicitly state that the meta-logical beliefs don’t change the agent’s reasoning at all; it seems like you’re boldly asserting that they are just a talisman which the agent keeps in its back pocket, and that this somehow solves everything.
in practice meta-logical beliefs are entirely implicit, and do not appear in the reasoning system used by agents.
In the new terminology I am proposing, I think perhaps what you are saying is that the meta-logical stuff is aliefs and thus not apparent in the beliefs of the system. What do you think of that interpretation?
(Obviously, I don’t think your proposal solves the Lobstacle in that case, but, that is a separate question.)
If I build a chess-playing robot, its program will not explicitly include the assumption that the rules of chess it carries are the correct ones,
Right. To me this overtly reads as “a chess playing robot only alieves the rules of chess. It has no explicit endorsement of those rules.” Which makes perfect sense to me.
, nor will it use such assumptions in determining its moves, because such determinations are made without any reference to a semantic map.
But then, this part of the sentence seems to go completely off the rails for me; a chess-playing robot will be no good at all if the rules of chess don’t bear on its moves. Can you clarify?
This is why I said the agent doesn’t change its reasoning.
I still don’t understand this part at all; could you go into more depth?
The metalogical beliefs thus are only relevant when an agent applies its (completed) reasoning to its environment via the semantic map.
This helps clarify a bit; it sounds like maybe we were conflating different notions of “reasoning”. IE, I interpreted you as saying the semantic map does not enter into the agent’s algorithm anywhere, not in the logical deduction system nor in the reasoning which the agent uses to decide on actions based on those logical deductions; whereas you were saying the semantic map does not enter into the agent’s logical deductions, but rather, has to do with how those deductions are used to make decisions.
But I am still confused by your proposal:
We can formalize that situation via the extended logic L’ if you like, in which case this is probably the answer that you keep demanding:
(It seems worth clarifying that I’m only demanding that the meta-logical reasoning be formalized for us, ie that you give a formal statement of the agent design which I can understand, not formalized for the agents, ie put into their formal system)
Both A and B “reason” in L’ (B could even work in a distinct extension of L), but will only accept proofs in the fragment L. Since the axioms in L’ extending L are identifiable by their reference to the semantic mapping, there is no risk of “belief contamination” in proofs, if that were ever a concern.
Lob’s theorem says that the conclusions X where L can believe its own reasoning to be sound are precisely the cases where L can prove X, that is, □(□X→X)→□X. So normally, L’ can accept proofs in L’ just fine, if they are concretely given. The lobstacle has to do with a logic trusting itself in the abstract, that is, trusting proofs before you see them. (Hence, the lobstacle doesn’t block an agent from trusting its future self if it can concretely simulate what its future self can do, because there will be no specific reasoning step which it will reject; what the lobstacle blocks is for an agent to trust its future self with unforseen chains of reasoning.)
So, one interpretation: you propose to modify this situation, by restricting L’ to only accept proofs given in L.
This interpretation seems to conform to my “back pocket” argument. Both A and B “reason” in L’, but really, only accept L. (This explains why you said ‘”reason”’ in scare quotes.) But, I’m left wondering where/how L’ matters here, and how this proposal differs from just building naive logical agents who use L (and fall prey to the lobstacle).
Thus, I’m probably better off interpreting you as referring to “accepting proofs” in the abstract, rather than concretely given proofs. With this interpretation, it seems you mean to say that A and B alieve L’ (that is, they use L’ internally), but only explicitly endorse proofs in L (that is, they can only accept principles of reasoning which warrant L-proofs, not L’-proofs, when they abstractly consider which proofs are normative).
But then, your bolded statement seems to just be a re-statement of the Lobstacle: logical agents can’t explicitly endorse their own logic L’ which they use to reason, but rather, can only generally accept reasoning in some weaker fragment L.
Without an intended semantics, what the probabilities assigned to formulas can only be interpreted as beliefs/levels of certainty about provability of statements from axioms (which it also believes with more or less certainty). This is great, but as soon as you want your logical inductor to reason about a particular mathematical object, the only way to turn those beliefs about provability into beliefs about truth in the model, you need to extend the inductor (explicitly or implicitly) with meta-logical beliefs about the soundness of that map, since it will update its beliefs based on provability even if its proof methods aren’t sound.
This part doesn’t seem totally relevant any more, but to respond: sure, but the standard model is an infinite object, so we don’t really know how to extend the inductor to (implicitly or explicitly) know the intended semantic map. (Although this is a subject of some interest for me.) It’s plausible that there’s no way. But then, it also becomes plausible that humans don’t do this (ie don’t actually possess a full semantic map for peano arithmetic).
Instead, I’ve come to think about us (like logical inductors) as being uncertain about the model (ie uncertain whether numbers with specific properties exist, rather than possessing any tool which would fully differentiate between standard and non-standard numbers).
As such, I feel you’ve misunderstood me here. I don’t want semantics-independent reasoning at all, if anything the opposite: reasoning that prioritises verifying soundness of a logic wrt specified semantic maps in an empirical way, and which can adapt its reasoning system when soundness is shown to fail.
Your critique of logical induction in the post was “fixed semantics are inflexible”. But now it seems like you are the one who proposes to have a fixed semantics (carrying a specific semantic map, eg, the standard model), and modifying the logic when that semantic map shows the logic to be unsound. In contrast, logical induction is the one who proposes to have no fixed semantic map (instead being uncertain about the model), and modifying those beliefs based on what the logic proves.
My critique of this is only that I don’t know how to “have the standard model”. In general, you propose that the agent has a semantic map which can be used to check the soundness of the logic. But I am skeptical: a semantic map will usually refer to things we cannot check (EG the external world, or uncomputable facts about numbers). Don’t get me wrong: I would love to be able to check those things more properly. It’s just that I don’t see a way (beyond what is already possible with logical reasoning, or more haphazardly but more powerfully, with the probabilistic extension of logical reasoning that logical induction gives us).
(And I also don’t yet see what that part has to do with getting around the Lobstacle.)
I like the alief/belief distinction, this seems to carry the distinction I was after. To make it more formal, I’ll use “belief” to refer to ‘things which an agent can prove in its reasoning engine/language (L)‘, and “alief” to refer to beliefs plus ‘additional assumptions which the agent makes about the bearing of that reasoning on the environment’, which together constitute a larger logic (L’). Does that match the distinction you intended between these terms?
An immediate pedagogical problem with this terminology is that we have to be careful not to conflate this notion of belief with the usual one: an agent will still be able to prove things in L even if it doesn’t believe (in the conventional sense) that the L-proof involved is valid.
There is a more serious formalization issue at play, though, which is the problem of expressing a negative alief. How does one express that an agent “does not alieve that a proof of X in L implies that X is true”? ¬(□X→X) is classically equivalent to □X∧¬X, which in particular is an assertion of both the existence of a proof of X and the falsehood of X, which is clearly far stronger than the intended claim. This is going off on a tangent, so for now I will just assume that it is possible to express disaliefs by introducing some extra operators in L’ and get on with it.
So, to be absolutely clear on this: do you accept the mathematical proofs in the original paper (but propose some way around them), or do you think they are actually mistaken? Do you accept the proof of Lob’s theorem itself, or do you think it is mistaken?
Yes. The mathematical proofs and Löb’s theorem are absolutely fine. What I’m refuting is their relevance; specifically the validity of this claim:
An agent can only trust another agent if it believes that agent’s aliefs.
My position is that *when their beliefs are sound* an agent only ever needs to *alieve* another agents *beliefs* in order to trust them. A definition of trust which fails to be reflexive is clearly a bad definition, and with this modified definition there is no obstacle because “beliefs being strictly weaker than aliefs” is the default (indeed, by Löb’s theorem, the only reasonable possibility), and can be implemented symmetrically between multiple agents; no heirarchy of logics or other such solution is needed.
Note that following the construction in the article, the secondary agent B can only act on the basis of a valid L-proof, so there is no need to distinguish between trusting what B says (the L-proofs B produces) and what B does (their subsequent action upon producing an L-proof). Attaining this guarantee in practice, so as to be able to trust that B will do what they have promised to do, is a separate but important problem. In general, the above notion of trust will only apply to what another agent says, or more precisely to the proofs they produce.
> So if A constructs B to produce proofs in L, it doesn’t matter what B’s beliefs are, or even if B has any beliefs;
But using proofs in L is precisely what I understood from “belief”; so, if you have something else in mind, I will need clarification.
In the language you introduce, and bearing in mind what I said above, this would be restated as “it doesn’t matter what B’s aliefs are”. I can use this to illustrate why I needed to include the condition “when their beliefs are sound” in the above: suppose A and B have have differing/imperfect knowledge about the state of the environment, to the effect that B may disalieve the soundness of L, while A alieves it. The result is that B might alieve they are misleading A by communicating an L-proof which B alieves to be invalid. But if A’s application of L is in fact sound (so B is in the wrong) then A can still trust and successfully apply the L-proof supplied by B.
> …nor will it use such assumptions in determining its moves, because such determinations are made without any reference to a semantic map.
But then, this part of the sentence seems to go completely off the rails for me; a chess-playing robot will be no good at all if the rules of chess don’t bear on its moves. Can you clarify?
You’re right, this part was a mistake. Such a robot will optimize play with respect to what it alieves are the rules, and so will become very good at what it implicitly alieves chess to be.
> This is why I said the agent doesn’t change its reasoning.
I still don’t understand this part at all; could you go into more depth?
I was taking “reasoning” here to mean “applying the logic L” (so manipulating statements of belief), since any assumptions lying strictly in L’ are only applied passively. It feels strange to me to extend “reasoning” to include this implicit stuff, even if we are including it in our formal model of the agent’s behaviour.
But then, your bolded statement seems to just be a re-statement of the Löbstacle: logical agents can’t explicitly endorse their own logic L’ which they use to reason, but rather, can only generally accept reasoning in some weaker fragment L.
It’s certainly a restatement of Löb’s theorem. My assertion is that there is no resultant obstacle.
Re the rest,
(And I also don’t yet see what that part has to do with getting around the Löbstacle.)
It’s not relevant to getting around the Löbstacle; this part of the discussion was the result of me proposing a possible advantage of the perspective shift which (I believe, but have yet to fully convince you) resolves the Löbstacle. I agree that this part is distracting, but it’s also interesting, so please direct message me (via whatever means is available on LW, or by finding me on the MIRIx Discord server or AI alignment Slack) if you have time to discuss it some more.
I like the alief/belief distinction, this seems to carry the distinction I was after. To make it more formal, I’ll use “belief” to refer to ‘things which an agent can prove in its reasoning engine/language (L)‘, and “alief” to refer to beliefs plus ‘additional assumptions which the agent makes about the bearing of that reasoning on the environment’, which together constitute a larger logic (L’). Does that match the distinction you intended between these terms?
Unfortunately, this seems almost opposite to the way I was defining the terminology. I had it that the aliefs are precisely what is proven by the formal system, and the beliefs are what the agent would explicitly endorse if asked. Aliefs are what you feel in your bones. So if the “bones” of the agent are the formal system, that’s the aliefs.
Note also that your definition implies that if an agent alieves something, it must also believe it. In contrast, part of the point for me is that an agent can alieve things without believing them. I would also allow the opposite, for humans and other probabilistic reasoners, though for pure-logic agents this would have to correspond to unsoundness. But pure-logical agents have to have the freedom to alieve without believing, on pain of inconsistency, even if we can’t model belief-without-alief in pure logic.
I find it interesting that you (seemingly) nodded along with my descriptions, but then proposed a definition which was almost opposite mine! I think there’s probably a deep reason for that (having to do with how difficult it is to reliably distinguish alief/belief), but I’m not grasping it for now. It is a symptom of my confusion in this regard that I’m not even sure we’re pointing to different notions of belief/alief even though your definition sounds almost opposite to me. It is well within the realm of possibility that we mean the same thing, and are just choosing very different ways to talk about it.
Specifically, your definition seems fine if L is not the formal language which the agent is hard-wired with, but rather, some logic which the agent explicitly endorses (like the relationship that we have with Peano Arithmetic). Then, yeah, “belief” is about provability in L, while “alief” implies that the agent has some “additional assumptions about the bearing of that reasoning on the environment”. Totally! But then, this suggests that those additional assumptions are somehow represented in some other subsystem of the agent (outside of L). The logic of that other subsystem is what I’m interested in. If that other subsystem uses L’, then it makes sense that the agent explicitly believes L. But now the aliefs of the agent are represented by L’. That is: L’ is the logic within the agent’s bones. So it’s L’ that I’m talking about when I define “aliefs” as the axiomatic system, and “beliefs” as more complicated (opposite to your definition).
Over this discussion, a possible interpretation of what you’re saying that’s been in the back of my mind has been that you think agents should not rely on formal logic in their bones, but rather, should use formal logic only as part of their explicit thinking IE a form of thinking which other, “more basic” reasoning systems use as a tool (a tool which they can choose to endorse or not). For example, you might believe that an RL system decides whether to employ logical reasoning. Or deep learning. Etc. In this case, you might say that there is no L’ to find (no logical system represents the aliefs).
To be clear, I do think this is a kind of legitimate response to the Lobstacle: the response of rejecting logic (as a tool for understanding what’s going on in an agent’s “bones” IE their basic decision architecture). This approach says: “Look what happens when you try to make the agent overly reliant on logic! Don’t do that!”
However, the Lobstacle is specifically about using logic to describe or design decision-making procedures. So, this ‘solution’ will not be very satisfying for people trying to do that. The puzzling nature of the Lobstacle remains: the claim is that RL (or something) has to basically solve the problem; we can’t use logic. But why is this? Is it because agents have to “be irrational” at some level (ie, their basic systems can’t conform to the normative content of logic)?
Anyway, this may or may not resemble your view. You haven’t explicitly come out and said anything like that, although it does seem like you think there should be a level beyond logic in some sense.
An immediate pedagogical problem with this terminology is that we have to be careful not to conflate this notion of belief with the usual one: an agent will still be able to prove things in L even if it doesn’t believe (in the conventional sense) that the L-proof involved is valid.
It seems like you think this property is so important that it’s almost definitional, and so, a notion of belief which doesn’t satisfy it is in conflict with the usual notion of belief. I just don’t have this intuition. My notion of belief-in-contrast-to-alief does contrast with the informal notion, but I would emphasize other differences:
“belief” contrasts with the intuitive notion of belief in that it much less implies that you’ll act on a belief; our intuitive notion more often predicts that you’ll act on something if you really believe it.
“alief” contrasts with the intuitive notion of belief in that it much less implies that you’ll explicitly endorse something, or even be able to articulate it in language at all.
In other words, I see the intuitive notion of belief as really consisting of two parts, belief and alief, which are intuitively assumed to go together but which we are splitting apart here.
The property you mention is derived from this conflation, because in fact we need to alieve a reasoning process in order to believe its outputs; so if we’re conflating alief and belief, then it seems like we need to believe that L-proofs are valid in order to see L-proofs and (as a direct result) come to believe what’s been proved.
But this is precisely what’s at stake, in making the belief/alief distinction: we want to point out that this isn’t a healthy relationship to have with logic (indeed, Godel shows how it leads to inconsistency).
There is a more serious formalization issue at play, though, which is the problem of expressing a negative alief. How does one express that an agent “does not alieve that a proof of X in L implies that X is true”? ¬(□X→X) is classically equivalent to □X∧¬X, which in particular is an assertion of both the existence of a proof of X and the falsehood of X, which is clearly far stronger than the intended claim. This is going off on a tangent, so for now I will just assume that it is possible to express disaliefs by introducing some extra operators in L’ and get on with it.
I like that you pointed this out, but yeah, it doesn’t seem especially important to our discussion. In any case, I would define disalief as something like this:
The agent’s mental architecture lacks a deduction rule accepting proofs in L, or anything tantamount to such a rule.
Note that the agent might also disbelieve in such a rule, IE, might expect some such proofs to have false conclusions. But this is, of course, not necessary. In particular it would not be true in the case of logics which the agent explicitly endorses (and therefore must not alieve).
Yes. The mathematical proofs and Löb’s theorem are absolutely fine. What I’m refuting is their relevance; specifically the validity of this claim:
An agent can only trust another agent if it believes that agent’s aliefs.
My position is that *when their beliefs are sound* an agent only ever needs to *alieve* another agents *beliefs* in order to trust them.
Hrm. I suspect language has failed us, and we need to make some more distinctions (but I am not sure what they are).
In my terms, if A alieves B’s beliefs, then (for example) if B explicitly endorses ZFC, then A must be using ZFC “in its bones”. But if B explicitly endorses ZFC, then the logic which B is using must be more powerful than that. So A might be logically weaker than B (if A only alieves ZFC, and not the stronger system which B used to decide that ZFC is sound). If so, A cannot trust B (A does not alieve that B’s reasoning is sound, that is, A does not believe B).
I have to confess that I’m confusing myself a bit, and am tempted to give yet another (different, incompatible) definition for the alief/belief split. I’ll hold off for now, but I hope it’s very clear that I’m not accusing all confusion about this as coming from you—I’m aiming to minimize confusion, but I still worry that I’ve introduced contradictory ideas in this conversation. (I’m actually tempted to start distinguishing 3 levels rather than 2! Alief/belief are relative terms, and I worry we’re actually conflating important subtleties by using only 2 terms rather than having multple levels...)
A definition of trust which fails to be reflexive is clearly a bad definition, and with this modified definition there is no obstacle
This goes back to the idea that you seem to think “belief in X implies belief in the processes whereby you came to believe in X” is so important as to be definitional, where I think this property has to be a by-product of other things.
In my understanding, the definition of “trust” should not explicitly allow or disallow this, if we’re going to be true to what “trust” means. Rather, for the Lobstacle, “A trusts B” has to be defined as “A willingly relies on B to perform mission-critical tasks”. This definition does indeed fail to be true for naive logical agents. But this should be an argument against naive logical agents, not our notion of trust.
Hence my perception that you do indeed have to question the theorems themselves, in order to dispute their “relevance” to the situation. The definition of trust seems fixed in place to me; indeed, I would instead have to question the relevance of your alternative definition, since what I actually want is the thing studied in the paper (IE being able to delegate critical tasks to another agent).
Note that following the construction in the article, the secondary agent B can only act on the basis of a valid L-proof, so there is no need to distinguish between trusting what B says (the L-proofs B produces) and what B does (their subsequent action upon producing an L-proof).
Ok, but if agent B can only act on valid L-proofs, it seems like agent B has been given a frontal lobotomy (IE this is just the “make sure my future self is dumber” style of solution to the problem).
Or, on the other hand, if the agent A also respects this same restriction, then A cannot delegate tasks to B (because A can’t prove that it’s OK to do so, at least not in L, the logic which it has been restricted to use when it comes to deciding how to act).
Which puts us back in the same lobstacle.
Attaining this guarantee in practice, so as to be able to trust that B will do what they have promised to do, is a separate but important problem. In general, the above notion of trust will only apply to what another agent says, or more precisely to the proofs they produce.
Is this a crux for you? My thinking is that this is going to be a deadly sticking point. It seems like you’re admitting that your approach has this problem, but, you think there’s value in what you’ve done so far because you’ve solved one part of the problem and you think this other part could also work with time. Is that what you’re intending to say? Whereas to me, it looks like this other part is just doomed to fail, so I don’t see what the value in your proposal could be.
For me, solving the Lobstacle means being able to actually decide to delegate.
I was taking “reasoning” here to mean “applying the logic L” (so manipulating statements of belief), since any assumptions lying strictly in L’ are only applied passively. It feels strange to me to extend “reasoning” to include this implicit stuff, even if we are including it in our formal model of the agent’s behaviour.
I think I get what you’re saying here. But if the assumptions lying strictly in L’ are only applied passively, how does it help us? I’m thinking your current answer is (as you’ve already said) “trusting that B will do what they’ve said they’ll do is a separate problem”—IE you aren’t even trying to build the full bridge between B thinking something is a good idea and A trusting B with such tasks.
Both A and B “reason” in L’ (B could even work in a distinct extension of L), but will only accept proofs in the fragment L.
[...]
But then, your bolded statement seems to just be a re-statement of the Löbstacle: logical agents can’t explicitly endorse their own logic L’ which they use to reason, but rather, can only generally accept reasoning in some weaker fragment L.
It’s certainly a restatement of Löb’s theorem. My assertion is that there is no resultant obstacle.
I still really, really don’t get why your language is stuff like “there’s no resultant obstacle” and “what I’m refuting is their relevance”. Your implication is “there was not a problem to begin with” rather than “I have solved the problem”. I asked whether you objected to details of the math in the original paper, and you said no—so apparently you would agree with the result that naive logical agents fail to trust their future self (which is the lobstacle!). Solving the lobstacle would presumably involve providing an improved agent design which would avoid the problem. Yet this seems like it’s not what you want to do—instead you claim something else, along the lines of claiming that there’s not actually a problem?
So, basically, what do you claim to accomplish? I suspect I’m still really misunderstanding that part of it.
Re the rest,
(And I also don’t yet see what that part has to do with getting around the Löbstacle.)
It’s not relevant to getting around the Löbstacle; this part of the discussion was the result of me proposing a possible advantage of the perspective shift which (I believe, but have yet to fully convince you) resolves the Löbstacle. I agree that this part is distracting, but it’s also interesting, so please direct message me (via whatever means is available on LW, or by finding me on the MIRIx Discord server or AI alignment Slack) if you have time to discuss it some more.
Since you’re now identifying it as another part of the perspective shift which you’re trying to communicate (rather than just some technical distraction), it sounds like it might actually be pretty helpful toward me understanding what you’re trying to get at. But, there are already a lot of points floating around in this conversation, so maybe I’ll let it drop.
I’m somewhat curious if you think you’ve communicated your perspective shift to any other person; so far, I’m like “there just doesn’t seem to be anything real here”, but maybe there are other people who get what you’re trying to say?
Note also that your definition implies that if an agent alieves something, it must also believe it.
I find it interesting that you (seemingly) nodded along with my descriptions, but then proposed a definition which was almost opposite mine!
I don’t know how you so misread what I said; I explicitly wrote that aliefs constitute the larger logic, so that beliefs are contained in aliefs (which I’m pretty sure is what you were going for!) and not vice versa. Maybe you got confused because I put beliefs first in this description, or because I described the smaller of the two logics as the “reasoning engine” (for the reason I subsequently provided)? What you said almost convinced me that our definitions actually align, until I reached the point where you said that that beliefs could be “more complicated” than aliefs, which made me unsure.
Anyway, since you keep taking the time to thoroughly reply in good faith, I’ll do my best to clarify and address some of the rest of what you’ve said. However, thanks to the discussion we’ve had so far, a more formal presentation of my ideas is crystallizing in my mind; I prefer to save that for another proper post, since I anticipate it will involve rejigging the terminology again, and I don’t want to muddy the waters further!
Rather, for the Lobstacle, “A trusts B” has to be defined as “A willingly relies on B to perform mission-critical tasks”. This definition does indeed fail to be true for naive logical agents. But this should be an argument against naive logical agents, not our notion of trust.
Hence my perception that you do indeed have to question the theorems themselves, in order to dispute their “relevance” to the situation. The definition of trust seems fixed in place to me; indeed, I would instead have to question the relevance of your alternative definition, since what I actually want is the thing studied in the paper (IE being able to delegate critical tasks to another agent).
Perhaps we have different intuitive notions of trust, since I certainly trust myself (to perform “mission-critical tasks”), at least as far as my own logical reasoning is concerned, and an agent that doesn’t trust itself is going to waste a lot of time second-guessing its own actions. So I don’t think you’ve addressed my argument that the definition of trust that leads to the Löbstacle is faulty because it fails to be reflexive.
Attaining this guarantee in practice, so as to be able to trust that B will do what they have promised to do, is a separate but important problem. In general, the above notion of trust will only apply to what another agent says, or more precisely to the proofs they produce.
Is this a crux for you? My thinking is that this is going to be a deadly sticking point. It seems like you’re admitting that your approach has this problem, but, you think there’s value in what you’ve done so far because you’ve solved one part of the problem and you think this other part could also work with time. Is that what you’re intending to say? Whereas to me, it looks like this other part is just doomed to fail, so I don’t see what the value in your proposal could be. For me, solving the Lobstacle means being able to actually decide to delegate.
There are two separate issues here, and this response makes it apparent that you are conflating them. The fact that the second agent in the original Löbstacle paper is constrained to act only once it has produced a provably effective strategy and is constrained to follow that strategy means that the Löbstacle only applies to questions concerning the (formal) reasoning of a subordinate agent. Whether or not I manage to convince you that the Löbstacle doesn’t exist (because it’s founded on an untenable definition of trust), you have to acknowledge that the argument as presented there doesn’t address the following second problem. Suppose I can guarantee that my subordinate uses reasoning that I believe to be valid. How can I guarantee that it will act on that reasoning in a way I approve of? This is (obviously) a rather general version of the alignment problem. If you’re claiming that Löb’s theorem has a bearing on this, then that would be big news, especially if it vindicates your opinion that it is “doomed to fail”.
The reason I see my post as progress is that currently the Löbstacle is blocking serious research in using simple systems of formal agents to investigate such important problems as the alignment problem.
Your implication is “there was not a problem to begin with” rather than “I have solved the problem”. I asked whether you objected to details of the math in the original paper, and you said no—so apparently you would agree with the result that naive logical agents fail to trust their future self (which is the lobstacle!).
Taking the revised definition of trust I described, that last sentence is no longer the content of any formal mathematical result in that paper, so I do not agree with it, and I stand by what I said.
Indeed, my claim boils down to saying that there is no problem. But I don’t see why that doesn’t constitute a solution to the apparent problem. It’s like the Missing Dollar Riddle; explaining why there’s no problem is the solution.
I’m somewhat curious if you think you’ve communicated your perspective shift to any other person; so far, I’m like “there just doesn’t seem to be anything real here”, but maybe there are other people who get what you’re trying to say?
There’s no real way for me to know. Everyone who I’ve spoken to about this in person has gotten it, but that only amounts to a handful of people. It’s hard to find an audience; I hoped LW would supply one, but so far it seems not. Hopefully a more formal presentation will improve the situation.
Anyway, since you keep taking the time to thoroughly reply in good faith, I’ll do my best to clarify and address some of the rest of what you’ve said. However, thanks to the discussion we’ve had so far, a more formal presentation of my ideas is crystallizing in my mind; I prefer to save that for another proper post, since I anticipate it will involve rejigging the terminology again, and I don’t want to muddy the waters further!
Looks like I forgot about this discussion! Did you post a more formal treatment?
I don’t know how you so misread what I said; I explicitly wrote that aliefs constitute the larger logic, so that beliefs are contained in aliefs (which I’m pretty sure is what you were going for!) and not vice versa. Maybe you got confused because I put beliefs first in this description, or because I described the smaller of the two logics as the “reasoning engine” (for the reason I subsequently provided)? What you said almost convinced me that our definitions actually align, until I reached the point where you said that that beliefs could be “more complicated” than aliefs, which made me unsure.
Sorry for the confusion here! I haven’t re-oriented myself to the whole context, but it sounds like I did invent a big disagreement that didn’t exist. This has to do with my continued confusion about your approach. But in retrospect I do think your early accusation that I was insisting on some rigid assumptions holds water; I needed to go a bit further afield to try and interpret what you were getting at.
Whether or not I manage to convince you that the Löbstacle doesn’t exist (because it’s founded on an untenable definition of trust), you have to acknowledge that the argument as presented there doesn’t address the following second problem.
Again, I haven’t yet understood your approach or even re-read the whole conversation here, but it now seems to me that I was doing something wrong and silly by insisting on a definition of trust that forces the Löbstacle. The original paper is careful to only state that Löb naively seems to present an obstacle, not that it really truly does so. It looks to me like I was repeatedly stubborn on this point in an unproductive way.
My problem is that I still don’t understand how you propose for the agent to reason/behave differently than what I’ve described; so, your statement that it does in fact do something different doesn’t help me much, sorry.
The semantic map is defined on L, not L’—sure, this makes some sense? But this just seems to reinforce the idea that our agent can only “understand” the internal logic of agents who restrict themselves to only use L (not any meta-logical beliefs).
Seems like you missed my point that the meta-logical belief could just be “L is sound” rather than “L plus me is sound”. Adding the first as an axiom to L is fine (it results in an L’ which is sound if L was sound), while adding the second as an axiom is very rarely fine (it proves soundness and consistency of the whole system, so the whole system had better be too weak for Godel’s incompleteness theorems to apply).
Does that make sense?
You were talking about the second sort of situation (where adding the meta-logical belief as an axiom would result in an inconsistent system, because it would claim its own soundness); I wanted to point out that we could also be in the first sort of situation (where adding the meta-logical belief would result in a perfectly consistent system, but would only let you trust L, not L’).
To me, this “ought” in the sentence reads as a prediction (basically an abuse of ‘ought’, which is in common usage basically because people make is/ought errors). I would prefer to re-phrase as “if phi is provable in L, then the interpretation of phi will be true” or less ambitiously “will probably be true”.
Is your proposal that “X is true” should be taken as a statement of X’s desirability, instead? Or perhaps X’s normativity? That’s what it means to put it on the “ought” side, to me. If it means something different to you, we need to start over with the question of what the is/ought divide refers to.
I agree that (by Tarski’s undefinability theorem) a logic can’t know its own semantic map (provided it meets the assumptions of that theorem). At least, if we’re on the same page about what a semantic map is.
However, Tarski’s analysis also shows how to build a stronger logic L’ which knows the semantic map for L. So if “move to the other side” means represent via more formal axioms (which is what I take you to mean), you seem to be wrong.
My problem with the general format of this argument is, the other interpretation of Lob’s theorem is still valid even if you re-interpret it. That is: Eliezer et al show that the assumptions of Lob’s theorem apply, and thereby, they conclude a formal result. No amound of re-interpreting the theorem changes that; one might as well suggest that we solve the Lobstacle by forgetting Lob’s theorem.
That is what I meant when I said I don’t get how it helps.
It seems to me like your post is missing a step where you design an alternative agent based on your improved thinking. Probably the alternative agent is supposed to be obvious from what you wrote, but I’m not getting it.
So how do you escape the conclusion from the paper??
Justified, perhaps, but also non-existent, right? You say the agent doesn’t change its reasoning. So the reasoning is exactly the same as the lobstacle agent from the paper. So it doesn’t conclude its own soundness. Right??
I have a couple of possible interpretations of what you might mean here, all of them really poor:
You’re saying that we allow the agent to conclude its own soundness without going through anything involving the semantic map, since it can’t possibly do that. But this seems to just result in an inconsistent agent, by Godel’s second theorem. Probably you don’t mean this.
You’re saying that we don’t change anything about the agent design; but we, as designers, don’t worry about the agent being able to reason about its own semantic map. Here, the question is, how does this help us? We still have the same bad agent designs. Probably this isn’t what you mean either.
Right, so, we seem to be on the same page about what the semantic map basically is and Tarski’s undefinability theorem and such.
But what I need is a sketch of the agent that you claim solves the Lobstacle.
Sure, but logical induction doesn’t know anything about the intended semantics. It doesn’t make a lick of difference to the algorithm whether you believe that PA refers to the standard model. Nor does it feature in the mathematical results.
So I would put it to you that logical induction does a good job of capturing what it means to reason in a semantics-ignorant way. If it also works well as a model of reasoning for semantic-ful things, well, that would seem to be a happy accident. And perhaps it doesn’t: perhaps logical induction is missing an aspect of rationality around “semantics”.
Thus, logical induction would appear to be precisely what you call for at the end of your post: a theory of rationality which reasons in a semantics-independent way.
Aha! I knew I must be missing something, thanks for the clarification. That makes things easier. I’ll continue to use L’ to mean “L + Sound(L,S)”, where S is a particular semantic map.
The Löbian obstacle is about trust in the reasoning performed by a subordinate agent; the promise of subsequent actions taken based on that reasoning are just a pretext for considering that formal problem. So if A constructs B to produce proofs in L, it doesn’t matter what B’s beliefs are, or even if B has any beliefs; B could just be manipulating these as formal expressions. If you insist that B’s beliefs be incorporated into its reasoning, as you seem to want to (more on that below), then I’m saying it doesn’t matter what extension of L the agent B is equipped with; it can even be an inconsistent extension, as long as only valid L-proofs are produced.
The word “normative” sticks out to me as potential common ground here, so I’ll use that language. The specified semantic map determines what is “actually” true, but its content is not a priori knowledge. As such, the only way for A’s reasoning in L to have any practical value is if A works under the (normative) assumption that provability implies/will imply truth under S.
If this sounds farfetched, consider how police dramas employ the normative nature of truth for dramatic effect on a regular basis. A rogue detective uses principles of reasoning that their superiors deem invalid, so that the latter do not expect the detective’s deductions to yield results in reality… Or perhaps the practice of constructive mathematics would be a more comfortable example, where the axiom of choice is rejected in favour of weaker deductive principles. A dedicated constructivist could reasonably make the claim that their chosen fragment of logic determines what “ought” to be true.
A compromise which was suggested to me this past week is to work with a two-level logic. It seems to me disingenuous that “A reasons in L” should mean “actually, A reasons in the stronger logic L’ which incorporates all the axioms it needs to ensure that provability in L implies truth”, as the Tarskian construction suggests. After all, if A attempts to justify that decision to itself, it seems to me to trigger an infinite regress of more and more powerful logics. Identifying and segregating the axioms which refer to the semantic map S as “meta-logical beliefs” is enough to avoid such an existential crisis, just as we only need to employ PA + Sound(PA,N), where N is our favourite model of the natural numbers, to use PA to reason about those natural numbers.
You seem exasperated that I’m not incorporating the meta-logical beliefs into the formal system, but this is because in practice meta-logical beliefs are entirely implicit, and do not appear in the reasoning system used by agents. If I build a chess-playing robot, its program will not explicitly include the assumption that the rules of chess it carries are the correct ones, nor will it use such assumptions in determining its moves, because such determinations are made without any reference to a semantic map. This is why I said the agent doesn’t change its reasoning.
The metalogical beliefs thus are only relevant when an agent applies its (completed) reasoning to its environment via the semantic map. We can formalize that situation via the extended logic L’ if you like, in which case this is probably the answer that you keep demanding:
Both A and B “reason” in L’ (B could even work in a distinct extension of L), but will only accept proofs in the fragment L. Since the axioms in L’ extending L are identifiable by their reference to the semantic mapping, there is no risk of “belief contamination” in proofs, if that were ever a concern.
I expect there is more I should say to justify how this avoids the obstacle, but I will wait for your feedback first.
Without an intended semantics, what the probabilities assigned to formulas can only be interpreted as beliefs/levels of certainty about provability of statements from axioms (which it also believes with more or less certainty). This is great, but as soon as you want your logical inductor to reason about a particular mathematical object, the only way to turn those beliefs about provability into beliefs about truth in the model, you need to extend the inductor (explicitly or implicitly) with meta-logical beliefs about the soundness of that map, since it will update its beliefs based on provability even if its proof methods aren’t sound.
As such, I feel you’ve misunderstood me here. I don’t want semantics-independent reasoning at all, if anything the opposite: reasoning that prioritises verifying soundness of a logic wrt specified semantic maps in an empirical way, and which can adapt its reasoning system when soundness is shown to fail. A logical inductor isn’t equipped with the capacity to work in mere fragments of its logic (it could be modified to do so, but that’s certainly not the main point of this algorithm, as I understand it), so can only go as far as identifying when its reasoning is not sound by observing that it believes a contradiction, without being able to do anything about it besides modifying the beliefs it holds in its axioms indefinitely.
I’m not insisting on anything about the agent design; I simply remain puzzled how your proposal differs from the one in the paper, and so, continue to assume it’s like the one in the paper except those differences which I understand. Your statements have been reading almost like you think you’ve refuted formal arguments in the paper (implying you don’t think the formal agent designs do what I think they do), rather than providing a new agent design which does better. This contributes to my feeling that you are really just wrestling with Lob’s theorem itself. Nor do I recall you saying much to dissuade me of this. In your OP, you use the language “Under the belief that the Löbian Obstacle was a genuine problem to be avoided”, as if the original idea was simply mistaken.
So, to be absolutely clear on this: do you accept the mathematical proofs in the original paper (but propose some way around them), or do you think they are actually mistaken? Do you accept the proof of Lob’s theorem itself, or do you think it is mistaken?
But using proofs in L is precisely what I understood from “belief”; so, if you have something else in mind, I will need clarification.
I think I haven’t understood much of this.
I would argue that the only way for A’s reasoning in L to have practical value is for A to act on such reasoning. The only way for A’s reasoning to have practical value for some other agent B is for B to be working under the assumption that provability-in-L implies truth under S. Indeed, this seems in line with your detective drama example. If the superiors were put in the position of the rogue detective, often they would have come to the same conclusion. Yet, looking at the problem from a removed position, they cannot accept the conclusion. But this is precisely the lobstacle: the condition for reasoning to have value to an agent A is different from the condition for A’s reasoning to have value to another agent B.
Let me therefore make a (not totally formal) distinction based on the alief/belief idea:
The aliefs of a logic-based agent are the axioms/theorems which inform action;
The beliefs of a logic-based agent are the axioms/theorems which the agent explicitly endorses.
This is also a version of the distinction between tacit knowledge (eg knowing how to ride a bike) vs explicit knowledge (eg being able to explain scientifically how bike-riding works). To say that an agent “alieves” a logic L is to say that it tacitly knows how to reason in L.
Roughly, I think you have been talking about beliefs, where I have been talking about aliefs.
Now, a “naive logical agent” (ie the simple agent design which falls prey to the Lobstacle, in the paper) has a few important properties:
Goedel’s incompleteness theorems tells us that aliefs cannot equal beliefs; a logic never explicitly endorses itself, but rather, only explicitly endorses weaker logics.
An agent constructed based on the logic L alieves L, but does not believe L (this is a re-statement of the lobstacle).
An agent can only trust another agent if it believes that agent’s aliefs.
An agent therefore cannot belief its own aliefs. (This is another restatement of the lobstacle.)
These statements are not necessarily true of logical agents in general, of course, since the paper gives some counterexamples (agents who can trust the same logic which they base their actions on). But those counterexamples all have some oddities. I presume your goal is to get rid of those oddities while still avoiding the lobstacle.
The thing I’m exasperated by is, rather, that I don’t understand what you are doing with the meta-logical beliefs if you aren’t including them in the formal system. It’s fine if you don’t include them in the formal system; just tell me what you are doing instead! This was the point of my “I have the semantic map here in my back pocket” argument: fine, I’m willing to grant that the agent ‘has’ these meta-logical beliefs, I just don’t yet understand how you propose the agent use them.
I mean, I’m particularly exasperated because you explicitly state that the meta-logical beliefs don’t change the agent’s reasoning at all; it seems like you’re boldly asserting that they are just a talisman which the agent keeps in its back pocket, and that this somehow solves everything.
In the new terminology I am proposing, I think perhaps what you are saying is that the meta-logical stuff is aliefs and thus not apparent in the beliefs of the system. What do you think of that interpretation?
(Obviously, I don’t think your proposal solves the Lobstacle in that case, but, that is a separate question.)
Right. To me this overtly reads as “a chess playing robot only alieves the rules of chess. It has no explicit endorsement of those rules.” Which makes perfect sense to me.
But then, this part of the sentence seems to go completely off the rails for me; a chess-playing robot will be no good at all if the rules of chess don’t bear on its moves. Can you clarify?
I still don’t understand this part at all; could you go into more depth?
This helps clarify a bit; it sounds like maybe we were conflating different notions of “reasoning”. IE, I interpreted you as saying the semantic map does not enter into the agent’s algorithm anywhere, not in the logical deduction system nor in the reasoning which the agent uses to decide on actions based on those logical deductions; whereas you were saying the semantic map does not enter into the agent’s logical deductions, but rather, has to do with how those deductions are used to make decisions.
But I am still confused by your proposal:
(It seems worth clarifying that I’m only demanding that the meta-logical reasoning be formalized for us, ie that you give a formal statement of the agent design which I can understand, not formalized for the agents, ie put into their formal system)
Lob’s theorem says that the conclusions X where L can believe its own reasoning to be sound are precisely the cases where L can prove X, that is, □(□X→X)→□X. So normally, L’ can accept proofs in L’ just fine, if they are concretely given. The lobstacle has to do with a logic trusting itself in the abstract, that is, trusting proofs before you see them. (Hence, the lobstacle doesn’t block an agent from trusting its future self if it can concretely simulate what its future self can do, because there will be no specific reasoning step which it will reject; what the lobstacle blocks is for an agent to trust its future self with unforseen chains of reasoning.)
So, one interpretation: you propose to modify this situation, by restricting L’ to only accept proofs given in L.
This interpretation seems to conform to my “back pocket” argument. Both A and B “reason” in L’, but really, only accept L. (This explains why you said ‘”reason”’ in scare quotes.) But, I’m left wondering where/how L’ matters here, and how this proposal differs from just building naive logical agents who use L (and fall prey to the lobstacle).
Thus, I’m probably better off interpreting you as referring to “accepting proofs” in the abstract, rather than concretely given proofs. With this interpretation, it seems you mean to say that A and B alieve L’ (that is, they use L’ internally), but only explicitly endorse proofs in L (that is, they can only accept principles of reasoning which warrant L-proofs, not L’-proofs, when they abstractly consider which proofs are normative).
But then, your bolded statement seems to just be a re-statement of the Lobstacle: logical agents can’t explicitly endorse their own logic L’ which they use to reason, but rather, can only generally accept reasoning in some weaker fragment L.
This part doesn’t seem totally relevant any more, but to respond: sure, but the standard model is an infinite object, so we don’t really know how to extend the inductor to (implicitly or explicitly) know the intended semantic map. (Although this is a subject of some interest for me.) It’s plausible that there’s no way. But then, it also becomes plausible that humans don’t do this (ie don’t actually possess a full semantic map for peano arithmetic).
Instead, I’ve come to think about us (like logical inductors) as being uncertain about the model (ie uncertain whether numbers with specific properties exist, rather than possessing any tool which would fully differentiate between standard and non-standard numbers).
Your critique of logical induction in the post was “fixed semantics are inflexible”. But now it seems like you are the one who proposes to have a fixed semantics (carrying a specific semantic map, eg, the standard model), and modifying the logic when that semantic map shows the logic to be unsound. In contrast, logical induction is the one who proposes to have no fixed semantic map (instead being uncertain about the model), and modifying those beliefs based on what the logic proves.
My critique of this is only that I don’t know how to “have the standard model”. In general, you propose that the agent has a semantic map which can be used to check the soundness of the logic. But I am skeptical: a semantic map will usually refer to things we cannot check (EG the external world, or uncomputable facts about numbers). Don’t get me wrong: I would love to be able to check those things more properly. It’s just that I don’t see a way (beyond what is already possible with logical reasoning, or more haphazardly but more powerfully, with the probabilistic extension of logical reasoning that logical induction gives us).
(And I also don’t yet see what that part has to do with getting around the Lobstacle.)
I like the alief/belief distinction, this seems to carry the distinction I was after. To make it more formal, I’ll use “belief” to refer to ‘things which an agent can prove in its reasoning engine/language (L)‘, and “alief” to refer to beliefs plus ‘additional assumptions which the agent makes about the bearing of that reasoning on the environment’, which together constitute a larger logic (L’). Does that match the distinction you intended between these terms?
An immediate pedagogical problem with this terminology is that we have to be careful not to conflate this notion of belief with the usual one: an agent will still be able to prove things in L even if it doesn’t believe (in the conventional sense) that the L-proof involved is valid.
There is a more serious formalization issue at play, though, which is the problem of expressing a negative alief. How does one express that an agent “does not alieve that a proof of X in L implies that X is true”? ¬(□X→X) is classically equivalent to □X∧¬X, which in particular is an assertion of both the existence of a proof of X and the falsehood of X, which is clearly far stronger than the intended claim. This is going off on a tangent, so for now I will just assume that it is possible to express disaliefs by introducing some extra operators in L’ and get on with it.
Yes. The mathematical proofs and Löb’s theorem are absolutely fine. What I’m refuting is their relevance; specifically the validity of this claim:
My position is that *when their beliefs are sound* an agent only ever needs to *alieve* another agents *beliefs* in order to trust them. A definition of trust which fails to be reflexive is clearly a bad definition, and with this modified definition there is no obstacle because “beliefs being strictly weaker than aliefs” is the default (indeed, by Löb’s theorem, the only reasonable possibility), and can be implemented symmetrically between multiple agents; no heirarchy of logics or other such solution is needed.
Note that following the construction in the article, the secondary agent B can only act on the basis of a valid L-proof, so there is no need to distinguish between trusting what B says (the L-proofs B produces) and what B does (their subsequent action upon producing an L-proof). Attaining this guarantee in practice, so as to be able to trust that B will do what they have promised to do, is a separate but important problem. In general, the above notion of trust will only apply to what another agent says, or more precisely to the proofs they produce.
In the language you introduce, and bearing in mind what I said above, this would be restated as “it doesn’t matter what B’s aliefs are”. I can use this to illustrate why I needed to include the condition “when their beliefs are sound” in the above: suppose A and B have have differing/imperfect knowledge about the state of the environment, to the effect that B may disalieve the soundness of L, while A alieves it. The result is that B might alieve they are misleading A by communicating an L-proof which B alieves to be invalid. But if A’s application of L is in fact sound (so B is in the wrong) then A can still trust and successfully apply the L-proof supplied by B.
You’re right, this part was a mistake. Such a robot will optimize play with respect to what it alieves are the rules, and so will become very good at what it implicitly alieves chess to be.
I was taking “reasoning” here to mean “applying the logic L” (so manipulating statements of belief), since any assumptions lying strictly in L’ are only applied passively. It feels strange to me to extend “reasoning” to include this implicit stuff, even if we are including it in our formal model of the agent’s behaviour.
It’s certainly a restatement of Löb’s theorem. My assertion is that there is no resultant obstacle.
Re the rest,
It’s not relevant to getting around the Löbstacle; this part of the discussion was the result of me proposing a possible advantage of the perspective shift which (I believe, but have yet to fully convince you) resolves the Löbstacle. I agree that this part is distracting, but it’s also interesting, so please direct message me (via whatever means is available on LW, or by finding me on the MIRIx Discord server or AI alignment Slack) if you have time to discuss it some more.
Unfortunately, this seems almost opposite to the way I was defining the terminology. I had it that the aliefs are precisely what is proven by the formal system, and the beliefs are what the agent would explicitly endorse if asked. Aliefs are what you feel in your bones. So if the “bones” of the agent are the formal system, that’s the aliefs.
Note also that your definition implies that if an agent alieves something, it must also believe it. In contrast, part of the point for me is that an agent can alieve things without believing them. I would also allow the opposite, for humans and other probabilistic reasoners, though for pure-logic agents this would have to correspond to unsoundness. But pure-logical agents have to have the freedom to alieve without believing, on pain of inconsistency, even if we can’t model belief-without-alief in pure logic.
I find it interesting that you (seemingly) nodded along with my descriptions, but then proposed a definition which was almost opposite mine! I think there’s probably a deep reason for that (having to do with how difficult it is to reliably distinguish alief/belief), but I’m not grasping it for now. It is a symptom of my confusion in this regard that I’m not even sure we’re pointing to different notions of belief/alief even though your definition sounds almost opposite to me. It is well within the realm of possibility that we mean the same thing, and are just choosing very different ways to talk about it.
Specifically, your definition seems fine if L is not the formal language which the agent is hard-wired with, but rather, some logic which the agent explicitly endorses (like the relationship that we have with Peano Arithmetic). Then, yeah, “belief” is about provability in L, while “alief” implies that the agent has some “additional assumptions about the bearing of that reasoning on the environment”. Totally! But then, this suggests that those additional assumptions are somehow represented in some other subsystem of the agent (outside of L). The logic of that other subsystem is what I’m interested in. If that other subsystem uses L’, then it makes sense that the agent explicitly believes L. But now the aliefs of the agent are represented by L’. That is: L’ is the logic within the agent’s bones. So it’s L’ that I’m talking about when I define “aliefs” as the axiomatic system, and “beliefs” as more complicated (opposite to your definition).
Over this discussion, a possible interpretation of what you’re saying that’s been in the back of my mind has been that you think agents should not rely on formal logic in their bones, but rather, should use formal logic only as part of their explicit thinking IE a form of thinking which other, “more basic” reasoning systems use as a tool (a tool which they can choose to endorse or not). For example, you might believe that an RL system decides whether to employ logical reasoning. Or deep learning. Etc. In this case, you might say that there is no L’ to find (no logical system represents the aliefs).
To be clear, I do think this is a kind of legitimate response to the Lobstacle: the response of rejecting logic (as a tool for understanding what’s going on in an agent’s “bones” IE their basic decision architecture). This approach says: “Look what happens when you try to make the agent overly reliant on logic! Don’t do that!”
However, the Lobstacle is specifically about using logic to describe or design decision-making procedures. So, this ‘solution’ will not be very satisfying for people trying to do that. The puzzling nature of the Lobstacle remains: the claim is that RL (or something) has to basically solve the problem; we can’t use logic. But why is this? Is it because agents have to “be irrational” at some level (ie, their basic systems can’t conform to the normative content of logic)?
Anyway, this may or may not resemble your view. You haven’t explicitly come out and said anything like that, although it does seem like you think there should be a level beyond logic in some sense.
It seems like you think this property is so important that it’s almost definitional, and so, a notion of belief which doesn’t satisfy it is in conflict with the usual notion of belief. I just don’t have this intuition. My notion of belief-in-contrast-to-alief does contrast with the informal notion, but I would emphasize other differences:
“belief” contrasts with the intuitive notion of belief in that it much less implies that you’ll act on a belief; our intuitive notion more often predicts that you’ll act on something if you really believe it.
“alief” contrasts with the intuitive notion of belief in that it much less implies that you’ll explicitly endorse something, or even be able to articulate it in language at all.
In other words, I see the intuitive notion of belief as really consisting of two parts, belief and alief, which are intuitively assumed to go together but which we are splitting apart here.
The property you mention is derived from this conflation, because in fact we need to alieve a reasoning process in order to believe its outputs; so if we’re conflating alief and belief, then it seems like we need to believe that L-proofs are valid in order to see L-proofs and (as a direct result) come to believe what’s been proved.
But this is precisely what’s at stake, in making the belief/alief distinction: we want to point out that this isn’t a healthy relationship to have with logic (indeed, Godel shows how it leads to inconsistency).
I like that you pointed this out, but yeah, it doesn’t seem especially important to our discussion. In any case, I would define disalief as something like this:
The agent’s mental architecture lacks a deduction rule accepting proofs in L, or anything tantamount to such a rule.
Note that the agent might also disbelieve in such a rule, IE, might expect some such proofs to have false conclusions. But this is, of course, not necessary. In particular it would not be true in the case of logics which the agent explicitly endorses (and therefore must not alieve).
Hrm. I suspect language has failed us, and we need to make some more distinctions (but I am not sure what they are).
In my terms, if A alieves B’s beliefs, then (for example) if B explicitly endorses ZFC, then A must be using ZFC “in its bones”. But if B explicitly endorses ZFC, then the logic which B is using must be more powerful than that. So A might be logically weaker than B (if A only alieves ZFC, and not the stronger system which B used to decide that ZFC is sound). If so, A cannot trust B (A does not alieve that B’s reasoning is sound, that is, A does not believe B).
I have to confess that I’m confusing myself a bit, and am tempted to give yet another (different, incompatible) definition for the alief/belief split. I’ll hold off for now, but I hope it’s very clear that I’m not accusing all confusion about this as coming from you—I’m aiming to minimize confusion, but I still worry that I’ve introduced contradictory ideas in this conversation. (I’m actually tempted to start distinguishing 3 levels rather than 2! Alief/belief are relative terms, and I worry we’re actually conflating important subtleties by using only 2 terms rather than having multple levels...)
This goes back to the idea that you seem to think “belief in X implies belief in the processes whereby you came to believe in X” is so important as to be definitional, where I think this property has to be a by-product of other things.
In my understanding, the definition of “trust” should not explicitly allow or disallow this, if we’re going to be true to what “trust” means. Rather, for the Lobstacle, “A trusts B” has to be defined as “A willingly relies on B to perform mission-critical tasks”. This definition does indeed fail to be true for naive logical agents. But this should be an argument against naive logical agents, not our notion of trust.
Hence my perception that you do indeed have to question the theorems themselves, in order to dispute their “relevance” to the situation. The definition of trust seems fixed in place to me; indeed, I would instead have to question the relevance of your alternative definition, since what I actually want is the thing studied in the paper (IE being able to delegate critical tasks to another agent).
Ok, but if agent B can only act on valid L-proofs, it seems like agent B has been given a frontal lobotomy (IE this is just the “make sure my future self is dumber” style of solution to the problem).
Or, on the other hand, if the agent A also respects this same restriction, then A cannot delegate tasks to B (because A can’t prove that it’s OK to do so, at least not in L, the logic which it has been restricted to use when it comes to deciding how to act).
Which puts us back in the same lobstacle.
Is this a crux for you? My thinking is that this is going to be a deadly sticking point. It seems like you’re admitting that your approach has this problem, but, you think there’s value in what you’ve done so far because you’ve solved one part of the problem and you think this other part could also work with time. Is that what you’re intending to say? Whereas to me, it looks like this other part is just doomed to fail, so I don’t see what the value in your proposal could be.
For me, solving the Lobstacle means being able to actually decide to delegate.
I think I get what you’re saying here. But if the assumptions lying strictly in L’ are only applied passively, how does it help us? I’m thinking your current answer is (as you’ve already said) “trusting that B will do what they’ve said they’ll do is a separate problem”—IE you aren’t even trying to build the full bridge between B thinking something is a good idea and A trusting B with such tasks.
I still really, really don’t get why your language is stuff like “there’s no resultant obstacle” and “what I’m refuting is their relevance”. Your implication is “there was not a problem to begin with” rather than “I have solved the problem”. I asked whether you objected to details of the math in the original paper, and you said no—so apparently you would agree with the result that naive logical agents fail to trust their future self (which is the lobstacle!). Solving the lobstacle would presumably involve providing an improved agent design which would avoid the problem. Yet this seems like it’s not what you want to do—instead you claim something else, along the lines of claiming that there’s not actually a problem?
So, basically, what do you claim to accomplish? I suspect I’m still really misunderstanding that part of it.
Since you’re now identifying it as another part of the perspective shift which you’re trying to communicate (rather than just some technical distraction), it sounds like it might actually be pretty helpful toward me understanding what you’re trying to get at. But, there are already a lot of points floating around in this conversation, so maybe I’ll let it drop.
I’m somewhat curious if you think you’ve communicated your perspective shift to any other person; so far, I’m like “there just doesn’t seem to be anything real here”, but maybe there are other people who get what you’re trying to say?
I don’t know how you so misread what I said; I explicitly wrote that aliefs constitute the larger logic, so that beliefs are contained in aliefs (which I’m pretty sure is what you were going for!) and not vice versa. Maybe you got confused because I put beliefs first in this description, or because I described the smaller of the two logics as the “reasoning engine” (for the reason I subsequently provided)? What you said almost convinced me that our definitions actually align, until I reached the point where you said that that beliefs could be “more complicated” than aliefs, which made me unsure.
Anyway, since you keep taking the time to thoroughly reply in good faith, I’ll do my best to clarify and address some of the rest of what you’ve said. However, thanks to the discussion we’ve had so far, a more formal presentation of my ideas is crystallizing in my mind; I prefer to save that for another proper post, since I anticipate it will involve rejigging the terminology again, and I don’t want to muddy the waters further!
Perhaps we have different intuitive notions of trust, since I certainly trust myself (to perform “mission-critical tasks”), at least as far as my own logical reasoning is concerned, and an agent that doesn’t trust itself is going to waste a lot of time second-guessing its own actions. So I don’t think you’ve addressed my argument that the definition of trust that leads to the Löbstacle is faulty because it fails to be reflexive.
There are two separate issues here, and this response makes it apparent that you are conflating them. The fact that the second agent in the original Löbstacle paper is constrained to act only once it has produced a provably effective strategy and is constrained to follow that strategy means that the Löbstacle only applies to questions concerning the (formal) reasoning of a subordinate agent. Whether or not I manage to convince you that the Löbstacle doesn’t exist (because it’s founded on an untenable definition of trust), you have to acknowledge that the argument as presented there doesn’t address the following second problem. Suppose I can guarantee that my subordinate uses reasoning that I believe to be valid. How can I guarantee that it will act on that reasoning in a way I approve of? This is (obviously) a rather general version of the alignment problem. If you’re claiming that Löb’s theorem has a bearing on this, then that would be big news, especially if it vindicates your opinion that it is “doomed to fail”.
The reason I see my post as progress is that currently the Löbstacle is blocking serious research in using simple systems of formal agents to investigate such important problems as the alignment problem.
Taking the revised definition of trust I described, that last sentence is no longer the content of any formal mathematical result in that paper, so I do not agree with it, and I stand by what I said.
Indeed, my claim boils down to saying that there is no problem. But I don’t see why that doesn’t constitute a solution to the apparent problem. It’s like the Missing Dollar Riddle; explaining why there’s no problem is the solution.
There’s no real way for me to know. Everyone who I’ve spoken to about this in person has gotten it, but that only amounts to a handful of people. It’s hard to find an audience; I hoped LW would supply one, but so far it seems not. Hopefully a more formal presentation will improve the situation.
Looks like I forgot about this discussion! Did you post a more formal treatment?
Sorry for the confusion here! I haven’t re-oriented myself to the whole context, but it sounds like I did invent a big disagreement that didn’t exist. This has to do with my continued confusion about your approach. But in retrospect I do think your early accusation that I was insisting on some rigid assumptions holds water; I needed to go a bit further afield to try and interpret what you were getting at.
Again, I haven’t yet understood your approach or even re-read the whole conversation here, but it now seems to me that I was doing something wrong and silly by insisting on a definition of trust that forces the Löbstacle. The original paper is careful to only state that Löb naively seems to present an obstacle, not that it really truly does so. It looks to me like I was repeatedly stubborn on this point in an unproductive way.