On 8/8/2021 1:50 PM, André G. Isaak wrote:
> On 2021-08-06 22:23, olcott wrote:
>> On 8/6/2021 10:55 PM, André G. Isaak wrote:
>>> On 2021-08-06 09:59, olcott wrote:
>
>>> Yes, but bear in mind that 'halting' refers to Turing Machines
>>> operating on a specific input. It does not refer to simulations or
>>> what happens inside a halting decider. It refers *only* to actual
>>> computations, i.e. an actual Turing Machine operating on an actual
>>> input string.
>>>
>>
>> So yet again you prove that you are totally clueless that pure
>> simulations are computationally equivalent to direct executions ?
>
> Your H is not a pure simulator
>

// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
}

_P()
[00000d02](01) 55 push ebp
[00000d03](02) 8bec mov ebp,esp
[00000d05](03) 8b4508 mov eax,[ebp+08]
[00000d08](01) 50 push eax // push 2nd Param
[00000d09](03) 8b4d08 mov ecx,[ebp+08]
[00000d0c](01) 51 push ecx // push 1st Param
[00000d0d](05) e870feffff call 00000b82 // call H
[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]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
....[00000d0d][00101829][00000d12] e870feffff call 00000b82 // call H

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 // push P
....[00000d09][002118ed][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][002118e9][00000d02] 51 push ecx // push P
....[00000d0d][002118e5][00000d12] e870feffff call 00000b82 // call H
....[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 // push P
....[00000d09][0025c315][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][0025c311][00000d02] 51 push ecx // push P
....[00000d0d][0025c30d][00000d12] e870feffff call 00000b82 // call H
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

The fact that the execution trace of the simulation of P(P) on page 6
perfectly matches its source-code on page 5 conclusively proves that
this execution trace performed by H is a pure simulation of P(P). There
is no correct basis for disagreement, therefore anyone disagreeing
either does not know the x86 language or they are simply lying.

https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation

>>>> (3) Equivalent, I have adapted the original definition to apply to
>>>> subsets of computations.
>>>
>>> I have no idea what that's even supposed to mean.
>>>
>>>> (4) Correct means that the condition of a conditional expression is
>>>> satisfied.
>>>
>>> Again, I have no idea what that's even supposed to mean.
>>>
>>>> (5) Proof, here is what I mean by proof, it is an adaptation of the
>>>> sound deductive inference model such that valid inference must only
>>>> include true preserving operations.
>>>>
>>>> By proof I mean the application of truth preserving inference steps
>>>> to premises that are known to be true. Since mathematical logic has
>>>> some inference steps that are not truth preserving these are ruled out.
>>>> https://en.wikipedia.org/wiki/Principle_of_explosion
>>>> https://en.wikipedia.org/wiki/Paradoxes_of_material_implication
>>>>
>>>> Validity and Soundness
>>>> A deductive argument is said to be valid if and only if it takes a
>>>> form that makes it impossible for the premises to be true and the
>>>> conclusion nevertheless to be false. Otherwise, a deductive argument
>>>> is said to be invalid.
>>>>
>>>> A deductive argument is sound if and only if it is both valid, and
>>>> all of its premises are actually true. Otherwise, a deductive
>>>> argument is unsound. https://iep.utm.edu/val-snd/
>>>>
>>>> // original definition of valid  (same as P → C)
>>>>
>>>> Material conditional
>>>> p   q p → q
>>>> T   T   T
>>>> T   F   F
>>>> F   T   T
>>>> F   F   T
>>>>
>>>> Transforming the above to become truth preserving:
>>>>
>>>> The definition of valid is changed to:
>>>> p   q   p [PROVES] q
>>>> T   T        T
>>>> T   F        F
>>>> F   T        F
>>>> F   F        F
>>>
>>> That is definitely *not* the definition of valid.
>>>
>>
>> It might be simplest to call what I consider proof simply sound
>> deductive inference.
>
> Nothing you write above has anything to do with validity or sound
> deductive inference.
>
> The truth table you give above is for AND. Olympia is the capital of
> Washington. Salem is the capital of Oregon. It is certainly *not* the
> case the either of these statements can 'prove' the other, but according
> to your table.
>
> Salem is the capital of Oregon PROVES Olympia is the capital of Washington.
>
>>>> A deductive argument is said to be valid if and only if it takes a form
>>>> that the conclusion is only true if and only if the premises are true.
>>>>
>>>> All of the above is summed up as
>>>> P [PROVES] C if and only if (True(P) ⊢ True(C) ∧ False(P) ⊢ False(C))
>>>
>>> Again, that is definitely *not* the definition of a proof.
>>>
>>>> modal operators are most often interpreted
>>>> "□" for "Necessarily" and "◇" for "Possibly".
>>>> https://en.wikipedia.org/wiki/Modal_logic
>>>> (P [PROVES] C) ↔ (P ↔ □C)
>
> So [PROVES] is your synomym for and and is now also equivalent to 'if
> and only if'? You need to go back to logic 101.
>
> And since P ⊢ C means something entirely different from P ⊢□C, you need
> to justify how that '□' magically appears. But since you don't know what
> it means that's going to be difficult for you.
>
>>> Not only is that not the definition of proof, but your use of □ is
>>> entirely meaningless above.
>>>
>>> You do realise that □ conveys absolutely *no* information unless you
>>
>> "□" for "Necessarily"
>
> Gee thanks. I already new that. And once again that conveys absolutely
> no information unless you explain what you mean by 'necessarily'. The
> fact that you don't understand what is being asked here just confirms my
> point that you have no idea what □ means and therefore shouldn't be
> using it.
>
> There are *many* different modal logics. In all of them □ is referred to
> as a necessity operator, but it *means* entirely different things. You
> can't just start throwing modal operators around unless you specify
> *which* type of modal logic you are using.
>>>
>>> *All* of the errors which have been pointed out to you have been
>>> errors in the actual argument.
>>
>> No you always make sure to avoid that part.
>>
>> This code proves that P has no escape from infinitely nested simulation.
>> The escape that exists is not in P. In both cases escape/no escape P
>> never reaches its final state of 0xc3f, therefore P never halts.
>
> No, it does not. In P(P) P creates a simulation of P. That simulation is
> eventually aborted and control returns to the outermost P which then halts.
>
> Since your trace completely skips over the call to 955 that abort code
> is not seen which means the the return of control to the outermost P is
> also not seen.
>
> There is *no* justification for not including the code of H in this trace.
>
>> _P()
>> [00000c25](01)  55          push ebp
>> [00000c26](02)  8bec        mov ebp,esp
>> [00000c28](03)  8b4508      mov eax,[ebp+08]
>> [00000c2b](01)  50          push eax       // push P
>> [00000c2c](03)  8b4d08      mov ecx,[ebp+08]
>> [00000c2f](01)  51          push ecx       // push P
>> [00000c30](05)  e820fdffff  call 00000955  // call H to simulate P
>> [00000c35](03)  83c408      add esp,+08
>> [00000c38](02)  85c0        test eax,eax
>> [00000c3a](02)  7402        jz 00000c3e
>> [00000c3c](02)  ebfe        jmp 00000c3c
>> [00000c3e](01)  5d          pop ebp
>> [00000c3f](01)  c3          ret
>> Size in bytes:(0027) [00000c3f]
>
>
> André
>
>

--
Copyright 2021 Pete Olcott

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