Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ](V2)

[olcott]

Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]

The x86utm operating system was created so that every detail of the
conventional halting problem counter example could be fully specified in
C/x86.

In computability theory, the halting problem is the
problem of determining, from a description of an
arbitrary computer program and an input, whether the
program will finish running, or continue to run forever...

For any program f that might determine if programs halt,
a "pathological" program g, called with some input, can
pass its own source and its input to f and then specifically
do the opposite of what f predicts g will do. No f can exist
that handles this case. https://en.wikipedia.org/wiki/Halting_problem

This exact same relationship of f(g,g) was created as H(P,P), shown below.

This is the overview of the method for proving that this analysis is
correct:
(a) Verify that the execution trace of P by H is correct by comparing
this execution trace to the ax86 source-code of P.

(b) Verify that this execution trace shows that P is stuck in infinitely
nested simulation (a non-halting behavior).

This proof can only be understood only by those having sufficient
technical competence in:
(a) software engineering (recognizing infinite recursion in C and x86 code)
(b) the x86 programming language
(c) the C programming language and
(d) the details of how C is translated into x86 by the Microsoft C
compilers.

#include <stdint.h>
#define u32 uint32_t

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

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

_P()
[00001352](01) 55 push ebp
[00001353](02) 8bec mov ebp,esp
[00001355](03) 8b4508 mov eax,[ebp+08]
[00001358](01) 50 push eax
[00001359](03) 8b4d08 mov ecx,[ebp+08]
[0000135c](01) 51 push ecx
[0000135d](05) e840feffff call 000011a2 // call H
[00001362](03) 83c408 add esp,+08
[00001365](02) 85c0 test eax,eax
[00001367](02) 7402 jz 0000136b
[00001369](02) ebfe jmp 00001369
[0000136b](01) 5d pop ebp
[0000136c](01) c3 ret
Size in bytes:(0027) [0000136c]

_main()
[00001372](01) 55 push ebp
[00001373](02) 8bec mov ebp,esp
[00001375](05) 6852130000 push 00001352 // push P
[0000137a](05) 6852130000 push 00001352 // push P
[0000137f](05) e81efeffff call 000011a2 // call H
[00001384](03) 83c408 add esp,+08
[00001387](01) 50 push eax
[00001388](05) 6823040000 push 00000423 // "Input_Halts = "
[0000138d](05) e8e0f0ffff call 00000472 // call Output
[00001392](03) 83c408 add esp,+08
[00001395](02) 33c0 xor eax,eax
[00001397](01) 5d pop ebp
[00001398](01) c3 ret
Size in bytes:(0039) [00001398]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
...[00001372][0010229e][00000000] 55 push ebp
...[00001373][0010229e][00000000] 8bec mov ebp,esp
...[00001375][0010229a][00001352] 6852130000 push 00001352 // push P
...[0000137a][00102296][00001352] 6852130000 push 00001352 // push P
...[0000137f][00102292][00001384] e81efeffff call 000011a2 // call H

Begin Local Halt Decider Simulation Execution Trace Stored at:212352
...[00001352][0021233e][00212342] 55 push ebp // enter P
...[00001353][0021233e][00212342] 8bec mov ebp,esp
...[00001355][0021233e][00212342] 8b4508 mov eax,[ebp+08]
...[00001358][0021233a][00001352] 50 push eax // push P
...[00001359][0021233a][00001352] 8b4d08 mov ecx,[ebp+08]
...[0000135c][00212336][00001352] 51 push ecx // push P
...[0000135d][00212332][00001362] e840feffff call 000011a2 // call H
...[00001352][0025cd66][0025cd6a] 55 push ebp // enter P
...[00001353][0025cd66][0025cd6a] 8bec mov ebp,esp
...[00001355][0025cd66][0025cd6a] 8b4508 mov eax,[ebp+08]
...[00001358][0025cd62][00001352] 50 push eax // push P
...[00001359][0025cd62][00001352] 8b4d08 mov ecx,[ebp+08]
...[0000135c][0025cd5e][00001352] 51 push ecx // push P
...[0000135d][0025cd5a][00001362] e840feffff call 000011a2 // call H
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

H sees that P is calling the same function from the same machine address
with identical parameters, twice in sequence. This is the infinite
recursion (infinitely nested simulation) non-halting behavior pattern.

...[00001384][0010229e][00000000] 83c408 add esp,+08
...[00001387][0010229a][00000000] 50 push eax
...[00001388][00102296][00000423] 6823040000 push 00000423 //
"Input_Halts = "
---[0000138d][00102296][00000423] e8e0f0ffff call 00000472 // call Output
Input_Halts = 0
...[00001392][0010229e][00000000] 83c408 add esp,+08
...[00001395][0010229e][00000000] 33c0 xor eax,eax
...[00001397][001022a2][00100000] 5d pop ebp
...[00001398][001022a6][00000004] c3 ret
Number of Instructions Executed(15892) lines = 237 pages


Halting problem undecidability and infinitely nested simulation (V5)

https://www.researchgate.net/publication/359984584_Halting_problem_undecidability_and_infinitely_nested_simulation_V5


--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

[Mr Flibble]

Your simulation approach is erroneous as there is no infinite
recursion; the key to understanding this is by realizing the
implication of the words "pass its own source" in the following:

For any program f that might determine if programs halt,
a "pathological" program g, called with some input, can
pass its own source and its input to f and then specifically
do the opposite of what f predicts g will do. No f can exist
that handles this case.

"pass its own source" is NOT the same as compiling and running its own
source as part of a simulation.

/Flibble

[Richard Damon]

On 5/11/22 2:07 PM, olcott wrote:
> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>
> The x86utm operating system was created so that every detail of the
> conventional halting problem counter example could be fully specified in
> C/x86.
>
>    In computability theory, the halting problem is the
>    problem of determining, from a description of an
>    arbitrary computer program and an input, whether the
>    program will finish running, or continue to run forever...
>
>    For any program f that might determine if programs halt,
>    a "pathological" program g, called with some input, can
>    pass its own source and its input to f and then specifically
>    do the opposite of what f predicts g will do. No f can exist
>    that handles this case. https://en.wikipedia.org/wiki/Halting_problem
>
> This exact same relationship of f(g,g) was created as H(P,P), shown below.
>
> This is the overview of the method for proving that this analysis is
> correct:
> (a) Verify that the execution trace of P by H is correct by comparing
> this execution trace to the ax86 source-code of P.

Except that this fails!!

The x86 code shows that P calls H.

The simulation doesn't but seems to act like a call to H is just a call
to P.

Even if you edit out the 'setup' code in H, unless H just calls P (and
not simulates it) the trace is incorrect, but should be showing H
actually simulating P.

>
> (b) Verify that this execution trace shows that P is stuck in infinitely
> nested simulation (a non-halting behavior).

Since the trace is incorrect, the logic is UNSOUND.

>
> This proof can only be understood only by those having sufficient
> technical competence in:
> (a) software engineering (recognizing infinite recursion in C and x86 code)
> (b) the x86 programming language
> (c) the C programming language and
> (d) the details of how C is translated into x86 by the Microsoft C
> compilers.

Which you seem to lack, as you seem to think that a call to H is a call
to P.

FAIL.

Error begins here.

> ...[00001352][0025cd66][0025cd6a] 55         push ebp      // enter P
> ...[00001353][0025cd66][0025cd6a] 8bec       mov ebp,esp
> ...[00001355][0025cd66][0025cd6a] 8b4508     mov eax,[ebp+08]
> ...[00001358][0025cd62][00001352] 50         push eax      // push P
> ...[00001359][0025cd62][00001352] 8b4d08     mov ecx,[ebp+08]
> ...[0000135c][0025cd5e][00001352] 51         push ecx      // push P
> ...[0000135d][0025cd5a][00001362] e840feffff call 000011a2 // call H
> Local Halt Decider: Infinite Recursion Detected Simulation Stopped
>
> H sees that P is calling the same function from the same machine address
> with identical parameters, twice in sequence. This is the infinite
> recursion (infinitely nested simulation) non-halting behavior pattern.

Nope, logic is ignoring the behavior of H.

[Ben]

olcott <No...@NoWhere.com> writes:

> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]

There are no arguments that can be passed to H so that H can correctly
report on the halting of the function call P(P). H falls at the first
hurdle: being able to decide the halting of specific function calls.

--
Ben.
"le génie humain a des limites, quand la bêtise humaine n’en a pas"
Alexandre Dumas (fils)

[olcott]

YOU IGNORED THIS PART

This proof can only be understood only by those having sufficient
technical competence in:

(a) software engineering - recognizing infinite recursion in C/x86

(b) the x86 programming language
(c) the C programming language and
(d) the details of how C is translated into x86 by the Microsoft C
compilers.

> For any program f that might determine if programs halt,
> a "pathological" program g, called with some input, can
> pass its own source and its input to f and then specifically
> do the opposite of what f predicts g will do. No f can exist
> that handles this case.
>
> "pass its own source" is NOT the same as compiling and running its own
> source as part of a simulation.

Passing the finite string of its own machine code is equivalent to
passing its own source.

>
> /Flibble

[olcott]

On 5/11/2022 7:17 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>
> There are no arguments that can be passed to H so that H can correctly
> report on the halting of the function call P(P). H falls at the first
> hurdle: being able to decide the halting of specific function calls.
>

A halt decider must only correctly report on the halt status of its
inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.

The HP proof tries to show an input that H gets wrong.
The proof no longer works on my H.

[Richard Damon]

On 5/11/22 8:29 PM, olcott wrote:
> On 5/11/2022 7:17 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>>
>> There are no arguments that can be passed to H so that H can correctly
>> report on the halting of the function call P(P).  H falls at the first
>> hurdle: being able to decide the halting of specific function calls.
>>
>
> A halt decider must only correctly report on the halt status of its
> inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.
>
> The HP proof tries to show an input that H gets wrong.
> The proof no longer works on my H.
>

Nope, a Halt Decider must report the Halting Status of the Machine the
input represents.

Thus P,P is ALWAYS the same computation for a Halting Decider.

The fact that your H and H1 give different answer just proves that they
aren't Halt Deciders.


Rmebmer xxx decider(foo) needs to give the mapping of xxx(foo) based on
the definition of xxx.

Halting(P,P) is defined as the halting of the computation P(P).

Thus anything that claims to be a Halting decider need to give the
answer of Halting(P,P) for H(P,P)

If you claim this isn't possbile because it isn't an input, just proves
that you can't make a Halting Decider.

This is like if we want to make an 'even decider' as a Turing Machine,
we can't give a Turing Machine an actual 'Number' but some
representation of a number.

In the same way the Halt Decider isn't given an ACTUAL program, but a
representation of it. (and it needs to be a representation of the ENTIRE
program, or it isn't decidable).

[Richard Damon]

And those that are see it to be the lie that it is.

I really don't think YOU understand the material to the level you claim
is needed.

>
>> For any program f that might determine if programs halt,
>> a "pathological" program g, called with some input, can
>> pass its own source and its input to f and then specifically
>> do the opposite of what f predicts g will do. No f can exist
>> that handles this case.
>>
>> "pass its own source" is NOT the same as compiling and running its own
>> source as part of a simulation.
>
> Passing the finite string of its own machine code is equivalent to
> passing its own source.

Only key is that you confuse the PROGRAM P with the SUBROUTINE P.

The finite string is NOT a definition of the actual compuation being
asked about, so you fail at step one.

>
>>
>> /Flibble
>>
>
>

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/11/2022 7:17 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>> There are no arguments that can be passed to H so that H can correctly
>> report on the halting of the function call P(P). H falls at the first
>> hurdle: being able to decide the halting of specific function calls.
>
> A halt decider must only correctly report on the halt status of its
> inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.

The "inputs" to H are two pointers. They have no halt status. What
H(X,Y) must correctly report on is the halting or otherwise of the
function call X(Y). Your H does not do the job it is supposed to do.

> The HP proof tries to show an input that H gets wrong.
> The proof no longer works on my H.

You are correct that the proof does not apply to your H. The proof is
about supposed halt deciders D such that D(X,Y) == true if and only if
X(Y) halts and false otherwise. Your H is not such a function -- you
can make it do what you like.

[olcott]

On 5/11/2022 8:10 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> On 5/11/2022 7:17 PM, Ben wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>>> There are no arguments that can be passed to H so that H can correctly
>>> report on the halting of the function call P(P). H falls at the first
>>> hurdle: being able to decide the halting of specific function calls.
>>
>> A halt decider must only correctly report on the halt status of its
>> inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.
>
> The "inputs" to H are two pointers. They have no halt status.

This is such a nutty thing to say when you already know that strings are
always passed in C as char* pointers.

I am passing strings of machine code as pointers, this is the normal
correct way to do this.

> What
> H(X,Y) must correctly report on is the halting or otherwise of the
> function call X(Y). Your H does not do the job it is supposed to do.
>

int sim(int N, int M)
{
return (N+M);
}

It turns out that this requirement is the same as requiring that
sum(3,4) must report on sum(5,6), thus making the requirement itself
incorrect.

The correct way of viewing the HP proof (and it is often stated this
way) is that there exists some inputs such that H cannot correctly
report their halt status.

>> The HP proof tries to show an input that H gets wrong.
>> The proof no longer works on my H.
>
> You are correct that the proof does not apply to your H. The proof is
> about supposed halt deciders D such that D(X,Y) == true if and only if
> X(Y) halts and false otherwise.

That is an incoherent requirement for some cases, thus incorrect for
these cases.

That incoherent requirement is based on the false assumption that the
behavior that the input to H(P,P) specifies is the always that exact
same behavior as P(P).

No one ever noticed that there are rare exceptions where this is not true.

> Your H is not such a function -- you
> can make it do what you like.
>


--

[Richard Damon]

On 5/11/22 10:29 PM, olcott wrote:
> On 5/11/2022 8:10 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/11/2022 7:17 PM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> Proof that H(P,P)==0 is correct [ refuting the halting problem
>>>>> proofs ]
>>>> There are no arguments that can be passed to H so that H can correctly
>>>> report on the halting of the function call P(P).  H falls at the first
>>>> hurdle: being able to decide the halting of specific function calls.
>>>
>>> A halt decider must only correctly report on the halt status of its
>>> inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.
>>
>> The "inputs" to H are two pointers.  They have no halt status.
>
> This is such a nutty thing to say when you already know that strings are
> always passed in C as char* pointers.
>
> I am passing strings of machine code as pointers, this is the normal
> correct way to do this.

But you violate the "bounds" of that string when you follow the call H
instruction.

>
>> What
>> H(X,Y) must correctly report on is the halting or otherwise of the
>> function call X(Y).  Your H does not do the job it is supposed to do.
>>
>
> int sim(int N, int M)
> {
>   return (N+M);
> }
>
> It turns out that this requirement is the same as requiring that
> sum(3,4) must report on sum(5,6), thus making the requirement itself
> incorrect.

Nope. UNSOUND Logic.

Sum is DEFINED to return the sum of the numbers given as its input.

H,(P,P) if it is a Halt Decider, is DEFINED to return and indication
about whether P(P) will Halt, read the DEFINITION.

If you disagree with the definition, you have a problem, because you
aren't allowed to change it, and still work on that same problem.

>
> The correct way of viewing the HP proof (and it is often stated this
> way) is that there exists some inputs such that H cannot correctly
> report their halt status.

Yes, which mean that NO H exist that can correctly report the correct
answer for ALL inputs.

>
>>> The HP proof tries to show an input that H gets wrong.
>>> The proof no longer works on my H.
>>
>> You are correct that the proof does not apply to your H.  The proof is
>> about supposed halt deciders D such that D(X,Y) == true if and only if
>> X(Y) halts and false otherwise.
>
> That is an incoherent requirement for some cases, thus incorrect for
> these cases.

No such thing as a incorrect requirement. Requirements ARE requirements.

What you actually mean is that some requirements are intrinsicly not
obtainable,

>
> That incoherent requirement is based on the false assumption that the
> behavior that the input to H(P,P) specifies is the always that exact
> same behavior as P(P).

Nope. You have the problem backwards.

xxx Deciders START with a defined mapping, and need to define how to
present that to the code to decide it.

Halting is about a Turing Machine and an Input to that machine.

A Halt Decider needs to define how to provide a computable
representation fpr that machine and input and have an algorithm to give
the right answer.

If there are machines/inputs that can't be properly expresses, that just
shows that the mapping is not computable, and no such decider exists.

IF we can't ask your H if P(P) will halt, then H fails to be a Halting
Decider,

>
> No one ever noticed that there are rare exceptions where this is not true.

Nope, there are no exceptions, you just don't understand what an xxx
decider is.

[Mr Flibble]

Indeed its own machine code is a representation of its own source code
so is valid to pass to a decider HOWEVER you ignored the second part
of my assertion:

"pass its own source" is NOT the same as compiling *AND RUNNING* its

own source as part of a simulation.

"AND RUNNING" means you cannot execute that machine code as part of a
simulation to correctly decide anything.

/Flibble

[Mr Flibble]

On Wed, 11 May 2022 19:23:45 -0500
olcott <No...@NoWhere.com> wrote:

(a) I have been a software developer/engineer since 1993 and am able to
recognize infinite recursion and additionally, and more importantly, a
lack of infinite recursion.
(b) I have been familiar with x86 assembly since before 1993
(c) I understand and have competence in both C and C++ (having used the
latter since 1993)
(d) I have written a compiler, have you?

/Flibble

[olcott]

My x86utm operating system operates exclusively on a compiled Microsoft
COFF object rile that has already been compiled.

> "AND RUNNING" means you cannot execute that machine code as part of a
> simulation to correctly decide anything.
>
> /Flibble
>

[olcott]

This has been disproven in that you did not see this:

>>>> H sees that P is calling the same function from the same machine
>>>> address with identical parameters, twice in sequence. This is the
>>>> infinite recursion (infinitely nested simulation) non-halting
>>>> behavior pattern.

> (b) I have been familiar with x86 assembly since before 1993
> (c) I understand and have competence in both C and C++ (having used the
> latter since 1993)
> (d) I have written a compiler, have you?
>
> /Flibble
>

[Mr Flibble]

On Thu, 12 May 2022 12:45:15 -0500

I am not talking about your braindead simulation, I am talking about
the halting problem proofs you are trying to refute: THEY DO NOT HAVE
AN INFINITE RECURSION.

/Flibble

[olcott]

My proofs prove that they do.
That you fail to comprehend this is no rebuttal at all.

[Mr Flibble]

On Thu, 12 May 2022 12:51:27 -0500

Only your simulation contains an infinite recursion due to a category
error ON YOUR PART. Your category error is proof that your
simulation-based proof is in error.

/Flibble

[olcott]

> PO's idea is to have a simulator with an infinite cycle detector.
> You would achieve this by modifying a UTM, so describing it as
> a "modified UTM", or "acts like a UTM until it detects an infinite
> cycle", is reasonable. And such a machine is a fairly powerful
> halt decider. Even if the infinite cycle detector isn't very
> sophisticated, it will still catch a large subset of non-halting
> machines.

The following simplifies the syntax for the definition of the Linz
Turing machine Ĥ.
There is no need for the infinite loop after H.qy because it is never
reached. The halting criteria has been adapted so that it applies to a
simulating halt decider (SHD).

Ĥ.q0 ⟨Ĥ⟩ ⊢* H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy
If the correctly simulated input ⟨Ĥ⟩ ⟨Ĥ⟩ to H would reach its own final
state of ⟨Ĥ.qy⟩ or ⟨Ĥ.qn⟩.

Ĥ.q0 ⟨Ĥ⟩ ⊢* H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn
If the correctly simulated input ⟨Ĥ⟩ ⟨Ĥ⟩ to H would never reach its own
final state of ⟨Ĥ.qy⟩ or ⟨Ĥ.qn⟩.

When Ĥ is applied to ⟨Ĥ⟩
Ĥ copies its input ⟨Ĥ0⟩ to ⟨Ĥ1⟩ then H simulates ⟨Ĥ0⟩ ⟨Ĥ1⟩

Then these steps would keep repeating: (unless their simulation is aborted)
Ĥ0 copies its input ⟨Ĥ1⟩ to ⟨Ĥ2⟩ then H0 simulates ⟨Ĥ1⟩ ⟨Ĥ2⟩
Ĥ1 copies its input ⟨Ĥ2⟩ to ⟨Ĥ3⟩ then H1 simulates ⟨Ĥ2⟩ ⟨Ĥ3⟩
Ĥ2 copies its input ⟨Ĥ3⟩ to ⟨Ĥ4⟩ then H2 simulates ⟨Ĥ3⟩ ⟨Ĥ4⟩...

Since we can see that the simulated input: ⟨Ĥ0⟩ to H would never reach
its own final state of ⟨Ĥ0.qy⟩ or ⟨Ĥ0.qn⟩ we know that it is non-halting.

Linz, Peter 1990. An Introduction to Formal Languages and Automata.
Lexington/Toronto: D. C. Heath and Company. (317-320)

[Mr Flibble]

On Thu, 12 May 2022 13:06:48 -0500

There is no point detecting infinite cycles as there is no infinite
recursion in the halting problem proofs you are trying to refute.

/Flibble

[Ben]

olcott <No...@NoWhere.com> writes:

> The halting criteria has been adapted so that

H is no longer a halt decider.

> it applies to a
> simulating halt decider (SHD).
>
> Ĥ.q0 ⟨Ĥ⟩ ⊢* H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy
> If the correctly simulated input ⟨Ĥ⟩ ⟨Ĥ⟩ to H would reach its own
> final state of ⟨Ĥ.qy⟩ or ⟨Ĥ.qn⟩.

This not Linz's Ĥ. Linz's H leads to a contradiction because of how H
and the "hat" construction are defined. Using a different "hat"
construction, and an "adapted" halt criterion, means you are not
addressing Linz's (or anyone's) proof. Why do you think anyone will
take any claims about your bogus seriously?

> Ĥ.q0 ⟨Ĥ⟩ ⊢* H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn
> If the correctly simulated input ⟨Ĥ⟩ ⟨Ĥ⟩ to H would never reach its
> own final state of ⟨Ĥ.qy⟩ or ⟨Ĥ.qn⟩.

A halt decider would have this simple behaviour:

J ⟨M⟩ s ⊢* J.qy if M applied to s halts, and
J ⟨M⟩ s ⊢* J.qn if M applied to s does not halt.

(I've changed the name because you are abusing H and Ĥ to refer to TMs
that do not meet Linz's specifications.)

Which, with the correct "hat" construction applied, results in

Ĵ.q0 ⟨Ĵ⟩ ⊢* J ⟨Ĵ⟩ ⟨Ĵ⟩ ⊢* J.qy ⊢* oo if J applied to ⟨Ĵ⟩ ⟨Ĵ⟩ halts, and
Ĵ.q0 ⟨Ĵ⟩ ⊢* J ⟨Ĵ⟩ ⟨Ĵ⟩ ⊢* J.qn if J applied to ⟨Ĵ⟩ ⟨Ĵ⟩ does not halt

which, as Linz says, is clearly nonsense. No TM can behave as Ĵ was
assumed to behave.

I bring this up only for the benefit of anyone who is still interested
in how the proof works. You stopped talking about the halting problem
and it's proofs some while ago, having failed to persuade anyone that
the wrong answer is the right one.

> Linz, Peter 1990. An Introduction to Formal Languages and
> Automata. Lexington/Toronto: D. C. Heath and Company. (317-320)

Bit of a nerve to cite Linz when you are ignoring his specification and
his proof!

[olcott]

My only point is that the input to embedded_H does specifies infinitely
nested simulation contradicting Flibble's claim that it does not, thus
my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.

[Richard Damon]

Except this pattern you are matching is flawed. The normal (and correct)
rule requires that no conditional be in the loop, and since H IS
conditional in its execution of P, you do not match a CORRECT infinite
recursion pattern. (That or H isn't conditional, at which point it NEVER
aborts, not even the top level copy, and thus fails to answer).

All you have "proven" is your own ignorance of the topic.

[Richard Damon]

You proofs are incorrect, and unsound, just as YOU are.

[Richard Damon]

Key words, "Unless their simulation is aborted", which, since H has been
show to actually abort the simulation, means that DOES happen, so H has
no proof that it was CORRECT to abort the simulation.

H can say that if it was programmed to NEVER abort, then it WOULD HAVE
BEEN correct to abort, but it didn't, so would have failed.

Once H is programmed to abort, it no longer has proof that it is correct
to do so.

You make the error of confounding the two possible versions of H, so
your reasoning is incorrect. H needs to decide on the copy of H that
actually exists, not the 'theoretical' alternative that might have, but
doesn't exist.

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/11/2022 8:10 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/11/2022 7:17 PM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>>>> There are no arguments that can be passed to H so that H can correctly
>>>> report on the halting of the function call P(P). H falls at the first
>>>> hurdle: being able to decide the halting of specific function calls.
>>>
>>> A halt decider must only correctly report on the halt status of its
>>> inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.
>>
>> The "inputs" to H are two pointers. They have no halt status.
>
> This is such a nutty thing to say when you already know that strings
> are always passed in C as char* pointers.

No pair of pointers has a halt status -- a fact I think you are aware of
since you appear to using this silly mantra to hide your key problem: H
gives the wrong answer as far as everyone but you is concerned.

In the context of H, what has a halt status is a function call. What H
should report is the whether calling the first pointer with the second
as its argument would or would not halt.

Your vague language about the "halt status of its inputs" is
deliberately designed to hide the truth: that H is not doing what it
should because H(P,P) == false even though P(P) halts.

> I am passing strings of machine code as pointers, this is the normal
> correct way to do this.

Maybe you are deliberately misusing the term string in order to draw the
argument way from the main problem: the "inputs" to H don't have a halt
status being simply data. What H should report is the whether calling
the first pointer with the second as its argument would or would not
halt. That's why H(P,P) == false is wrong. P(P) halts.

>> What
>> H(X,Y) must correctly report on is the halting or otherwise of the
>> function call X(Y). Your H does not do the job it is supposed to do.
>>
>

> int sum(int N, int M)

> {
> return (N+M);
> }
>
> It turns out that this requirement is the same as requiring that
> sum(3,4) must report on sum(5,6), thus making the requirement itself
> incorrect.

It does not "turn out" like that. Your new mantra -- that H reports in
the "halt status of its inputs" -- is just waffle to hide the plain fact
that H(P,P) == false is wrong because P(P) halts.

> The correct way of viewing the HP proof (and it is often stated this
> way) is that there exists some inputs such that H cannot correctly
> report their halt status.

That's not the correct view of the proof. That's exactly the incorrect
view that got you into trouble, and gets students into trouble everytime
this material is taught badly. Unfortunately I agree that it's a common
explanation, but that is no excuse. After 18 years you really should
know what the proof is saying.

> That incoherent requirement is based on the false assumption that the
> behavior that the input to H(P,P) specifies is the always that exact
> same behavior as P(P).

At least you accept that H can't do what the world wants it to.
Apparently you H does something no on cares about: determining the "halt
status if its inputs" which you are now crystal clear about is not the
same as the halt status of P(P).

What amazes me is how seriously you've lost track of what matters. Are
you not interested in the fact -- one you appear now to accept -- that
no function D(X,Y) can determine the halting of the function call X(Y)?
After all, as a programmer, you must know that's what you care about.
Even if your delusion is so profound that you are convinced that the
halting problems is about something else, you must see that this "other
halting problem", the one the world cares about is, unfortunately,
undecidable?

Since you are clear that no function can do what the world wants, what
else have you got to say? Can persuade anyone to care about what your H
is actually deciding? Not me.

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/12/2022 3:12 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> The halting criteria has been adapted so that
>>
>> H is no longer a halt decider.

<cut various errors>

> My only point is that the input to embedded_H does specifies
> infinitely nested simulation contradicting Flibble's claim that it
> does not, thus my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.

You made lots of point. Many of them wrong. I pointed out some of the
errors.

But since you are now unashamedly admitting to using an adapted
criterion for halting, is there any point in carrying on?

[Richard Damon]

The input to embedded_H only specifies infinitely nested simulations if
H is designed to NEVER abort its simulation of this input, and if this
is true, then H will not return an answer to H <H^> <H^> because it too
will get stuck in the same infinite nested simulation loop.

[olcott]

On 5/12/2022 5:54 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> On 5/11/2022 8:10 PM, Ben wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> On 5/11/2022 7:17 PM, Ben wrote:
>>>>> olcott <No...@NoWhere.com> writes:
>>>>>
>>>>>> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>>>>> There are no arguments that can be passed to H so that H can correctly
>>>>> report on the halting of the function call P(P). H falls at the first
>>>>> hurdle: being able to decide the halting of specific function calls.
>>>>
>>>> A halt decider must only correctly report on the halt status of its
>>>> inputs. H(P,P)==0 and H1(P,P)==1 both do that correctly.
>>>
>>> The "inputs" to H are two pointers. They have no halt status.
>>
>> This is such a nutty thing to say when you already know that strings
>> are always passed in C as char* pointers.
>
> No pair of pointers has a halt status -- a fact I think you are aware of
> since you appear to using this silly mantra to hide your key problem: H
> gives the wrong answer as far as everyone but you is concerned.
>
> In the context of H, what has a halt status is a function call. What H
> should report is the whether calling the first pointer with the second
> as its argument would or would not halt.
>
> Your vague language about the "halt status of its inputs" is
> deliberately designed to hide the truth: that H is not doing what it
> should because H(P,P) == false even though P(P) halts.
>

Being a learned-by-rote by-the-book person anything that goes against
the book must be wrong because the book establishes the conventional
view. This view is generally locked into academia by groupthink.
https://www.psychologytoday.com/us/basics/groupthink

It is objectively incorrect to say that a halt decider must base its
halt decision on anything other than the actual behavior actually
specified by its actual input such as H(P,P) reporting on P(P).

It is also objectively incorrect to assume that actual behavior actually
specified by the actual input to a halt decider will always be identical
to the direct execution of the corresponding computation. This was
previously unknown before my research.

This is where the faulty requirement came from.

[Mr Flibble]

You have a nerve, mate, being a Christian by-the-book (Bible) person
you also hold those negative traits. Christianity is the largest
groupthink of them all.

/Flibble

[olcott]

On 5/12/2022 5:58 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> On 5/12/2022 3:12 PM, Ben wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> The halting criteria has been adapted so that
>>>
>>> H is no longer a halt decider.
>
> <cut various errors>
>
>> My only point is that the input to embedded_H does specifies
>> infinitely nested simulation contradicting Flibble's claim that it
>> does not, thus my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.
>
> You made lots of point. Many of them wrong. I pointed out some of the
> errors.
>
> But since you are now unashamedly admitting to using an adapted
> criterion for halting, is there any point in carrying on?
>

I proved that the criteria for halting is objectively incorrect.
It requires a decider to base its decision on a non-input thus directly
contradicting the definition of a decider thus making the requirement
itself incorrect.

My H conclusively proves that it does correctly compute the mapping from
its input finite strings to its own reject state on the basis of the
actual behavior specified by these finite strings.

[olcott]

Not me. I believe that God intentionally put lots of bullshit in the
bible so that people could learn actual spiritual discernment.

> you also hold those negative traits. Christianity is the largest
> groupthink of them all.
>
> /Flibble
>

I am much more ruggedly individualist than anyone else that you have
ever even heard of.

I always hypothesize that everything that anyone has ever told me is
possibly incorrect until after I conclusively prove otherwise.

[Ben]

Being an ignorant-of-the-subject person, you don't know what you are
talking about.

> It is objectively incorrect to say that a halt decider must base its
> halt decision on anything other than the actual behavior actually
> specified by its actual input such as H(P,P) reporting on P(P).

You have entered the twilight zone. What is objectively correct is
based on the definition of the problem. If there are no "inputs" to H
that specify the call P(P) then H is useless. But at least you accept
that H can't report on P(P) correctly. You used to simply pretend that
the wrong answer was the right one.

I am stunned that you don't see that you can't avoid the problem. What
everyone wants -- a function D(X,Y) to determine if X(Y) would or would
not halt -- is not possible and you are admitting that fact as if it's
of no interest to you. You are wrong about why there is no such D, but
you agree that the problem can't be solved.

> It is also objectively incorrect to assume that actual behavior
> actually specified by the actual input to a halt decider will always
> be identical to the direct execution of the corresponding
> computation.

One way or another, we only care about the useful one. What the "actual
behavior actually specified by the actual input" is of no interest to
us if it does correspond the "direct execution of the corresponding
computation". We want something that tells up about direct function
calls.

> This was previously unknown before my research.

Don't be so pompous! Your new mantra is just a ruse to draw attention
away from the fact that you clearly accept that what everyone else has
been talking about can't be done.

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/12/2022 5:58 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/12/2022 3:12 PM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> The halting criteria has been adapted so that
>>>>
>>>> H is no longer a halt decider.
>> <cut various errors>
>>
>>> My only point is that the input to embedded_H does specifies
>>> infinitely nested simulation contradicting Flibble's claim that it
>>> does not, thus my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.
>> You made lots of point. Many of them wrong. I pointed out some of the
>> errors.
>> But since you are now unashamedly admitting to using an adapted
>> criterion for halting, is there any point in carrying on?
>
> I proved that the criteria for halting is objectively incorrect.

It can't be incorrect. It's a definition. And it's based on the most
natural notion: is the sequence of TM configurations finite or not.

> It requires a decider to base its decision on a non-input thus
> directly contradicting the definition of a decider thus making the
> requirement itself incorrect.

No, halting has to be based on the input. The input contains everything
that specifies the sequence of configurations, yet no algorithm exists
that can made the determination from the input alone.

[Richard Damon]

On 5/12/22 7:28 PM, olcott wrote:
> On 5/12/2022 5:58 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/12/2022 3:12 PM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> The halting criteria has been adapted so that
>>>>
>>>> H is no longer a halt decider.
>>
>> <cut various errors>
>>
>>> My only point is that the input to embedded_H does specifies
>>> infinitely nested simulation contradicting Flibble's claim that it
>>> does not, thus my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.
>>
>> You made lots of point.  Many of them wrong.  I pointed out some of the
>> errors.
>>
>> But since you are now unashamedly admitting to using an adapted
>> criterion for halting, is there any point in carrying on?
>>
>
> I proved that the criteria for halting is objectively incorrect.
> It requires a decider to base its decision on a non-input thus directly
> contradicting the definition of a decider thus making the requirement
> itself incorrect.

No, you proved that the halting function is not computable, which is
exactly the claim of the Halting Theorem that you are trying to disprove.

That an actual algorithmic H can't correctly handle the problem is
exactly what the Halting Problem is about.

Note, MOST deciders are working on problems that aren't directly stated
by their literal inputs, but by something the input represents, not is.

ANY time a Turing Machine is being asked a problem about math, is one
such case as the tape is a string of symbols, not "numbers". Yes, it is
a representation of the numbers, but it is JUST a representation of the
number, not the number itself.

By your logic, it is impossible to ask a Turing Machine if a "Number" is
even, only if the number of symbols on a tape is even or the string of
symbols on the tape is a representation of an even number.

This is EXACTLY the same as asking if the reprentation on the tape
represents a Halting Computation.

>
> My H conclusively proves that it does correctly compute the mapping from
> its input finite strings to its own reject state on the basis of the
> actual behavior specified by these finite strings.
>

But the mapping isn't that defined by the Halting problem, so it doesn't
say anything about that mapping.


You seem to be thinking of the Halting Problem as an exam question given
by a teacher to their students, a mere theoretical concept to just try
to solve.

You don't understand that the criteria of the Halting Problem has actual
utility, and came about out of basic problems trying to decide if
certain things are "solvable". Changing the critera means you aren't
actually asking the question that needs to be answered, so is a
worthless result.

[Richard Damon]

So, basicaally you are rejecting the idea that formal logic has rules.

That says that your whole arguement is irrelevant for any field that
says that there are rules that need to be followed.

Thus, you are showing that your proof doesn't actually apply to the
Halting Problem as you have just rejected the foundation that it is
built on.

Good luck getting anyone to publish your paper in anything but the most
esoteric philosophical journal that specializes in logic without rules.

[olcott]

All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
Paradox have been concrete proxies for my study of the philosophical
foundation of analytical truth.

I examine these things as they fit into the whole grande scheme of the
nature of truth itself.

It turns out that all "undecidable" problems are only "undecidable"
because they have very well hidden incoherence.

Taking a form such as this: Provide a natural number N such that N > 7
and N < 3, the answer must be a natural number.

When the definition of the halting problem directly contradicts the
definition of a computer science decider, then the definition of the
halting problem is proven to be incorrect.

[olcott]

On 5/12/2022 7:40 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> On 5/12/2022 5:58 PM, Ben wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> On 5/12/2022 3:12 PM, Ben wrote:
>>>>> olcott <No...@NoWhere.com> writes:
>>>>>
>>>>>> The halting criteria has been adapted so that
>>>>>
>>>>> H is no longer a halt decider.
>>> <cut various errors>
>>>
>>>> My only point is that the input to embedded_H does specifies
>>>> infinitely nested simulation contradicting Flibble's claim that it
>>>> does not, thus my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.
>>> You made lots of point. Many of them wrong. I pointed out some of the
>>> errors.
>>> But since you are now unashamedly admitting to using an adapted
>>> criterion for halting, is there any point in carrying on?
>>
>> I proved that the criteria for halting is objectively incorrect.
>
> It can't be incorrect. It's a definition. And it's based on the most
> natural notion: is the sequence of TM configurations finite or not.

It is an objectively verifiable fact that the sequence of configurations
specified by the input to H(P,P) is not the same as the one specified by
P(P).

When you have two definitions in computer science that directly
contradict each other what do you do? Toss out at least one of them.

>> It requires a decider to base its decision on a non-input thus
>> directly contradicting the definition of a decider thus making the
>> requirement itself incorrect.
>
> No, halting has to be based on the input.

The H(P,P)==0 is correct.

> The input contains everything
> that specifies the sequence of configurations,

It is an objectively verifiable fact that the sequence of configurations
specified by the input to H(P,P) is not the same as the one specified by
P(P).

> yet no algorithm exists
> that can made the determination from the input alone.
>

H(P,P)==0 and H1(P,P)==1 are both provably correct.

[Richard Damon]

Nope, the problems do NOT state such an impossibility.

For example, machine M appied to inut w WILL Halt or Not, so its Halting
property is a Truth Bearer, and thus, the Definition of the Halting
Problem is NOT "incorrect"

The issue is that no "Computation" can always be able to determine this
property, because we are able to make a machine that can confound any
other machine that is trying to do that determination.

This doesn't make the problem contradictory, just uncomptable.

Only by adding a rule that the only things are provable can be true, do
you run into the contradiction, which is what proves that such a rule is
incorrect, at least in any logic system capable of describing such
computations.

All you have proved is that you don't understand this level of subtlty
in logic, that different fields can work under somewhat different "rules".

Some system, which limit the compexity of what operations you can
perform on statements, can include rules like for a statement to be a
truthbearer, it needs to be provable or refutable. While others, because
they allow for higher order logical operations, lose the ability for
constraints like that.

[Richard Damon]

Then H is not implementing the Halting Mapping, so is NOT a Halt Decider.

>
>> yet no algorithm exists
>> that can made the determination from the input alone.
>>
>
> H(P,P)==0 and H1(P,P)==1 are both provably correct.
>
>

Only if H and H1 are not Halt Deciders, which has been proven a long
time ago.

[Ben]

olcott <No...@NoWhere.com> writes:

> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
> Paradox have been concrete proxies for my study of the philosophical
> foundation of analytical truth.

Why have you not had anything published? Everyone here knows why, but
what's your opinion?

You can't publish H(P,P) == false even though P(P) halts, but I leave
the rest of you grand claims to others.

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/12/2022 7:40 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/12/2022 5:58 PM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> On 5/12/2022 3:12 PM, Ben wrote:
>>>>>> olcott <No...@NoWhere.com> writes:
>>>>>>
>>>>>>> The halting criteria has been adapted so that
>>>>>>
>>>>>> H is no longer a halt decider.
>>>> <cut various errors>
>>>>
>>>>> My only point is that the input to embedded_H does specifies
>>>>> infinitely nested simulation contradicting Flibble's claim that it
>>>>> does not, thus my H(P,P) is equivalent to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩.
>>>> You made lots of point. Many of them wrong. I pointed out some of the
>>>> errors.
>>>> But since you are now unashamedly admitting to using an adapted
>>>> criterion for halting, is there any point in carrying on?
>>>
>>> I proved that the criteria for halting is objectively incorrect.
>> It can't be incorrect. It's a definition. And it's based on the most
>> natural notion: is the sequence of TM configurations finite or not.
>
> It is an objectively verifiable fact that the sequence of
> configurations specified by the input to H(P,P) is not the same as the
> one specified by P(P).

Who cares? Only you. You accept, now, that you can't write a D that
does what everyone but you wants: D(X,Y) == true if and only if X(Y)
halts and false otherwise.

You are done with halting now because you are not making any claims to
have anything to say about what the world calls halting.

> When you have two definitions in computer science that directly
> contradict each other what do you do? Toss out at least one of them.

No. Whatever your H is deciding might be interesting. I don't think
so, but there's no reason to toss it out just because it does not decide
halting.

[Mikko]

On 2022-05-11 18:07:16 +0000, olcott said:

> This proof can only be understood only by those having sufficient
> technical competence in:
> (a) software engineering (recognizing infinite recursion in C and x86 code)
> (b) the x86 programming language
> (c) the C programming language and
> (d) the details of how C is translated into x86 by the Microsoft C compilers.

Then it is not a proof. A real proof can be verified by anyone who
knows logic or mathematics.

Mikko

[Mikko]

On 2022-05-13 01:25:37 +0000, olcott said:

> Taking a form such as this: Provide a natural number N such that N > 7
> and N < 3, the answer must be a natural number.

Or a proof that no such natural number exists.

> When the definition of the halting problem directly contradicts the
> definition of a computer science decider, then the definition of the
> halting problem is proven to be incorrect.

The definition of the halting problem cannot contradict the definition
of decider. It can only contradict another definition of halting problem.

Mikko

[olcott]

On 5/13/2022 8:11 AM, Mikko wrote:
> On 2022-05-13 01:25:37 +0000, olcott said:
>
>> Taking a form such as this: Provide a natural number N such that N > 7
>> and N < 3, the answer must be a natural number.
>
> Or a proof that no such natural number exists.
>

The answer is restricted to elements of the set of natural numbers hence
making the problem undecidable through Flibble's category error.

My first example of Flibble's category error in 2004 (I didn't call it
that at that time) is the question: What time is it (yes or no)?

>> When the definition of the halting problem directly contradicts the
>> definition of a computer science decider, then the definition of the
>> halting problem is proven to be incorrect.
>
> The definition of the halting problem cannot contradict the definition
> of decider.

Everyone here is requiring a halt decider to break the rule that it only
computes the mapping from its inputs. They insist that the definition of
the halting problem requires a halt decider to compute the mapping from
non inputs.

H(P,P)==0 is correct even though P(P) halts because the correct
simulation of the input to H(P,P) specifies an entirely different
sequence of configurations that the exuecution of P(P).

> It can only contradict another definition of halting problem.
>
> Mikko
>

[olcott]

On 5/13/2022 6:05 AM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
>> Paradox have been concrete proxies for my study of the philosophical
>> foundation of analytical truth.
>
> Why have you not had anything published? Everyone here knows why, but
> what's your opinion?
>

I have to conclusively prove my point concretely such the every single
detail of my reasoning can be verified as factually correct before
people will understand that I have corrected errors in some of the
aspects of the basic foundations of logic.

Actual fully operational code refuting the HP proof works best for this
because the Gödel, Tarski, and the LP have hidden semantic gaps that are
defined as non-existent by the conventional terms of their art so they
cannot be seen when using these terms of the art.

The errors in the foundations of logic can be summed up very simply.
Whenever only truth preserving operations are applied to expressions of
language known to be true then a true conclusion is derived.

I also correct the definition of validity:

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. https://iep.utm.edu/val-snd/

If the Moon is made of green cheese then all dogs are cats is valid and
even though premises and conclusion are semantically unrelated.

Here is my correction to that issue:
A deductive argument is said to be valid if and only if it takes a form
that its conclusion is a necessary consequence of all of its premises.

The semantically unrelated premises and conclusion is not possible with
syllogisms. https://en.wikipedia.org/wiki/Syllogism#Basic_structure

Because syllogisms are comprised of
https://en.wikipedia.org/wiki/Categorical_proposition

> You can't publish H(P,P) == false even though P(P) halts, but I leave
> the rest of you grand claims to others.
>


--

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/13/2022 6:05 AM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
>>> Paradox have been concrete proxies for my study of the philosophical
>>> foundation of analytical truth.
>>
>> Why have you not had anything published? Everyone here knows why, but
>> what's your opinion?
>
> I have to conclusively prove my point concretely such the every single
> detail of my reasoning can be verified as factually correct before
> people will understand that I have corrected errors in some of the
> aspects of the basic foundations of logic.

Hmm.. but it's "dead obvious", isn't it?

[wij]

On Thursday, 12 May 2022 at 02:07:26 UTC+8, olcott wrote:
> Proof that H(P,P)==0 is correct [ refuting the halting problem proofs ]
>

> The x86utm operating system was created so that every detail of the
> conventional halting problem counter example could be fully specified in
> C/x86.
>
> In computability theory, the halting problem is the
> problem of determining, from a description of an
> arbitrary computer program and an input, whether the
> program will finish running, or continue to run forever...
>
> For any program f that might determine if programs halt,
> a "pathological" program g, called with some input, can
> pass its own source and its input to f and then specifically
> do the opposite of what f predicts g will do. No f can exist
> that handles this case. https://en.wikipedia.org/wiki/Halting_problem
>
> This exact same relationship of f(g,g) was created as H(P,P), shown below.
>
> This is the overview of the method for proving that this analysis is
> correct:
> (a) Verify that the execution trace of P by H is correct by comparing
> this execution trace to the ax86 source-code of P.
>
> (b) Verify that this execution trace shows that P is stuck in infinitely
> nested simulation (a non-halting behavior).
>

> This proof can only be understood only by those having sufficient
> technical competence in:
> (a) software engineering (recognizing infinite recursion in C and x86 code)
> (b) the x86 programming language
> (c) the C programming language and
> (d) the details of how C is translated into x86 by the Microsoft C
> compilers.
>

> --
> Copyright 2022 Pete Olcott
>
> "Talent hits a target no one else can hit;
> Genius hits a target no one else can see."
> Arthur Schopenhauer

According to GUR https://groups.google.com/g/comp.theory/c/_tbCYyMox9M
Your POOH is incorrect, totally garbage, nonsense.

[olcott]

On 5/13/2022 2:06 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> On 5/13/2022 6:05 AM, Ben wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
>>>> Paradox have been concrete proxies for my study of the philosophical
>>>> foundation of analytical truth.
>>>
>>> Why have you not had anything published? Everyone here knows why, but
>>> what's your opinion?
>>
>> I have to conclusively prove my point concretely such the every single
>> detail of my reasoning can be verified as factually correct before
>> people will understand that I have corrected errors in some of the
>> aspects of the basic foundations of logic.
>
> Hmm.. but it's "dead obvious", isn't it?
>

It has been dead obvious that H(P,P)==0 is the correct halt status for
the input to H(P,P) on the basis of the actual behavior that this input
actually specifies.

This has been dead obvious on this basis for at least six months, yet
people very persistently insisted on simply ignoring the easily
verifiable facts for this whole six month period.

[Richard Damon]

On 5/13/22 3:24 PM, olcott wrote:
> On 5/13/2022 2:06 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/13/2022 6:05 AM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
>>>>> Paradox have been concrete proxies for my study of the philosophical
>>>>> foundation of analytical truth.
>>>>
>>>> Why have you not had anything published?  Everyone here knows why, but
>>>> what's your opinion?
>>>
>>> I have to conclusively prove my point concretely such the every single
>>> detail of my reasoning can be verified as factually correct before
>>> people will understand that I have corrected errors in some of the
>>> aspects of the basic foundations of logic.
>>
>> Hmm.. but it's "dead obvious", isn't it?
>>
>
> It has been dead obvious that H(P,P)==0 is the correct halt status for
> the input to H(P,P) on the basis of the actual behavior that this input
> actually specifies.
>
> This has been dead obvious on this basis for at least six months, yet
> people very persistently insisted on simply ignoring the easily
> verifiable facts for this whole six month period.
>

Nope, since BY THE PROBLEM STATEMENT of the Halting Problem, the "actual
behavior" of the input to H applied to <H^> <H^> is DEFINED to be the
behavior of H^ applied to <H^>.

If you claim it means anything else, you aren't working on the Halting
Problem.

If you claim that the Halting Problem can't ask H that question because
of "something", then that is just PROVING the Halting Theorem, as if you
can't even ask the question, then you can't expect there to be an H that
can give the right answer. The mapping being "Not Computatable" is a
valid answer, and just proves the Theorem.

All you have actually proven is that you don't understand the problem
and likely don't even understand how formal logic works.

The fact that you admit that you are changing core foundationally
premises of logic, means you are vastly premature to be talking about
the Halting Problem, you first need to go through and prove the logical
foundations of EVERYTHING it is built on.

GOOD LUCK.

[olcott]

The ultimate measure superseding and overruling every other measure is
the actual behavior of the actual input as demonstrated by a correct
simulation of this input by the simulating halt decider.

[Dennis Bush]

And your H doesn't perform a correct simulation as has been described many times. If the answer H gives doesn't match the defined mapping:

H applied to <H^> <H^> reports halting if and only if H^ applied to <H^> halts, and
H applied to <H^> <H^> reports non-halting if and only if H^ applied to <H^> does not halt

Which it doesn't, then it is by definition wrong.

[wij]

Where is the actual POOH? We only hear you lie all day long.

[olcott]

That the execution trace provided by H(P,P) exactly matches the behavior
that the x86 source-code of P specifies conclusively proves that the
simulation of the input to H(P,P) is correct.

How much longer are you going to deny this empirically proven fact?
How much longer are you going to deny this empirically proven fact?
How much longer are you going to deny this empirically proven fact?
How much longer are you going to deny this empirically proven fact?
How much longer are you going to deny this empirically proven fact?

Number_of_User_Instructions(1)
Number of Instructions Executed(15892)

[Mr Flibble]

On Fri, 13 May 2022 15:38:23 -0500
olcott <No...@NoWhere.com> wrote:
> H sees that P is calling the same function from the same machine
> address with identical parameters, twice in sequence. This is the
> infinite recursion (infinitely nested simulation) non-halting
> behavior pattern.

An infinite recursion that only exists in your simulation and not in
the proofs you are attempting to refute. Your simulation is based on a
category error and is thus invalid.

Give it up and do something useful with the rest of your life.

/Flibble

[Richard Damon]

THen H is PROVEN to not be a Halt Decider, because the Halting Mapping
is defined differently.

If the definition of H doesn't match the requirements of the problem,
then it just fails to be an aswer to the problem.

You lack of understanding of this just proves your own level (total lack
of) competence in this area.

FAIL.

[olcott]

Tarski makes a similar mistake when he concludes that True() is not a
definable predicate entirely on the basis that he cannot prove that the
liar paradox is true. It never occurred to him that the liar paradox is
simply untrue.

That the definition of the halting problem criteria (in some rare cases)
directly contradicts the definition of a computer science decider that
requires all deciders to compute the mapping from their inputs
conclusively proves that the definition of the halting problem criteria
is incorrect in these (previously undiscovered) rare cases.

[Richard Damon]

You are just proving that you don't know what you are talking about.
Definitions can not be 'incorrect', as they are DEFINITIONS. They can be
non-sensical or inconsistent, but the definition of Halting doesn't have
that problem, any computation will either Halt or Not.

Maybe, it is non-sensical to think you can ask a Turing Machine to
compute the Halting Mapping, but that just means the answer to the
Halting Problem is that NO, there does not exist such a machine. It does
NOT mean that the machine can be correct giving some other answer.

[olcott]

That is a naive thing to say.
This means that a pair of contradictory defininitions within the same
system would both be correct. This is simply not the way that truth
actually works.

[Ben]

olcott <No...@NoWhere.com> writes:

> On 5/13/2022 2:06 PM, Ben wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> On 5/13/2022 6:05 AM, Ben wrote:
>>>> olcott <No...@NoWhere.com> writes:
>>>>
>>>>> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
>>>>> Paradox have been concrete proxies for my study of the philosophical
>>>>> foundation of analytical truth.
>>>>
>>>> Why have you not had anything published? Everyone here knows why, but
>>>> what's your opinion?
>>>
>>> I have to conclusively prove my point concretely such the every single
>>> detail of my reasoning can be verified as factually correct before
>>> people will understand that I have corrected errors in some of the
>>> aspects of the basic foundations of logic.
>> Hmm.. but it's "dead obvious", isn't it?
>
> It has been dead obvious that H(P,P)==0 is the correct halt status for
> the input to H(P,P) on the basis of the actual behavior that this
> input actually specifies.

But not obvious enough to get it published! Come, now. You know its
nonsense.

[olcott]

On 5/13/2022 5:46 PM, Ben wrote:
> olcott <No...@NoWhere.com> writes:
>
>> On 5/13/2022 2:06 PM, Ben wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> On 5/13/2022 6:05 AM, Ben wrote:
>>>>> olcott <No...@NoWhere.com> writes:
>>>>>
>>>>>> All of my studies of Gödel 1931, Tarski 1936, the HP and the Liar
>>>>>> Paradox have been concrete proxies for my study of the philosophical
>>>>>> foundation of analytical truth.
>>>>>
>>>>> Why have you not had anything published? Everyone here knows why, but
>>>>> what's your opinion?
>>>>
>>>> I have to conclusively prove my point concretely such the every single
>>>> detail of my reasoning can be verified as factually correct before
>>>> people will understand that I have corrected errors in some of the
>>>> aspects of the basic foundations of logic.
>>> Hmm.. but it's "dead obvious", isn't it?
>>
>> It has been dead obvious that H(P,P)==0 is the correct halt status for
>> the input to H(P,P) on the basis of the actual behavior that this
>> input actually specifies.
>
> But not obvious enough to get it published! Come, now. You know its
> nonsense.
>

It has been empirically proven that H(P,P)==0 is the correct halt status
for the input to H(P,P) on the basis of the empirically proven correct
simulation of the input to H(P,P) that H derives.

Not only must a halt decider compute the mapping from its inputs it must
compute the mapping only on the basis of what its inputs explicitly
specify otherwise it is not a computation (pure function of its inputs)
at all.

[Richard Damon]

Right, they both ARE correct, and make the system inconsistent. That is
the meaning of the word DEFINITION. (and an inconsistent systems tend to
make a hash about 'truth' in that system, as you tend to be able to
prove and disprove a lot in such a system).

Now, a given definition might make a system not model well the actual
system that it is supposed to model. But that doesn't make the
definition incorrect in the system, but makes the system a bad model.

We might talk about that definition as being 'incorrect', but
technically, it IS correct in that system and makes the system a bad model.

[olcott]

Inconsistent is another word for incorrect, thus in any system of
correct reasoning there can be no contradictory definitions.

> That is
> the meaning of the word DEFINITION. (and an inconsistent systems tend to
> make a hash about 'truth' in that system, as you tend to be able to
> prove and disprove a lot in such a system).
>
> Now, a given definition might make a system not model well the actual
> system that it is supposed to model. But that doesn't make the
> definition incorrect in the system, but makes the system a bad model.
>
> We might talk about that definition as being 'incorrect', but
> technically, it IS correct in that system and makes the system a bad model.

[Richard Damon]

STILL proving you don't know what you are talking about.

You have proved no such thing, since H does not do a CORRECT simulation
(which will never abort, since machines don't just stop in the middle)

You also prove you still don't understand what a computation is.

FAIL.

[olcott]

simulation of the input to H(P,P) that H derives up to the point where H
has proven that this correct simulation would never stop running.

>
> You also prove you still don't understand what a computation is.
>
> FAIL.
>

[Richard Damon]

Nopw, not the same definitions by the normal definitions.

If your going to play Humpty Dumpty then you are just admitting that you
have lost already, because you are admitting that your goal isn't to
find truth but to create obfuscation.

I guess just want you systems to be defined that we can't tell it they
are correct at all (if more than a toy).

Actually PROVING that a system is not inconsistent within that system is
beyond the reach of most systems, and can only be done in very finite
systems.

If that is all you logic is good for, you are setting your self up to be
ignored.

[olcott]

I am referring to a system of correct reasoning and showing how symbolic
logic diverges from this.

> If your going to play Humpty Dumpty then you are just admitting that you
> have lost already, because you are admitting that your goal isn't to
> find truth but to create obfuscation.
>
> I guess just want you systems to be defined that we can't tell it they
> are correct at all (if more than a toy).
>
> Actually PROVING that a system is not inconsistent within that system is
> beyond the reach of most systems, and can only be done in very finite
> systems.
>
> If that is all you logic is good for, you are setting your self up to be
> ignored.
>
>>
>>
>>> That is the meaning of the word DEFINITION. (and an inconsistent
>>> systems tend to make a hash about 'truth' in that system, as you tend
>>> to be able to prove and disprove a lot in such a system).
>>>
>>> Now, a given definition might make a system not model well the actual
>>> system that it is supposed to model. But that doesn't make the
>>> definition incorrect in the system, but makes the system a bad model.
>>>
>>> We might talk about that definition as being 'incorrect', but
>>> technically, it IS correct in that system and makes the system a bad
>>> model.
>>
>>
>

[Ben]

But it not the correct halt status for P(P) which is what the world
wants and why you know you'll never get this silly idea published.

[Richard Damon]

IF you aren't talking about Formal Logic and the rules for it, then you
are talking in the wrong place. Note, you don't get to change the rules.

If you really want to try to turn the whole field of logic on its head,
you really need to be working in the fields that deal with the core
basics of how logic works.

Comutation Theory and the Halting Problem is NOT where to try to change
those things. The fact that you even think it is tends to be a pretty
good sign that you don't really understand what you are talking about.

My guess is that if you actually had an idea of that level, you needed
to start decades ago in the right places for THAT sort of discussion.

As it is, you claim to have very limited time, and have ruined any
reputation that you might have hoped to have, so you are proably doomed
to fail at establishing any sort of new class of logic based on your ideas.

[Richard Damon]

No, it has been proven that H can't possibly simulate the input to a
final state, so you have proved that H can't prove its input Halts. You
haven't proved that it doesn't halt, at least not by the REAL definition
of Halting (which you aren't allowed to change).

H has NOT proven that the input won't halt, only that H can't prove that
the input halts.

H has used UNSOUND logic to conclude that the input doesn't halt, as it
assumes that the copy of H it is simulating won't abort its simulation
of its input, when this is NOT true (at least if H is a computation).
Thus H HASN'T actually proved the input is non-halting and thus makes an
error and gets the wrong answer.

[olcott]

That the definition of the halting problem criteria (in some rare cases)
directly contradicts the definition of a computer science decider that
requires all deciders to compute the mapping from their inputs
conclusively proves that the definition of the halting problem criteria
is incorrect in these (previously undiscovered) rare cases.

It has been empirically proven that H(P,P)==0 is the correct halt status
for the input to H(P,P) on the basis of the empirically proven correct

simulation of the input to H(P,P) that H derives up to the point where H
has proven that this correct simulation would never stop running.

It has been empirically proven that H1(P,P)==1 is the correct halt
status for the input to H1(P,P) on the basis of the empirically proven
correct simulation of the input to H1(P,P) that H1 derives halts.

[Ben]

There's only one -- a computation either halts or it does not halt, and
the is no ambiguity about what that means. (It can be made precise, but
only using a formal model of computation and you don't know any of
those.)

The function call P(P) unambiguously halts. Your H can not tell us this
fact. By no longer talking about actual halting, you are, in effect,
agreeing that no D can exist such that D(X,Y) == true if and only if
X(Y) halts and false otherwise.

[olcott]

When the rules of logic prove to be inconsistent then that proves that
they do not correspond to correct reasoning, thus making them incorrect.

>
> If you really want to try to turn the whole field of logic on its head,
> you really need to be working in the fields that deal with the core
> basics of how logic works.
>

This issue is the philosophical foundation of logic is inconsistent.

> Comutation Theory and the Halting Problem is NOT where to try to change
> those things. The fact that you even think it is tends to be a pretty
> good sign that you don't really understand what you are talking about.
>
> My guess is that if you actually had an idea of that level, you needed
> to start decades ago in the right places for THAT sort of discussion.
>

I started in 1997. The HP is the only concrete example where all of the
details of the error in the philosophical foundation of logic can be
shown in all of its complete detail as actually fully operational code.

Every other way of proving my point has gaps in reasoning that have been
hard-wired into the conventional definitions of terms of the art.

When I try to correct these errors people simply assume that I do not
correctly know the proper definition.

> As it is, you claim to have very limited time, and have ruined any
> reputation that you might have hoped to have, so you are proably doomed
> to fail at establishing any sort of new class of logic based on your ideas.
>

[olcott]

Learned-by-rote by-the-book people can't get past the fact that the book
really cannot be relied upon as infallible because it is their only basis.

[Ben]

Not-learned-by-any-method people spout nonsense on Usenet all the time.
They don't get papers published. They don't contribute the sum total of
human knowledge.

[Richard Damon]

The rules of logic ARE the rules of logic. PERIOD.

If you disagree with what the logic says, fine, you reject those fields
of logic as useful. Others disagree.

Most others will say that YOU are incorrect.

>
>>
>> If you really want to try to turn the whole field of logic on its
>> head, you really need to be working in the fields that deal with the
>> core basics of how logic works.
>>
>
> This issue is the philosophical foundation of logic is inconsistent.

But it IS the foundation of logic.

If you want to try to come up with something better, go ahead, work on it.

>
>> Comutation Theory and the Halting Problem is NOT where to try to
>> change those things. The fact that you even think it is tends to be a
>> pretty good sign that you don't really understand what you are talking
>> about.
>>
>> My guess is that if you actually had an idea of that level, you needed
>> to start decades ago in the right places for THAT sort of discussion.
>>
>
> I started in 1997. The HP is the only concrete example where all of the
> details of the error in the philosophical foundation of logic can be
> shown in all of its complete detail as actually fully operational code.

Then you don't understand your logic well enough.

The Halting Problems is likely THOUSANDS of steps removed from the
foundation assumptions of the Formal Logic of the system it is built on.

>
> Every other way of proving my point has gaps in reasoning that have been
> hard-wired into the conventional definitions of terms of the art.

I think it shows that there are gaps in YOUR understanding of the issue.
Most of the stuff that you have tried to point out seems to be stuff
that has been out there for most of a century, and the errors in it found.

You want all truth to be provable, it has been shown that this can only
hold in the simpler logic systems. by NECESSITY, more complicated logic
operations expand the region of "Truth" faster than the region of
"Provable", so we get stuff that can be true, but not proven, and
incompleteness of the system.

It turns out that most of the very useful logic systems have crossed
that line, so have decided that the greater reasoning power is worth
being incomplete.

>
> When I try to correct these errors people simply assume that I do not
> correctly know the proper definition.

Which you are proved that you don't know.

[André G. Isaak]

On 2022-05-13 18:20, olcott wrote:

> When the rules of logic prove to be inconsistent then that proves that
> they do not correspond to correct reasoning, thus making them incorrect.

But you haven't identified any rules of logic which are inconsistent.

André


--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

[Richard Damon]

On 5/13/22 9:03 PM, André G. Isaak wrote:
> On 2022-05-13 18:20, olcott wrote:
>
>> When the rules of logic prove to be inconsistent then that proves that
>> they do not correspond to correct reasoning, thus making them incorrect.
>
> But you haven't identified any rules of logic which are inconsistent.
>
> André
>
>

They are inconsistent with HIS idea that Truth must be provable, Which
can't be Proved so isn't True in a system that wants to use it.

It can only be an Axiom, but it has been proved inconsistent with most
logic system that are complicated enough, so adding it distroys the
logic system.

This shows that it is HIS idea that is inconsistent and must be rejected
for not being correct reasoning.

Of course, that logc will just blow the circuit breakers in his head.

[olcott]

On 5/13/2022 8:03 PM, André G. Isaak wrote:
> On 2022-05-13 18:20, olcott wrote:
>
>> When the rules of logic prove to be inconsistent then that proves that
>> they do not correspond to correct reasoning, thus making them incorrect.
>
> But you haven't identified any rules of logic which are inconsistent.
>
> André

I have not articulated this clearly enough yet.

[Mikko]

On 2022-05-13 16:15:35 +0000, olcott said:

> On 5/13/2022 8:11 AM, Mikko wrote:
>> On 2022-05-13 01:25:37 +0000, olcott said:
>>
>>> Taking a form such as this: Provide a natural number N such that N > 7
>>> and N < 3, the answer must be a natural number.
>>
>> Or a proof that no such natural number exists.
>>
>
> The answer is restricted to elements of the set of natural numbers
> hence making the problem undecidable through Flibble's category error.

Undecidable does not apply as the question is not about a claim but
about a number. But no number satisfies all requirements. A common
convention with problems of this type is that the clause "or prove
that no solution exists" is omitted but understood to be a part of
the problem.

Mikko

[Mikko]

On 2022-05-13 22:57:47 +0000, olcott said:

> It has been empirically proven that H(P,P)==0 is the correct halt
> status for the input to H(P,P) on the basis of the empirically proven
> correct simulation of the input to H(P,P) that H derives.

There is a category error in that statement. Mathematical truths do not
refer to empirical facts so they cannot be empirically proven. Whether
H(P,P) == 0 is true or false is a mathematical question so it cannot be
determined empirically.

Mikko

[olcott]

In programming language theory and proof theory, the Curry–Howard
correspondence (also known as the Curry–Howard isomorphism or
equivalence, or the proofs-as-programs and propositions- or
formulae-as-types interpretation) is the direct relationship between
computer programs and mathematical proofs.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

[Mikko]

On 2022-05-14 09:28:20 +0000, olcott said:

> On 5/14/2022 3:45 AM, Mikko wrote:
>> On 2022-05-13 22:57:47 +0000, olcott said:
>>
>>> It has been empirically proven that H(P,P)==0 is the correct halt
>>> status for the input to H(P,P) on the basis of the empirically proven
>>> correct simulation of the input to H(P,P) that H derives.
>>
>> There is a category error in that statement. Mathematical truths do not
>> refer to empirical facts so they cannot be empirically proven. Whether
>> H(P,P) == 0 is true or false is a mathematical question so it cannot be
>> determined empirically.
>>
>> Mikko
>>
>
> In programming language theory and proof theory, the Curry–Howard
> correspondence (also known as the Curry–Howard isomorphism or
> equivalence, or the proofs-as-programs and propositions- or
> formulae-as-types interpretation) is the direct relationship between
> computer programs and mathematical proofs.
> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

That is a mathematical equivalence between mathematical structures.
Nothing empirical there.

Mikko

[olcott]

proofs-as-programs and programs do run, thus the mapping between the
math and empirical validation of this math. C is a formal language of a
formal system.

[Mikko]

On 2022-05-14 13:53:29 +0000, olcott said:

> On 5/14/2022 7:55 AM, Mikko wrote:
>> On 2022-05-14 09:28:20 +0000, olcott said:
>>
>>> On 5/14/2022 3:45 AM, Mikko wrote:
>>>> On 2022-05-13 22:57:47 +0000, olcott said:
>>>>
>>>>> It has been empirically proven that H(P,P)==0 is the correct halt
>>>>> status for the input to H(P,P) on the basis of the empirically proven
>>>>> correct simulation of the input to H(P,P) that H derives.
>>>>
>>>> There is a category error in that statement. Mathematical truths do not
>>>> refer to empirical facts so they cannot be empirically proven. Whether
>>>> H(P,P) == 0 is true or false is a mathematical question so it cannot be
>>>> determined empirically.
>>>>
>>>> Mikko
>>>>
>>>
>>> In programming language theory and proof theory, the Curry–Howard
>>> correspondence (also known as the Curry–Howard isomorphism or
>>> equivalence, or the proofs-as-programs and propositions- or
>>> formulae-as-types interpretation) is the direct relationship between
>>> computer programs and mathematical proofs.
>>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>>
>> That is a mathematical equivalence between mathematical structures.
>> Nothing empirical there.
>>
>> Mikko
>>
>
> proofs-as-programs and programs do run, thus the mapping between the
> math and empirical validation of this math.

Even when the same text can be interpreted as a proof or as a program,
those interpretaions involve different semantics. Therefore the execution
does not validate anything beyond the syntax.

> C is a formal language of a formal system.

No, it is not. The definition C leaves much unspecified and allows
unspecified extensions. Conseqently, one confoming C implementation
may accept a program that another conforming implementation rejects,
and the same conforming C program may produce different results when
run in tow different cocforming implementations.

Mikko