I don’t think we’ve defined “escalating modal UDT” on this forum yet; as is clear from context, we mean the agent like the one in this post, except that instead of having a single value of the parameter ℓ, the escalating version increments that parameter every time it fails at finding a proof.
This has the intuitive benefit that the later stages can prove that the earlier stages failed to find a proof (because they know the consistency of all earlier proof systems used).
I don’t think we’ve defined “escalating modal UDT” on this forum yet; as is clear from context, we mean the agent like the one in this post, except that instead of having a single value of the parameter ℓ, the escalating version increments that parameter every time it fails at finding a proof.
This has the intuitive benefit that the later stages can prove that the earlier stages failed to find a proof (because they know the consistency of all earlier proof systems used).