I suppose in addition to confirming that it’s wrong I should tell you what it was supposed to mean. For that I’ll appeal to some concepts that I considered when I was first working on the problem last Wednesday. Imagine a formula taking encoding terms to encoding terms, such that whenver we’re given t which codes a proof for P from A2 then the formula applied to t produces s, a term encoding a proof of P from A1. If the A1 can construct that formula, then it should trust A2. That isn’t hugely helpful for solving the problem, because when A1 and A2 are equivalent, we can just use t-type codes as s-type codes, and when they’re not then we need to impose heavy restrictions on allowable t-type codes. Also that absolutely does require limiting the set of P. Once you satisfy both of those, you basically can embed a fragment of A2 in A1 and A1 in the fragment, though that’s not quite how you go about doing it. There, epistemic duty mostly satisfied for the night.
I suppose in addition to confirming that it’s wrong I should tell you what it was supposed to mean. For that I’ll appeal to some concepts that I considered when I was first working on the problem last Wednesday. Imagine a formula taking encoding terms to encoding terms, such that whenver we’re given t which codes a proof for P from A2 then the formula applied to t produces s, a term encoding a proof of P from A1. If the A1 can construct that formula, then it should trust A2. That isn’t hugely helpful for solving the problem, because when A1 and A2 are equivalent, we can just use t-type codes as s-type codes, and when they’re not then we need to impose heavy restrictions on allowable t-type codes. Also that absolutely does require limiting the set of P. Once you satisfy both of those, you basically can embed a fragment of A2 in A1 and A1 in the fragment, though that’s not quite how you go about doing it. There, epistemic duty mostly satisfied for the night.