The new symbols extend the language, while their definitions, obtained from agent and world programs respectively by standard methods of defining recursively enumerable functions, extend the theory.
I haven’t yet read beyond this point, but this is a kind of confusing thing to write. Definitions can’t extend a theory, because they don’t give you new theorems. My assumption is that you will add axioms that incorporate the new symbols, and the axioms will extend the theory.
Definitions can’t extend a theory, because they don’t give you new theorems.
A conservative extension of a language/theory doesn’t introduce new theorems in the old language, but could introduce new theorems that make use of new symbols, although in the case of extension by definitions, all new theorems can also be expressed in the smaller (original) language and would be the theorems of original theory.
This is unlike the situation with A and O, where the agent can’t just perform action A, since it’s not defined in the way the agent knows how to perform (even though A is (provably) equivalent to one of the constants, the agent can’t prove that for any given constant).
It might be clearer to maintain the distinction between a constant symbol c and the element v(c), in the domain of discourse, assigned to c by the interpretation valuation v.
For example, I found the quote above confusing, but I think that you meant “This is unlike the situation with v(A) and v(O), where the agent can’t just perform action v(A), since it’s not defined in the way the agent knows how to perform (even though v(A) is (provably, in the metalogic) equal to the interpretation of one of the constants, the agent can’t prove that for any given constant).”
I think that he means something analogous to the way that we can add some axioms involving the symbol “+” to the Peano axioms, and then show in second-order logic that the new axioms define addition uniquely.
The agent normally won’t even know “explicit values” of actual action and actual outcome. Knowing actual value would break the illusion of consistent consequences: suppose the agent is consistent, knows that A=2, and isn’t out of time yet, then it can prove [A=1 ⇒ O=100000], even if in fact O=1000, use that moral argument to beat any other with worse promised outcome, and decide A=1, contradiction.
This would only happen if the agent had a rule of inference that allowed it to infer from
A=1 ⇒ O=100000
and
all other promised outcomes are worse than 100000
that
A = 1.
But why would the first-order theory use such a rule of inference? You seem to have just given an argument for why we shouldn’t put this rule of inference into the theory.
ETA: I guess that my point leads right to your conclusion, and explains it. The agent is built so that, upon deducing the first two bullet-points, the agent proceeds to do the action assigned to the constant 1 by the interpretation. But the point is that the agent doesn’t bother to infer the third bullet-point; the agent just acts. As a result, it never deduces any formulas of the form [A=X], which is what you were saying.
I haven’t yet read beyond this point, but this is a kind of confusing thing to write. Definitions can’t extend a theory, because they don’t give you new theorems. My assumption is that you will add axioms that incorporate the new symbols, and the axioms will extend the theory.
A conservative extension of a language/theory doesn’t introduce new theorems in the old language, but could introduce new theorems that make use of new symbols, although in the case of extension by definitions, all new theorems can also be expressed in the smaller (original) language and would be the theorems of original theory.
Okay, thanks. I didn’t know that adding certain kinds of axioms was called “extension by definitions”.
It might be clearer to maintain the distinction between a constant symbol c and the element v(c), in the domain of discourse, assigned to c by the interpretation valuation v.
For example, I found the quote above confusing, but I think that you meant “This is unlike the situation with v(A) and v(O), where the agent can’t just perform action v(A), since it’s not defined in the way the agent knows how to perform (even though v(A) is (provably, in the metalogic) equal to the interpretation of one of the constants, the agent can’t prove that for any given constant).”
Some axioms are definitions.
Previous theorem: All unmarried men are not married New definition: “Bachelor” means “unmarried man” New theorem: All bachelors are unmarried men.
I’m pretty sure that’s what he means. Hopefully clarified, if not made perfectly in accord with standard definitions.
I think that he means something analogous to the way that we can add some axioms involving the symbol “+” to the Peano axioms, and then show in second-order logic that the new axioms define addition uniquely.
Still commenting while reading:
This would only happen if the agent had a rule of inference that allowed it to infer from
A=1 ⇒ O=100000
and
all other promised outcomes are worse than 100000
that
A = 1.
But why would the first-order theory use such a rule of inference? You seem to have just given an argument for why we shouldn’t put this rule of inference into the theory.
ETA: I guess that my point leads right to your conclusion, and explains it. The agent is built so that, upon deducing the first two bullet-points, the agent proceeds to do the action assigned to the constant 1 by the interpretation. But the point is that the agent doesn’t bother to infer the third bullet-point; the agent just acts. As a result, it never deduces any formulas of the form [A=X], which is what you were saying.