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.
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.