Yes. If you call it with the argument AIQ2_T (i.e. the same algorithm but with T instead of PA(omega)), it will accept if it can find a proof that forall q,
AIQ2_T(q) != ‘self-destruct’
(which is easy) and
AIQ2_T(q) == ‘double’ ==> AIQ2(q)==‘double’
The latter condition expands to
PA(omega) |- someFormula ==> T |- someFormula
which may be quite easy to show, depending on T.
Basically, the Quining approach avoids trouble from the 2nd incompleteness theorem by using relative consistency instead of consistency.
It seems to me that the two programs don’t have the same “someFormula”, because each program’s formula uses a quined description of that program, but not the other one. Or maybe I’m wrong. Can you expand what you mean by “someFormula”?
Yes. If you call it with the argument AIQ2_T (i.e. the same algorithm but with T instead of PA(omega)), it will accept if it can find a proof that forall q,
AIQ2_T(q) != ‘self-destruct’
(which is easy) and
AIQ2_T(q) == ‘double’ ==> AIQ2(q)==‘double’
The latter condition expands to
PA(omega) |- someFormula ==> T |- someFormula
which may be quite easy to show, depending on T.
Basically, the Quining approach avoids trouble from the 2nd incompleteness theorem by using relative consistency instead of consistency.
It seems to me that the two programs don’t have the same “someFormula”, because each program’s formula uses a quined description of that program, but not the other one. Or maybe I’m wrong. Can you expand what you mean by “someFormula”?
Oops.