Something I’m now realizing, having written all these down: the core mechanism really does echo Löb’s theorem! Gah, maybe these are more like Löb than I thought.
(My whole hope was to generalize to things that Löb’s theorem doesn’t! And maybe these ideas still do, but my story for why has broken, and I’m now confused.)
As something to ponder on, let me show you how we can prove Löb’s theorem following the method of ideas #3 and #5:
□A→A is assumed
We consider the loop-cutter X↔□(X→A)
We verify that if X activates then A must be true:
X→(□X→□A)
X→□X
X→□A
X→A
Then, X can satisfy □(X→A) by finding the same proof.
So X activates, and A is true.
In english:
We have A who is blocked on □A
We introduce A to the loop cutter X, who will activate if activation provably leads to A being true
A encounters the argument “if X activates then A is true, and this causes X to activate”
This satisfies A’s requirement for some □A, so A becomes true.
Something I’m now realizing, having written all these down: the core mechanism really does echo Löb’s theorem! Gah, maybe these are more like Löb than I thought.
(My whole hope was to generalize to things that Löb’s theorem doesn’t! And maybe these ideas still do, but my story for why has broken, and I’m now confused.)
As something to ponder on, let me show you how we can prove Löb’s theorem following the method of ideas #3 and #5:
□A→A is assumed
We consider the loop-cutter X↔□(X→A)
We verify that if X activates then A must be true:
X→(□X→□A)
X→□X
X→□A
X→A
Then, X can satisfy □(X→A) by finding the same proof.
So X activates, and A is true.
In english:
We have A who is blocked on □A
We introduce A to the loop cutter X, who will activate if activation provably leads to A being true
A encounters the argument “if X activates then A is true, and this causes X to activate”
This satisfies A’s requirement for some □A, so A becomes true.