My thoughts on this problem were: define a predicate quasi_safe(p), equivalent to:
p does not self-destruct after 0 time steps
PA proves p does not self destruct after 1 time step
PA proves PA proves p does not self destruct after 2 time steps
PA proves PA proves PA proves p does not self destruct after 3 time steps
etc.
(I may have some off-by-one errors in that but that was the general idea). In the OP’s statement of the problem, a time step can represent either a single step of computation or halting with “double down” and being instantaneously replaced with Quirrel’s new program.
Anyway, I reckoned that:
As outsiders with superior wisdom, i.e. with some proof system stronger than PA, we can show that quasi-safe implies safe, i.e. quasi-safe programs never self destruct
There exists a program which accepts provably quasi-safe programs, which is itself quasi-safe.
Should I write this up or am I obviously confused about something?
My thoughts on this problem were: define a predicate quasi_safe(p), equivalent to:
p does not self-destruct after 0 time steps
PA proves p does not self destruct after 1 time step
PA proves PA proves p does not self destruct after 2 time steps
PA proves PA proves PA proves p does not self destruct after 3 time steps
etc.
(I may have some off-by-one errors in that but that was the general idea). In the OP’s statement of the problem, a time step can represent either a single step of computation or halting with “double down” and being instantaneously replaced with Quirrel’s new program.
Anyway, I reckoned that:
As outsiders with superior wisdom, i.e. with some proof system stronger than PA, we can show that quasi-safe implies safe, i.e. quasi-safe programs never self destruct
There exists a program which accepts provably quasi-safe programs, which is itself quasi-safe.
Should I write this up or am I obviously confused about something?
I’ve started wondering whether this may be closely related to Wei Dai’s quining approach; posted some preliminary thoughts here.
(Sorry for the delayed reply.) Yeah, that does sound as if it could work! Would be helpful to see the details.