Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

In computing, the mean time to failure keeps getting shorter.


computers / comp.ai.philosophy / Re: Honest dialogue on the proof that H(P,P)==0 is correct [proof defined]

Subject: Re: Honest dialogue on the proof that H(P,P)==0 is correct [proof defined]
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng, sci.math.symbolic
Date: Mon, 9 Aug 2021 16:57 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Mon, 09 Aug 2021 11:57:11 -0500
Subject: Re: Honest dialogue on the proof that H(P,P)==0 is correct [proof
defined]
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng,sci.math.symbolic
References: <HNidndugKOWGvpH8nZ2dnUU7-fXNnZ2d@giganews.com>
<Vs0PI.2099$xY.509@fx05.iad> <GLudnUM2eaoEC5H8nZ2dnUU7-evNnZ2d@giganews.com>
<5Z1PI.1823$6h1.1128@fx39.iad>
<r6idnXrkQsZ5JJH8nZ2dnUU7-V_NnZ2d@giganews.com> <qb9PI.22$uV3.2@fx18.iad>
<6radnYHwiMoYvpD8nZ2dnUU7-UPNnZ2d@giganews.com> <owaPI.297$uk4.251@fx20.iad>
<a82dnc_0ypriwZD8nZ2dnUU7-QHNnZ2d@giganews.com> <sel07d$pcf$1@dont-email.me>
<DdCdnaOAJLE3l5P8nZ2dnUU7-enNnZ2d@giganews.com> <sep914$6pc$1@dont-email.me>
From: NoO...@NoWhere.com (olcott)
Date: Mon, 9 Aug 2021 11:57:10 -0500
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.12.0
MIME-Version: 1.0
In-Reply-To: <sep914$6pc$1@dont-email.me>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <mdKdncO0j8L6w4z8nZ2dnUU7-S_NnZ2d@giganews.com>
Lines: 220
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-Gt4MQfEDhezofSWn2YNJLGeEsUFjK6Q3I32uNwyAakogChEU+x/KNs9B+eqNloNEoCAUwnMq5mGu4h4!AGLclol1jvlGHwNc+L040aGPcLcpIfIEYo7BlsmWQfV+jOedYRSL093i/hyrFTOf82oDduDrMQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 10819
View all headers
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


SubjectRepliesAuthor
o Anyone wanting an actual honestly dialogue on the proof that H(P,P)==0

By: olcott on Thu, 5 Aug 2021

15olcott
rocksolid light 0.7.2
clearneti2ptor