If simulating halt decider H correctly simulates its input D until H
correctly determines that its simulated D would never stop running
unless aborted then H can abort its simulation of D and correctly report
that D specifies a non-halting sequence of configurations.

Once the above is verified to be a tautology then it can be accepted as
an axiom for Simulating halt deciders.

When we apply ordinary software engineering code analysis to H(D,D)
shown below we see that the criteria of the above axiom is met:

simulating halt decider H correctly simulates its
input D until H correctly determines that its
simulated D would never stop running unless aborted

thus it is proven that H correctly reports that D specifies a
non-halting sequence of configurations.

*Every rebuttal to this*
(a) Ignores that the first paragraph above is an axiom, thus failing to
understand that it is a tautology.
(b) Performs the software engineering code analysis incorrectly.

void D(void (*x)())
{ int Halt_Status = H(x, x);
if (Halt_Status)
HERE: goto HERE;
return;
}

int main()
{ H(D,D);
}

_D()
[000019b3] 55 push ebp
[000019b4] 8bec mov ebp,esp
[000019b6] 51 push ecx
[000019b7] 8b4508 mov eax,[ebp+08]
[000019ba] 50 push eax
[000019bb] 8b4d08 mov ecx,[ebp+08]
[000019be] 51 push ecx
[000019bf] e8bff9ffff call 00001383
[000019c4] 83c408 add esp,+08
[000019c7] 8945fc mov [ebp-04],eax
[000019ca] 837dfc00 cmp dword [ebp-04],+00
[000019ce] 7402 jz 000019d2
[000019d0] ebfe jmp 000019d0
[000019d2] 8be5 mov esp,ebp
[000019d4] 5d pop ebp
[000019d5] c3 ret
Size in bytes:(0035) [000019d5]

_main()
[000019e3] 55 push ebp
[000019e4] 8bec mov ebp,esp
[000019e6] 68b3190000 push 000019b3 // push D
[000019eb] 68b3190000 push 000019b3 // push D
[000019f0] e88ef9ffff call 00001383 // call H
[000019f5] 83c408 add esp,+08
[000019f8] 33c0 xor eax,eax
[000019fa] 5d pop ebp
[000019fb] c3 ret
Size in bytes:(0025) [000019fb]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[000019e3][00102a39][00000000] 55 push ebp // begin main
[000019e4][00102a39][00000000] 8bec mov ebp,esp
[000019e6][00102a35][000019b3] 68b3190000 push 000019b3 // push D
[000019eb][00102a31][000019b3] 68b3190000 push 000019b3 // push D
[000019f0][00102a2d][000019f5] e88ef9ffff call 00001383 // call H

When H correctly simulates D it finds that D remains stuck in recursive
simulation

H: Begin Simulation Execution Trace Stored at:112ae5
Address_of_H:1383
[000019b3][00112ad1][00112ad5] 55 push ebp // begin D
[000019b4][00112ad1][00112ad5] 8bec mov ebp,esp
[000019b6][00112acd][00102aa1] 51 push ecx
[000019b7][00112acd][00102aa1] 8b4508 mov eax,[ebp+08]
[000019ba][00112ac9][000019b3] 50 push eax // call D
[000019bb][00112ac9][000019b3] 8b4d08 mov ecx,[ebp+08]
[000019be][00112ac5][000019b3] 51 push ecx // push D
[000019bf][00112ac1][000019c4] e8bff9ffff call 00001383 // call H
H: Infinitely Recursive Simulation Detected Simulation Stopped

We can see that the first seven instructions of D simulated by H
precisely match the first seven instructions of the x86 source-code of
D. This conclusively proves that these instructions were simulated
correctly.

Anyone sufficiently technically competent in the x86 programming
language will agree that the above execution trace of D simulated by H
shows that D will never stop running unless H aborts its simulation of D.

H detects that D is calling itself with the exact same arguments that H
was called with and there are no conditional branch instructions from
the beginning of D to its call to H that can possibly escape the
repetition of this recursive simulation.

[000019f5][00102a39][00000000] 83c408 add esp,+08
[000019f8][00102a39][00000000] 33c0 xor eax,eax
[000019fa][00102a3d][00000018] 5d pop ebp
[000019fb][00102a41][00000000] c3 ret // end main
Number of Instructions Executed(972) == 15 Pages

Simulating Halt Decider Applied to the Halting Theorem
https://www.researchgate.net/publication/364657019_Simulating_Halt_Decider_Applied_to_the_Halting_Theorem

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

On Saturday, 3 December 2022 at 19:34:59 UTC+2, olcott wrote:
> If simulating halt decider H correctly simulates its input D until H
> correctly determines that its simulated D would never stop running
Olcott, shut up already. Your decider is using proof by induction. You are extrapolating a general conclusion from a small set of observations.

The argument isn't whether your decider is "correct" or "incorrect".

The argument is whether your generalization is "faulty"; or not.

https://en.wikipedia.org/wiki/Faulty_generalization

On 12/3/2022 2:11 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 19:34:59 UTC+2, olcott wrote:
>> If simulating halt decider H correctly simulates its input D until H
>> correctly determines that its simulated D would never stop running
> Olcott, shut up already. Your decider is using proof by induction. You are extrapolating a general conclusion from a small set of observations.
>
> The argument isn't whether your decider is "correct" or "incorrect".
>
> The argument is whether your generalization is "faulty"; or not.
>
> https://en.wikipedia.org/wiki/Faulty_generalization

As you just said in your rebuttal of Richard H is a partial halt
decider. H correctly determines whether or not elements of its domain
specify halting computations.

One of the elements of its domain is the "impossible" input required by
all of the conventional halting problem proofs:

void D(void (*x)())
{ int Halt_Status = H(x, x);
if (Halt_Status)
HERE: goto HERE;
return;
}

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

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

On 12/3/2022 2:11 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 19:34:59 UTC+2, olcott wrote:
>> If simulating halt decider H correctly simulates its input D until H
>> correctly determines that its simulated D would never stop running
> Olcott, shut up already. Your decider is using proof by induction. You are extrapolating a general conclusion from a small set of observations.
>
> The argument isn't whether your decider is "correct" or "incorrect".
>
> The argument is whether your generalization is "faulty"; or not.
>
> https://en.wikipedia.org/wiki/Faulty_generalization

It can be seen on the basis of induction that D correctly simulated by H
would never stop running unless aborted.

void D(void (*x)())
{ int Halt_Status = H(x, x);
if (Halt_Status)
HERE: goto HERE;
return;
}

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

--
Copyright 2022 Olcott

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

On Saturday, 3 December 2022 at 22:28:33 UTC+2, olcott wrote:
> On 12/3/2022 2:11 PM, Skep Dick wrote:
> > On Saturday, 3 December 2022 at 19:34:59 UTC+2, olcott wrote:
> >> If simulating halt decider H correctly simulates its input D until H
> >> correctly determines that its simulated D would never stop running
> > Olcott, shut up already. Your decider is using proof by induction. You are extrapolating a general conclusion from a small set of observations.
> >
> > The argument isn't whether your decider is "correct" or "incorrect".
> >
> > The argument is whether your generalization is "faulty"; or not.
> >
> > https://en.wikipedia.org/wiki/Faulty_generalization
> As you just said in your rebuttal of Richard H is a partial halt
> decider. H correctly determines whether or not elements of its domain
> specify halting computations.
>
> One of the elements of its domain is the "impossible" input required by
> all of the conventional halting problem proofs:
> void D(void (*x)())
> {
> int Halt_Status = H(x, x);
> if (Halt_Status)
> HERE: goto HERE;
> return;
> }
>
> int main()
> {
> Output("Input_Halts = ", H(D, D));
> }
You are not even attempting to address my point. Your decider is drawing its conclusion inductively.
Induction is a problem: https://en.wikipedia.org/wiki/Problem_of_induction

Just because you've observed a call (with the same parameters) N times; it doesn't mean that the next call won't be different and break the pattern.

On Saturday, 3 December 2022 at 22:33:20 UTC+2, olcott wrote:
> It can be seen on the basis of induction that D correctly simulated by H
> would never stop running unless aborted.
It might have stopped. You don't know!

https://en.wikipedia.org/wiki/Problem_of_induction

On 12/3/2022 2:36 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 22:28:33 UTC+2, olcott wrote:
>> On 12/3/2022 2:11 PM, Skep Dick wrote:
>>> On Saturday, 3 December 2022 at 19:34:59 UTC+2, olcott wrote:
>>>> If simulating halt decider H correctly simulates its input D until H
>>>> correctly determines that its simulated D would never stop running
>>> Olcott, shut up already. Your decider is using proof by induction. You are extrapolating a general conclusion from a small set of observations.
>>>
>>> The argument isn't whether your decider is "correct" or "incorrect".
>>>
>>> The argument is whether your generalization is "faulty"; or not.
>>>
>>> https://en.wikipedia.org/wiki/Faulty_generalization
>> As you just said in your rebuttal of Richard H is a partial halt
>> decider. H correctly determines whether or not elements of its domain
>> specify halting computations.
>>
>> One of the elements of its domain is the "impossible" input required by
>> all of the conventional halting problem proofs:
>> void D(void (*x)())
>> {
>> int Halt_Status = H(x, x);
>> if (Halt_Status)
>> HERE: goto HERE;
>> return;
>> }
>>
>> int main()
>> {
>> Output("Input_Halts = ", H(D, D));
>> }
> You are not even attempting to address my point. Your decider is drawing its conclusion inductively.
> Induction is a problem: https://en.wikipedia.org/wiki/Problem_of_induction
>
> Just because you've observed a call (with the same parameters) N times; it doesn't mean that the next call won't be different and break the pattern.
>

The fact that there is no conditional code that can break the pattern
establishes a recursion invariant that proves non-halting.

http://web.stanford.edu/class/archive/cs/cs161/cs161.1176/Sections/161-section-1.pdf

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

On Saturday, 3 December 2022 at 22:40:59 UTC+2, olcott wrote:
> The fact that there is no conditional code that can break the pattern
> establishes a recursion invariant that proves non-halting.

There is conditional code. Do you not see the "IF" statement?

On 12/3/2022 2:37 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 22:33:20 UTC+2, olcott wrote:
>> It can be seen on the basis of induction that D correctly simulated by H
>> would never stop running unless aborted.
> It might have stopped. You don't know!
>
> https://en.wikipedia.org/wiki/Problem_of_induction

Are you ignoring that analytic versus synthetic distinction on purpose
or have you never heard of this?

The POI does not apply to mathematical induction.

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

On 12/3/2022 2:50 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 22:40:59 UTC+2, olcott wrote:
>> The fact that there is no conditional code that can break the pattern
>> establishes a recursion invariant that proves non-halting.
>
> There is conditional code. Do you not see the "IF" statement?
>
>

The execution trace of D correctly simulated by H proves that it cannot
possibly reach its conditional code. I have already showed this in my OP.

_D()
[000019b3] 55 push ebp
[000019b4] 8bec mov ebp,esp
[000019b6] 51 push ecx
[000019b7] 8b4508 mov eax,[ebp+08]
[000019ba] 50 push eax
[000019bb] 8b4d08 mov ecx,[ebp+08]
[000019be] 51 push ecx
[000019bf] e8bff9ffff call 00001383 // can't get past here
[000019c4] 83c408 add esp,+08
[000019c7] 8945fc mov [ebp-04],eax
[000019ca] 837dfc00 cmp dword [ebp-04],+00
[000019ce] 7402 jz 000019d2
[000019d0] ebfe jmp 000019d0
[000019d2] 8be5 mov esp,ebp
[000019d4] 5d pop ebp
[000019d5] c3 ret
Size in bytes:(0035) [000019d5]

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

On Saturday, 3 December 2022 at 23:03:26 UTC+2, olcott wrote:
> The POI does not apply to mathematical induction.
It doesn't apply to inductively-defined objects, but it absolutely applies to function analysis!

You have absolutely NO idea whether the function you are studying is inductively defined with some upper bound!

https://en.wikipedia.org/wiki/Wittgenstein_on_Rules_and_Private_Language#The_rule-following_paradox

On Saturday, 3 December 2022 at 23:07:33 UTC+2, olcott wrote:
> The execution trace of D correctly simulated by H proves that it cannot
> possibly reach its conditional code. I have already showed this in my OP.
Huh?!?!

Here is the conditional code which would lead to a halt. It looks very reachable to me.

> _D()
> [000019ce] 7402 jz 000019d2

On Saturday, 3 December 2022 at 23:07:33 UTC+2, olcott wrote:
> _D()
> [000019ce] 7402 jz 000019d2
> [000019d0] ebfe jmp 000019d0
> [000019d2] 8be5 mov esp,ebp

Let me translate that the instruction @ 000019ce into English for you.
it says "Jump OVER the Infinite loop."

On 12/3/22 12:34 PM, olcott wrote:
> If simulating halt decider H correctly simulates its input D until H
> correctly determines that its simulated D would never stop running
> unless aborted then H can abort its simulation of D and correctly report
> that D specifies a non-halting sequence of configurations.

Right, and the DEFINITON of "Correct Simultion" means a simulation that
demonstrates the behavior of the direct exectution of this exact input.

Since D(D) WILL Halt BECAUSE ITS copy of H aborts another simulation of
D(D), this H doesn't NEED to abort its simulation, so the condition is
not satisfied.

>
> Once the above is verified to be a tautology then it can be accepted as
> an axiom for Simulating halt deciders.
>
> When we apply ordinary software engineering code analysis to H(D,D)
> shown below we see that the criteria of the above axiom is met:
>
>    simulating halt decider H correctly simulates its
>    input D until H correctly determines that its
>    simulated D would never stop running unless aborted

Which you either do not apply correctly or is defined incorrectly making
your definition inconsistent with the Computation Theory definition of a
Halting Decider.

Meaning you are not working on the Halting Problem

>
> thus it is proven that H correctly reports that D specifies a
> non-halting sequence of configurations.

Only by the WRONG definiotion.

>
> *Every rebuttal to this*
> (a) Ignores that the first paragraph above is an axiom, thus failing to
>     understand that it is a tautology.

No, it isn't an axiom.

It is a statement which can be proven witht ee CORRECT meaning pof teh
words from teh DEFINTION of a Halt Decider, which shows what the correct
meaning of the words needs to be.

> (b) Performs the software engineering code analysis incorrectly.

What, you think running the input program isn't a correct analysis to
determine if the program halt?

Since it is the DEFINITION, YOU sre the one doing an incorrect analysis.

>
> void D(void (*x)())
> {
>   int Halt_Status = H(x, x);
>   if (Halt_Status)
>     HERE: goto HERE;
>   return;
> }
>
> int main()
> {
>   H(D,D);
> }
>
> _D()
> [000019b3] 55         push ebp
> [000019b4] 8bec       mov ebp,esp
> [000019b6] 51         push ecx
> [000019b7] 8b4508     mov eax,[ebp+08]
> [000019ba] 50         push eax
> [000019bb] 8b4d08     mov ecx,[ebp+08]
> [000019be] 51         push ecx
> [000019bf] e8bff9ffff call 00001383
> [000019c4] 83c408     add esp,+08
> [000019c7] 8945fc     mov [ebp-04],eax
> [000019ca] 837dfc00   cmp dword [ebp-04],+00
> [000019ce] 7402       jz 000019d2
> [000019d0] ebfe       jmp 000019d0
> [000019d2] 8be5       mov esp,ebp
> [000019d4] 5d         pop ebp
> [000019d5] c3         ret
> Size in bytes:(0035) [000019d5]
>
> _main()
> [000019e3] 55             push ebp
> [000019e4] 8bec           mov ebp,esp
> [000019e6] 68b3190000     push 000019b3 // push D
> [000019eb] 68b3190000     push 000019b3 // push D
> [000019f0] e88ef9ffff     call 00001383 // call H
> [000019f5] 83c408         add esp,+08
> [000019f8] 33c0           xor eax,eax
> [000019fa] 5d             pop ebp
> [000019fb] c3             ret
> Size in bytes:(0025) [000019fb]
>
>  machine   stack     stack     machine    assembly
>  address   address   data      code       language
>  ========  ========  ========  =========  =============
> [000019e3][00102a39][00000000] 55         push ebp      // begin main
> [000019e4][00102a39][00000000] 8bec       mov ebp,esp
> [000019e6][00102a35][000019b3] 68b3190000 push 000019b3 // push D
> [000019eb][00102a31][000019b3] 68b3190000 push 000019b3 // push D
> [000019f0][00102a2d][000019f5] e88ef9ffff call 00001383 // call H
>
> When H correctly simulates D it finds that D remains stuck in recursive
> simulation
>
> H: Begin Simulation   Execution Trace Stored at:112ae5
> Address_of_H:1383
> [000019b3][00112ad1][00112ad5] 55         push ebp       // begin D
> [000019b4][00112ad1][00112ad5] 8bec       mov ebp,esp
> [000019b6][00112acd][00102aa1] 51         push ecx
> [000019b7][00112acd][00102aa1] 8b4508     mov eax,[ebp+08]
> [000019ba][00112ac9][000019b3] 50         push eax       // call D
> [000019bb][00112ac9][000019b3] 8b4d08     mov ecx,[ebp+08]
> [000019be][00112ac5][000019b3] 51         push ecx       // push D
> [000019bf][00112ac1][000019c4] e8bff9ffff call 00001383  // call H
> H: Infinitely Recursive Simulation Detected Simulation Stopped
>
> We can see that the first seven instructions of D simulated by H
> precisely match the first seven instructions of the x86 source-code of
> D. This conclusively proves that these instructions were simulated
> correctly.
>
> Anyone sufficiently technically competent in the x86 programming
> language will agree that the above execution trace of D simulated by H
> shows that D will never stop running unless H aborts its simulation of D.
>
> H detects that D is calling itself with the exact same arguments that H
> was called with and there are no conditional branch instructions from
> the beginning of D to its call to H that can possibly escape the
> repetition of this recursive simulation.
>
> [000019f5][00102a39][00000000] 83c408     add esp,+08
> [000019f8][00102a39][00000000] 33c0       xor eax,eax
> [000019fa][00102a3d][00000018] 5d         pop ebp
> [000019fb][00102a41][00000000] c3         ret  // end main
> Number of Instructions Executed(972) == 15 Pages
>
> Simulating Halt Decider Applied to the Halting Theorem
> https://www.researchgate.net/publication/364657019_Simulating_Halt_Decider_Applied_to_the_Halting_Theorem
>
>

On 12/3/2022 3:40 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 23:03:26 UTC+2, olcott wrote:
>> The POI does not apply to mathematical induction.
> It doesn't apply to inductively-defined objects, but it absolutely applies to function analysis!
>
> You have absolutely NO idea whether the function you are studying is inductively defined with some upper bound!
>
> https://en.wikipedia.org/wiki/Wittgenstein_on_Rules_and_Private_Language#The_rule-following_paradox

Because we could possibly be brains in vats connected to computers we
cannot trust that any aspect of what appears to be physical reality is
actual reality. This does not apply to mathematics.

Whether or not we are brains in vats 2+2 = 4 either way.

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

On 12/3/2022 3:41 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 23:07:33 UTC+2, olcott wrote:
>> The execution trace of D correctly simulated by H proves that it cannot
>> possibly reach its conditional code. I have already showed this in my OP.
> Huh?!?!
>
> Here is the conditional code which would lead to a halt. It looks very reachable to me.
>
>> _D()
>> [000019ce] 7402 jz 000019d2
>

Only because you did not carefully study my original post. D simulated
by H remains stuck in recursive simulation until aborted thus cannot
possibly reach its own conditional code whether aborted or not.

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

On Saturday, 3 December 2022 at 23:48:31 UTC+2, olcott wrote:
> On 12/3/2022 3:40 PM, Skep Dick wrote:
> > On Saturday, 3 December 2022 at 23:03:26 UTC+2, olcott wrote:
> >> The POI does not apply to mathematical induction.
> > It doesn't apply to inductively-defined objects, but it absolutely applies to function analysis!
> >
> > You have absolutely NO idea whether the function you are studying is inductively defined with some upper bound!
> >
> > https://en.wikipedia.org/wiki/Wittgenstein_on_Rules_and_Private_Language#The_rule-following_paradox
> Because we could possibly be brains in vats connected to computers we
> cannot trust that any aspect of what appears to be physical reality is
> actual reality. This does not apply to mathematics.
No idea why you are even comparing the two.

Mathematics is invented. Reality is not.

You've confused synthetic truths (Mathematics) with analytic truths (studying reality).

On 12/3/2022 3:57 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 23:48:31 UTC+2, olcott wrote:
>> On 12/3/2022 3:40 PM, Skep Dick wrote:
>>> On Saturday, 3 December 2022 at 23:03:26 UTC+2, olcott wrote:
>>>> The POI does not apply to mathematical induction.
>>> It doesn't apply to inductively-defined objects, but it absolutely applies to function analysis!
>>>
>>> You have absolutely NO idea whether the function you are studying is inductively defined with some upper bound!
>>>
>>> https://en.wikipedia.org/wiki/Wittgenstein_on_Rules_and_Private_Language#The_rule-following_paradox
>> Because we could possibly be brains in vats connected to computers we
>> cannot trust that any aspect of what appears to be physical reality is
>> actual reality. This does not apply to mathematics.
> No idea why you are even comparing the two.
>
> Mathematics is invented. Reality is not.
>
> You've confused synthetic truths (Mathematics) with analytic truths (studying reality).

That wild guess of the analytic/synthetic distinction is woefully
incorrect.

*I divided it up a little more precisely*
(a) Analytic truth is verified as true entirely on the basis of the
semantic meaning of expressions of language.

(b) Expressions of language of Empirical truth requires sense data from
the sense organs to verify its truth.

The problem of induction only applies to the latter and not to the former.

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

On Sunday, 4 December 2022 at 00:14:38 UTC+2, olcott wrote:
> *I divided it up a little more precisely*
> (a) Analytic truth is verified as true entirely on the basis of the
> semantic meaning of expressions of language.

How are you going to verify the semantic meaning when you continuously confuse syntax for semantics?

> (b) Expressions of language of Empirical truth requires sense data from
> the sense organs to verify its truth.
Which is exactly what the BHK interpretation requires also!

https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation

On 2022-12-03 17:34:55 +0000, olcott said:

> If simulating halt decider H correctly simulates its input D until H
> correctly determines that its simulated D would never stop running
> unless aborted then H can abort its simulation of D and correctly
> report that D specifies a non-halting sequence of configurations.
>
> Once the above is verified to be a tautology then it can be accepted as
> an axiom for Simulating halt deciders.

Once that is verified to be a tautology then it can (and should) be removed
from the set of axioms for Simulating halt deciders (and other axiom sets).
It is regarded as a bad style to use redundant axioms, and tautologies are
theorems of logic, thus redundant as axioms of a theory.

Mikko

On Sunday, 4 December 2022 at 11:31:18 UTC+2, Mikko wrote:
> Once that is verified to be a tautology then it can (and should) be removed
> from the set of axioms for Simulating halt deciders (and other axiom sets).
> It is regarded as a bad style to use redundant axioms, and tautologies are
> theorems of logic, thus redundant as axioms of a theory.

What is the logical implication of your words? What theorems follow form what you say?
Are you suggesting that axioms are NOT tautologies (true in every model) and are thus subject to falsification?

On Sunday, 4 December 2022 at 11:31:18 UTC+2, Mikko wrote:
> Once that is verified to be a tautology then it can (and should) be removed
> from the set of axioms for Simulating halt deciders (and other axiom sets).
> It is regarded as a bad style to use redundant axioms, and tautologies are
> theorems of logic, thus redundant as axioms of a theory.

Perhaps an example would bode well...

x=x is assumed to be a tautology. That's all fine and well, but is it an axiom or a theorem?

On 12/4/2022 3:31 AM, Mikko wrote:
> On 2022-12-03 17:34:55 +0000, olcott said:
>
>> If simulating halt decider H correctly simulates its input D until H
>> correctly determines that its simulated D would never stop running
>> unless aborted then H can abort its simulation of D and correctly
>> report that D specifies a non-halting sequence of configurations.
>>
>> Once the above is verified to be a tautology then it can be accepted
>> as an axiom for Simulating halt deciders.
>
> Once that is verified to be a tautology then it can (and should) be removed
> from the set of axioms for Simulating halt deciders (and other axiom sets).
> It is regarded as a bad style to use redundant axioms, and tautologies are
> theorems of logic, thus redundant as axioms of a theory.
>
> Mikko
>

All axioms are tautologies. The only way to correctly determine that a
brand new axiom has been discovered is to verify that it is a tautology.

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

On Sun, 04 Dec 2022 02:29:35 -0800, Skep Dick wrote:

> On Sunday, 4 December 2022 at 11:31:18 UTC+2, Mikko wrote:
>> Once that is verified to be a tautology then it can (and should) be
>> removed from the set of axioms for Simulating halt deciders (and other
>> axiom sets).
>> It is regarded as a bad style to use redundant axioms, and tautologies
>> are theorems of logic, thus redundant as axioms of a theory.
>
> Perhaps an example would bode well...
>
> x=x is assumed to be a tautology. That's all fine and well, but is it an
> axiom or a theorem?

It is an axiom and axioms require no proof as they are true by definition.

/Flibble

On 12/4/22 10:20 AM, olcott wrote:
> On 12/4/2022 3:31 AM, Mikko wrote:
>> On 2022-12-03 17:34:55 +0000, olcott said:
>>
>>> If simulating halt decider H correctly simulates its input D until H
>>> correctly determines that its simulated D would never stop running
>>> unless aborted then H can abort its simulation of D and correctly
>>> report that D specifies a non-halting sequence of configurations.
>>>
>>> Once the above is verified to be a tautology then it can be accepted
>>> as an axiom for Simulating halt deciders.
>>
>> Once that is verified to be a tautology then it can (and should) be
>> removed
>> from the set of axioms for Simulating halt deciders (and other axiom
>> sets).
>> It is regarded as a bad style to use redundant axioms, and tautologies
>> are
>> theorems of logic, thus redundant as axioms of a theory.
>>
>> Mikko
>>
>
> All axioms are tautologies. The only way to correctly determine that a
> brand new axiom has been discovered is to verify that it is a tautology.
>

No, a tautology is a statment that by its structure MUST be true for all
cases.

An axiom is a statement of accepted self-evident truth. They are not
"Discovered", except in the creation of a new branch of a field, as they
form the basis of that branch/field.

For example, Euclid's 5th Axiom: Given a line, and a point not on that
line, only one line can be drawn through that point that never touches
that line.

This statement is taken as a true statement in Euclidian Geometry.

That statement is NOT a tautology in general, as in non-Euclidian
Geometry it does not hold.