Also, an infinite sequence of Con(...) statements can be included in the theory, it’s not something requiring a new construction...
An interesting question suggested by the post is what true statements about itself can an agent produce in that setting, assuming it can control which statements to withhold (for how long or under what conditions), even if it knows them to be true.
(There seems to be a sense in which an agent builds the axioms of the formal system that it has access to by making decisions and observations. That is, we can reason about the agent in a fixed system, but the system that the agent itself knows is revealed to it only gradually, depending on what the agent decides and observes at each step, based on the formal system it has at the moment. In this sense, in some cases the agent won’t be withholding statements despite knowing them to be true, it just won’t know them to be true yet (in a stronger sense than not having found consequences of a formal system it has; instead it doesn’t have the formal system that has them as consequences), but will figure them out later.
This view seems to be connected with free will-as-incompleteness demonstrated by the chicken rule: actions are independent of the given formal system, but the agent should be able to learn what the action was after actually performing it, thus extending the original formal system.)
An interesting question suggested by the post is what true statements about itself can an agent produce in that setting, assuming it can control which statements to withhold (for how long or under what conditions), even if it knows them to be true.
Gödel’s theorems apply to effectively generated theories, which means precisely that there is a program printing out all the axioms (or, equivalently, all the provable theorems). So even if an agent is very crafty about this sort of control, it can’t become exempt from Gödel. And I don’t see why it would produce something much stronger than our existing axiomatic systems. So why bother?
To capture some aspects of theory-building and incompleteness associated with decision-making. I agree that all of agent’s activity could just be captured in a stronger system that anticipates all of its decisions from the start, but agent’s own decision-making seems to be modeled best as using weaker theories that can’t predict the next decisions; and after each decision is made, it should become known to plan further.
So the reason why the question is interesting is not because it leads to stronger theories, but because it’s concerned with capturing the effect of decisions on theories involved in making them.
If this approach doesn’t lead to stronger theories, then the game described in Paul’s post doesn’t seem to be strong motivation for studying it. Can you think of some other game where it would be useful?
Sure, not a strong motivation, that’s why I said “question suggested by the post” (we are talking of two different questions now...). The second question seems to be mainly about interpreting agent’s activity, not directly about construction of agents, so I don’t expect a game that clearly requires this kind of analysis. (For example, all agents are “just programs” (perhaps with “just oracles”), so any talk of formal systems used by agents is something in addition, a method of understanding them, even if it results in useful designs.)
On the other hand, if we want the agent to remain ignorant of its own actions, adding axioms that decide the actions to agent’s own theory from the very start is not an option, so describing a procedure for adding them later is a way of keeping both of the requirements: a strong theory and consistency of counterfactuals at each decision.
An interesting question suggested by the post is what true statements about itself can an agent produce in that setting, assuming it can control which statements to withhold (for how long or under what conditions), even if it knows them to be true.
If the agent decides to print any statement at all, that’s probably because it follows from some formal system, right? Then there seems to be no harm in printing all statements that follow from that formal system.
Also, an infinite sequence of Con(...) statements can be included in the theory, it’s not something requiring a new construction...
An interesting question suggested by the post is what true statements about itself can an agent produce in that setting, assuming it can control which statements to withhold (for how long or under what conditions), even if it knows them to be true.
(There seems to be a sense in which an agent builds the axioms of the formal system that it has access to by making decisions and observations. That is, we can reason about the agent in a fixed system, but the system that the agent itself knows is revealed to it only gradually, depending on what the agent decides and observes at each step, based on the formal system it has at the moment. In this sense, in some cases the agent won’t be withholding statements despite knowing them to be true, it just won’t know them to be true yet (in a stronger sense than not having found consequences of a formal system it has; instead it doesn’t have the formal system that has them as consequences), but will figure them out later.
This view seems to be connected with free will-as-incompleteness demonstrated by the chicken rule: actions are independent of the given formal system, but the agent should be able to learn what the action was after actually performing it, thus extending the original formal system.)
Gödel’s theorems apply to effectively generated theories, which means precisely that there is a program printing out all the axioms (or, equivalently, all the provable theorems). So even if an agent is very crafty about this sort of control, it can’t become exempt from Gödel. And I don’t see why it would produce something much stronger than our existing axiomatic systems. So why bother?
To capture some aspects of theory-building and incompleteness associated with decision-making. I agree that all of agent’s activity could just be captured in a stronger system that anticipates all of its decisions from the start, but agent’s own decision-making seems to be modeled best as using weaker theories that can’t predict the next decisions; and after each decision is made, it should become known to plan further.
So the reason why the question is interesting is not because it leads to stronger theories, but because it’s concerned with capturing the effect of decisions on theories involved in making them.
If this approach doesn’t lead to stronger theories, then the game described in Paul’s post doesn’t seem to be strong motivation for studying it. Can you think of some other game where it would be useful?
Sure, not a strong motivation, that’s why I said “question suggested by the post” (we are talking of two different questions now...). The second question seems to be mainly about interpreting agent’s activity, not directly about construction of agents, so I don’t expect a game that clearly requires this kind of analysis. (For example, all agents are “just programs” (perhaps with “just oracles”), so any talk of formal systems used by agents is something in addition, a method of understanding them, even if it results in useful designs.)
On the other hand, if we want the agent to remain ignorant of its own actions, adding axioms that decide the actions to agent’s own theory from the very start is not an option, so describing a procedure for adding them later is a way of keeping both of the requirements: a strong theory and consistency of counterfactuals at each decision.
If the agent decides to print any statement at all, that’s probably because it follows from some formal system, right? Then there seems to be no harm in printing all statements that follow from that formal system.