wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."

About both the wording and the technical soundness of its intent:

1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.

2. You can always simulate that loop to see the actual number of iterations. Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?

3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.

4. Is this actually equivalent to "provably halts" but then that is equivalent to "halts" since halt <=> provably halts?

C-B

On Monday, 2 August 2021 at 15:01:04 UTC+1, Charlie-Boo wrote:
> wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."
>
> About both the wording and the technical soundness of its intent:
>
> 1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.
>
> 2. You can always simulate that loop to see the actual number of iterations. Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?
>
> 3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.
>
> 4. Is this actually equivalent to "provably halts" but then that is equivalent to "halts" since halt <=> provably halts?
>
> C-B
>
If a machine can be proved to halt, then of course it halts.
But if a machine halts, it's a bit more difficult. If you step it then eventually you will reach the halt state. But
that might be so many steps on that no earthly computer could ever simulate it. Now we know that there are
machines with very few states which take inordinate numbers of steps to reach a final halt state, basically
we are talking about six state machines with binary encoding being totally intractable.

On 02/08/2021 15:01, Charlie-Boo wrote:
> wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."
>
> About both the wording and the technical soundness of its intent:
>
> 1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.

? (don't see what you're getting at here. If you delete the words
"before entering the loop" the definition doesn't work, right?)

>
> 2. You can always simulate that loop to see the actual number of iterations. Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?

No, a simulated loop to count the iterations will in general involve
some kind of unbounded loop.

Hmm, that's probably not be what you're asking. If you're just saying
that specifically for a PR function we can always count the loop
iterations, that looks ok. It's doesn't work as a definition for PR
though, as it seems to be just saying that the computation terminates,
i.e. that the function is total recursive. There are functions that are
total recursive but not primitive recursive. Also of course, saying
that all loops terminate is not obviously an "effective" property which
can be confirmed just by looking at the code, whereas the PR definition
as given can be effective if the programming language is designed to
enforce the loop limit (or the programs are limited by structuring them
to make conformance obvious).

>
> 3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.

Not sure about this (more below...)

Perhaps the question is whether you are referring to a single given
input, or about an arbitrary input.

>
> 4. Is this actually equivalent to "provably halts"

I'd guess probably not, but more thought required! I expect you'd get a
more thorough answer over in sci.logic, but a few regulars there read
here too... (Also with "provably halts" you have the job of explaining
what that means, e.g. what formal system you're considering for the proof.)

> but then that is equivalent to "halts" since halt <=> provably halts?

?

Well, /for a given input/ :

privably halts --> halts [tick]
halts --> provably halts [tick]

If we're saying /for all inputs/ :

privably halts --> halts [tick]
halts --> provably halts [pretty sure not so!]

I think the question of "for a given input" versus "for any input" was
not on your mind, but it seems important here.

Mike.

On 02/08/2021 15:13, Malcolm McLean wrote:
> If a machine can be proved to halt, then of course it halts.
> But if a machine halts, it's a bit more difficult.

If it's not been proved to halt, then, as any fule kno,
it's rather more than a /bit/ more difficult. See the HP! Of
course, if it does halt on stepping, that constitutes a proof
of halting; absent such a proof, when do you stop? We know
from both the HP and BB that there is no computable answer to
that question. So you step, and it doesn't halt. You step
again and it still doesn't halt. You never know whether it's
never going to halt, or is about to halt on the next step.

Note that, in general, a proof of termination does not,
of itself, set a bound on the number of steps; cf, eg, the game
"Sylver Coinage" [qv], which is easily proved to terminate, but
can [tho' not with optimal play] take arbitrarily many steps
before progress is made into a new situation where arbitrarily
many steps can be taken before ....

> If you step it
> then eventually you will reach the halt state. But that might be so
> many steps on that no earthly computer could ever simulate it.

Plausibly yes, but irrelevant to the /theory/. Possibly
OTOH, it is at least conceivable that "earthly computer" power
could increase sufficiently rapidly to enable such a simulation.
Cf Zeno's paradox, where Achilles first has to run to where the
tortoise is "now", then to where it is "then", then to where ...;
yet in reality the infinity of steps is taken with sufficiently
increasing rapidity that Achilles has no difficulty in catching
and then overtaking the tortoise. Quantum computers, anyone?

--
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music
Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Chalon

On 8/2/2021 9:01 AM, Charlie-Boo wrote:
> wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."
>
> About both the wording and the technical soundness of its intent:
>
> 1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.
>
> 2. You can always simulate that loop to see the actual number of iterations. Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?
>
> 3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.
>
> 4. Is this actually equivalent to "provably halts" but then that is equivalent to "halts" since halt <=> provably halts?
>
> C-B
>

Provably halting is simply a pure simulation that reaches a final state.
Proving never halting is proving that the final state can never be
reached. Below is proof that P(P) halts and the input to H(P,P) never
halts.

There may be a very high tendency to reject this latter claim
out-of-hand without sufficient review through the human fallibility of
bias. If no error exists in steps (a)(b)(c) then we know that H(P,P)==0
is the correct halt status of the input to the input to H(P,P).

If P(P) halts and H(P,P)==0 is the correct halt status of the input to
the input to H(P,P) then we have a paradox rather than a contradiction.

Because H only acts as a pure simulator of its input until after its
halt status decision has been made it has no behavior that can possibly
effect the behavior of its input. Because of this H screens out its own
address range in every execution trace that it examines. This is why we
never see any instructions of H in any execution trace after an input
calls H.

Once we fully understand all of the above we can see from the execution
trace of H(P,P):

(1) The execution trace is correct because it corresponds to the x86
source-code of P.

(2) The execution trace of the simulation of P(P) cannot possibly ever
reach its final state whether or not this simulation is aborted.

int Simulate(u32 P, u32 I)
{ ((int(*)(int))P)(I);
return 1;
}

void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
}

void P()
{ if(PSR_Decider((u32)P, (u32)P)==0)
if(H1((u32)P, (u32)P))
HERE: goto HERE;
}

int main()
{ Output("Input_Halts = ", Simulate((u32)P, (u32)P));
}

(a) Whether or not H aborts its simulation of this input the input to
H(P,P) cannot possibly ever reach its final state (proved by the x86
execution trace shown below).

(b) Because input to H(P,P) cannot possibly ever reach its final state
we know that it never halts.

(c) Because it never halts we know that H(P,P) correctly returns 0
indicating that its input never halts.

(d) P reaches its final state.

_Simulate()
[00000ce2](01) 55 push ebp
[00000ce3](02) 8bec mov ebp,esp
[00000ce5](03) 8b450c mov eax,[ebp+0c]
[00000ce8](01) 50 push eax
[00000ce9](03) ff5508 call dword [ebp+08]
[00000cec](03) 83c404 add esp,+04
[00000cef](05) b801000000 mov eax,00000001
[00000cf4](01) 5d pop ebp
[00000cf5](01) c3 ret
Size in bytes:(0020) [00000cf5]

_P()
[00000d02](01) 55 push ebp
[00000d03](02) 8bec mov ebp,esp
[00000d05](03) 8b4508 mov eax,[ebp+08]
[00000d08](01) 50 push eax
[00000d09](03) 8b4d08 mov ecx,[ebp+08]
[00000d0c](01) 51 push ecx
[00000d0d](05) e870feffff call 00000b82
[00000d12](03) 83c408 add esp,+08
[00000d15](02) 85c0 test eax,eax
[00000d17](02) 7402 jz 00000d1b
[00000d19](02) ebfe jmp 00000d19
[00000d1b](01) 5d pop ebp
[00000d1c](01) c3 ret
Size in bytes:(0027) [00000d1c]

_main()
[00000d22](01) 55 push ebp
[00000d23](02) 8bec mov ebp,esp
[00000d25](05) 68020d0000 push 00000d02
[00000d2a](05) 68020d0000 push 00000d02
[00000d2f](05) e8aeffffff call 00000ce2
[00000d34](03) 83c408 add esp,+08
[00000d37](01) 50 push eax
[00000d38](05) 6823030000 push 00000323
[00000d3d](05) e810f6ffff call 00000352
[00000d42](03) 83c408 add esp,+08
[00000d45](02) 33c0 xor eax,eax
[00000d47](01) 5d pop ebp
[00000d48](01) c3 ret
Size in bytes:(0039) [00000d48]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
....[00000d22][00101851][00000000] 55 push ebp
....[00000d23][00101851][00000000] 8bec mov ebp,esp
....[00000d25][0010184d][00000d02] 68020d0000 push 00000d02
....[00000d2a][00101849][00000d02] 68020d0000 push 00000d02
....[00000d2f][00101845][00000d34] e8aeffffff call 00000ce2
....[00000ce2][00101841][00101851] 55 push ebp
....[00000ce3][00101841][00101851] 8bec mov ebp,esp
....[00000ce5][00101841][00101851] 8b450c mov eax,[ebp+0c]
....[00000ce8][0010183d][00000d02] 50 push eax
Calling:_P()
....[00000ce9][00101839][00000cec] ff5508 call dword [ebp+08]
....[00000d02][00101835][00101841] 55 push ebp
....[00000d03][00101835][00101841] 8bec mov ebp,esp
....[00000d05][00101835][00101841] 8b4508 mov eax,[ebp+08]
....[00000d08][00101831][00000d02] 50 push eax
....[00000d09][00101831][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][0010182d][00000d02] 51 push ecx
....[00000d0d][00101829][00000d12] e870feffff call 00000b82

Begin Local Halt Decider Simulation at Machine Address:d02
....[00000d02][002118f1][002118f5] 55 push ebp
....[00000d03][002118f1][002118f5] 8bec mov ebp,esp
....[00000d05][002118f1][002118f5] 8b4508 mov eax,[ebp+08]
....[00000d08][002118ed][00000d02] 50 push eax
....[00000d09][002118ed][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][002118e9][00000d02] 51 push ecx
....[00000d0d][002118e5][00000d12] e870feffff call 00000b82
....[00000d02][0025c319][0025c31d] 55 push ebp
....[00000d03][0025c319][0025c31d] 8bec mov ebp,esp
....[00000d05][0025c319][0025c31d] 8b4508 mov eax,[ebp+08]
....[00000d08][0025c315][00000d02] 50 push eax
....[00000d09][0025c315][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][0025c311][00000d02] 51 push ecx
....[00000d0d][0025c30d][00000d12] e870feffff call 00000b82
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

....[00000d12][00101835][00101841] 83c408 add esp,+08
....[00000d15][00101835][00101841] 85c0 test eax,eax
....[00000d17][00101835][00101841] 7402 jz 00000d1b
....[00000d1b][00101839][00000cec] 5d pop ebp
....[00000d1c][0010183d][00000d02] c3 ret
....[00000cec][00101841][00101851] 83c404 add esp,+04
....[00000cef][00101841][00101851] b801000000 mov eax,00000001
....[00000cf4][00101845][00000d34] 5d pop ebp
....[00000cf5][00101849][00000d02] c3 ret
....[00000d34][00101851][00000000] 83c408 add esp,+08
....[00000d37][0010184d][00000001] 50 push eax
....[00000d38][00101849][00000323] 6823030000 push 00000323
---[00000d3d][00101849][00000323] e810f6ffff call 00000352
Input_Halts = 1
....[00000d42][00101851][00000000] 83c408 add esp,+08
....[00000d45][00101851][00000000] 33c0 xor eax,eax
....[00000d47][00101855][00100000] 5d pop ebp
....[00000d48][00101859][000000bc] c3 ret
Number_of_User_Instructions(48)
Number of Instructions Executed(23742)

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

olcott wrote:
> On 8/2/2021 9:01 AM, Charlie-Boo wrote:
>> wiki: "a primitive recursive function is a function that can be
>> computed by a computer program [for which] an upper bound [on] the
>> number of iterations of every loop can be determined before entering
>> the loop."
>>
>> About both the wording and the technical soundness of its intent:
>>
>> 1. You can perform calculations equivalent to "entering the loop" so
>> that's inconsequential.
>>
>> 2. You can always simulate that loop to see the actual number of
>> iterations.  Is that ok even though it doesn't terminate if applied to
>> a program that doesn't meet this criteria?
>>
>> 3. Since it calculates a total function it halts and you can prove
>> everything about it because you can simulate its complete execution.
>>
>> 4. Is this actually equivalent to "provably halts" but then that is
>> equivalent to "halts" since halt <=> provably halts?
>>
>> C-B
>>
>
> Provably halting is simply a pure simulation that reaches a final state. [...]

No, it means provable in some specified theory such as Peano arithmetic.
--
The world will little note, nor long remember what we say here
Abraham Lincoln at Gettysburg

On 8/2/21 9:54 AM, olcott wrote:
> On 8/2/2021 9:01 AM, Charlie-Boo wrote:
>> wiki: "a primitive recursive function is a function that can be
>> computed by a computer program [for which] an upper bound [on] the
>> number of iterations of every loop can be determined before entering
>> the loop."
>>
>> About both the wording and the technical soundness of its intent:
>>
>> 1. You can perform calculations equivalent to "entering the loop" so
>> that's inconsequential.
>>
>> 2. You can always simulate that loop to see the actual number of
>> iterations.  Is that ok even though it doesn't terminate if applied to
>> a program that doesn't meet this criteria?
>>
>> 3. Since it calculates a total function it halts and you can prove
>> everything about it because you can simulate its complete execution.
>>
>> 4. Is this actually equivalent to "provably halts" but then that is
>> equivalent to "halts" since halt <=> provably halts?
>>
>> C-B
>>
>
> Provably halting is simply a pure simulation that reaches a final state.
> Proving never halting is proving that the final state can never be
> reached. Below is proof that P(P) halts and the input to H(P,P) never
> halts.

Can never be reached by a PURE simulator, ie one that doesn't stop
simulating until it reaches the end.
>
> There may be a very high tendency to reject this latter claim
> out-of-hand without sufficient review through the human fallibility of
> bias. If no error exists in steps (a)(b)(c) then we know that H(P,P)==0
> is the correct halt status of the input to the input to H(P,P).

A partial simulator that aborts its simulation does NOT prove non-halting.

>
> If P(P) halts and H(P,P)==0 is the correct halt status of the input to
> the input to H(P,P) then we have a paradox rather than a contradiction.

You have an inconsistency. If the right answer is the wrong answer than
you system is kaput.

>
> Because H only acts as a pure simulator of its input until after its
> halt status decision has been made it has no behavior that can possibly
> effect the behavior of its input. Because of this H screens out its own
> address range in every execution trace that it examines. This is why we
> never see any instructions of H in any execution trace after an input
> calls H.

But acting as a pure simulator until, is NOT truly acting as a pure
simulator. The definition of a Pure Simulator is one that doesn't stop
until its input reaches it Halting State.

>
> Once we fully understand all of the above we can see from the execution
> trace of H(P,P):
>

Which is incorrect as previously noted many times.

> (1) The execution trace is correct because it corresponds to the x86
> source-code of P.

I know on NO x86 that a call to 0xB82 causes execution to go to 0xD02,
do you?

I think you have a broken simulator.
>
> (2) The execution trace of the simulation of P(P) cannot possibly ever
> reach its final state whether or not this simulation is aborted.

Please note, also, that you simulation of the top level P DID reach its
terminal address 0xD1C and thus this trace actually shows that P(P) is a
halting machine.

>
> int Simulate(u32 P, u32 I)
> {
>   ((int(*)(int))P)(I);
>   return 1;
> }
>
> void P(u32 x)
> {
>   if (H(x, x))
>     HERE: goto HERE;
> }
>
> void P()
> {
>   if(PSR_Decider((u32)P, (u32)P)==0)
>     if(H1((u32)P, (u32)P))
>       HERE: goto HERE;
> }
>
> int main()
> {
>   Output("Input_Halts = ", Simulate((u32)P, (u32)P));
> }
>
> (a) Whether or not H aborts its simulation of this input the input to
> H(P,P) cannot possibly ever reach its final state (proved by the x86
> execution trace shown below).

That does't matter, it is does P(P) reach its final state.

>
> (b) Because input to H(P,P) cannot possibly ever reach its final state
> we know that it never halts.

UNSOUND.

>
> (c) Because it never halts we know that H(P,P) correctly returns 0
> indicating that its input never halts.

FALSE.
>
> (d) P reaches its final state.
>
> _Simulate()
> [00000ce2](01)  55          push ebp
> [00000ce3](02)  8bec        mov ebp,esp
> [00000ce5](03)  8b450c      mov eax,[ebp+0c]
> [00000ce8](01)  50          push eax
> [00000ce9](03)  ff5508      call dword [ebp+08]
> [00000cec](03)  83c404      add esp,+04
> [00000cef](05)  b801000000  mov eax,00000001
> [00000cf4](01)  5d          pop ebp
> [00000cf5](01)  c3          ret
> Size in bytes:(0020) [00000cf5]
>
> _P()
> [00000d02](01)  55          push ebp
> [00000d03](02)  8bec        mov ebp,esp
> [00000d05](03)  8b4508      mov eax,[ebp+08]
> [00000d08](01)  50          push eax
> [00000d09](03)  8b4d08      mov ecx,[ebp+08]
> [00000d0c](01)  51          push ecx
> [00000d0d](05)  e870feffff  call 00000b82
> [00000d12](03)  83c408      add esp,+08
> [00000d15](02)  85c0        test eax,eax
> [00000d17](02)  7402        jz 00000d1b
> [00000d19](02)  ebfe        jmp 00000d19
> [00000d1b](01)  5d          pop ebp
> [00000d1c](01)  c3          ret
> Size in bytes:(0027) [00000d1c]
>
> _main()
> [00000d22](01)  55          push ebp
> [00000d23](02)  8bec        mov ebp,esp
> [00000d25](05)  68020d0000  push 00000d02
> [00000d2a](05)  68020d0000  push 00000d02
> [00000d2f](05)  e8aeffffff  call 00000ce2
> [00000d34](03)  83c408      add esp,+08
> [00000d37](01)  50          push eax
> [00000d38](05)  6823030000  push 00000323
> [00000d3d](05)  e810f6ffff  call 00000352
> [00000d42](03)  83c408      add esp,+08
> [00000d45](02)  33c0        xor eax,eax
> [00000d47](01)  5d          pop ebp
> [00000d48](01)  c3          ret
> Size in bytes:(0039) [00000d48]
>
>  machine   stack     stack     machine    assembly
>  address   address   data      code       language
>  ========  ========  ========  =========  =============
> ...[00000d22][00101851][00000000] 55          push ebp
> ...[00000d23][00101851][00000000] 8bec        mov ebp,esp
> ...[00000d25][0010184d][00000d02] 68020d0000  push 00000d02
> ...[00000d2a][00101849][00000d02] 68020d0000  push 00000d02
> ...[00000d2f][00101845][00000d34] e8aeffffff  call 00000ce2
> ...[00000ce2][00101841][00101851] 55          push ebp
> ...[00000ce3][00101841][00101851] 8bec        mov ebp,esp
> ...[00000ce5][00101841][00101851] 8b450c      mov eax,[ebp+0c]
> ...[00000ce8][0010183d][00000d02] 50          push eax
> Calling:_P()
> ...[00000ce9][00101839][00000cec] ff5508      call dword [ebp+08]
> ...[00000d02][00101835][00101841] 55          push ebp
> ...[00000d03][00101835][00101841] 8bec        mov ebp,esp
> ...[00000d05][00101835][00101841] 8b4508      mov eax,[ebp+08]
> ...[00000d08][00101831][00000d02] 50          push eax
> ...[00000d09][00101831][00000d02] 8b4d08      mov ecx,[ebp+08]
> ...[00000d0c][0010182d][00000d02] 51          push ecx
> ...[00000d0d][00101829][00000d12] e870feffff  call 00000b82
>
> Begin Local Halt Decider Simulation at Machine Address:d02
> ...[00000d02][002118f1][002118f5] 55          push ebp
> ...[00000d03][002118f1][002118f5] 8bec        mov ebp,esp
> ...[00000d05][002118f1][002118f5] 8b4508      mov eax,[ebp+08]
> ...[00000d08][002118ed][00000d02] 50          push eax
> ...[00000d09][002118ed][00000d02] 8b4d08      mov ecx,[ebp+08]
> ...[00000d0c][002118e9][00000d02] 51          push ecx
> ...[00000d0d][002118e5][00000d12] e870feffff  call 00000b82
> ...[00000d02][0025c319][0025c31d] 55          push ebp
> ...[00000d03][0025c319][0025c31d] 8bec        mov ebp,esp
> ...[00000d05][0025c319][0025c31d] 8b4508      mov eax,[ebp+08]
> ...[00000d08][0025c315][00000d02] 50          push eax
> ...[00000d09][0025c315][00000d02] 8b4d08      mov ecx,[ebp+08]
> ...[00000d0c][0025c311][00000d02] 51          push ecx
> ...[00000d0d][0025c30d][00000d12] e870feffff  call 00000b82
> Local Halt Decider: Infinite Recursion Detected Simulation Stopped
>
> ...[00000d12][00101835][00101841] 83c408      add esp,+08
> ...[00000d15][00101835][00101841] 85c0        test eax,eax
> ...[00000d17][00101835][00101841] 7402        jz 00000d1b
> ...[00000d1b][00101839][00000cec] 5d          pop ebp
> ...[00000d1c][0010183d][00000d02] c3          ret
> ...[00000cec][00101841][00101851] 83c404      add esp,+04
> ...[00000cef][00101841][00101851] b801000000  mov eax,00000001
> ...[00000cf4][00101845][00000d34] 5d          pop ebp
> ...[00000cf5][00101849][00000d02] c3          ret
> ...[00000d34][00101851][00000000] 83c408      add esp,+08
> ...[00000d37][0010184d][00000001] 50          push eax
> ...[00000d38][00101849][00000323] 6823030000  push 00000323
> ---[00000d3d][00101849][00000323] e810f6ffff  call 00000352
> Input_Halts = 1
> ...[00000d42][00101851][00000000] 83c408      add esp,+08
> ...[00000d45][00101851][00000000] 33c0        xor eax,eax
> ...[00000d47][00101855][00100000] 5d          pop ebp
> ...[00000d48][00101859][000000bc] c3          ret
> Number_of_User_Instructions(48)
> Number of Instructions Executed(23742)
>
>

On Monday, 2 August 2021 at 22:01:04 UTC+8, Charlie-Boo wrote:
> wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."
>
> About both the wording and the technical soundness of its intent:
>
> 1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.
>
> 2. You can always simulate that loop to see the actual number of iterations. Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?
>
> 3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.
>
> 4. Is this actually equivalent to "provably halts" but then that is equivalent to "halts" since halt <=> provably halts?
>
> C-B

I just respond to "provably halts" and "halts" in the traditional HP context.

See GUR example 2: https://groups.google.com/g/comp.theory/c/_tbCYyMox9M
U can be anything(e.g. Computer-God). No doubt CG can prove P halts or not
(Human can probably prove P halts or not, too).
BUT, if P can use the result, then the problem becomes undecidable.