the diagonal rule guarantees that □(~A()=a) ⇒ A()=a
Something like that, but not quite, as you can’t get an implication from provability if agent is a program, it’s not decidable (unless you use a provability oracle). So you only impose some finite difficulty on (un)provability of a statement, not outright impossibility. See this comment.
You’re saying, the use of “□” is not justified, because for the agent it means “provable with a proof length of up to N” and not simply “provable”?
This is technically correct, but is this case significantly different from the cases where we assume variables in programming languages are integers, when in fact they are members of Zn for some large n? The resource limits only mean we have to additionally prove that (1) the modal logic axioms hold for all statements with sufficiently short proofs, or something like that, and (2) that the N is sufficiently large for our purposes.
Something like that, but not quite, as you can’t get an implication from provability if agent is a program, it’s not decidable (unless you use a provability oracle). So you only impose some finite difficulty on (un)provability of a statement, not outright impossibility. See this comment.
You’re saying, the use of “□” is not justified, because for the agent it means “provable with a proof length of up to N” and not simply “provable”?
This is technically correct, but is this case significantly different from the cases where we assume variables in programming languages are integers, when in fact they are members of Zn for some large n? The resource limits only mean we have to additionally prove that (1) the modal logic axioms hold for all statements with sufficiently short proofs, or something like that, and (2) that the N is sufficiently large for our purposes.