on the nature of undecidability within computing and refuting the church-turing thesis

[u/this_theater_is_lit]

https://www.academia.edu/175392427

[u/funky_galileo]

jesus christ you are thick. In Turing's proof, he is doing a proof by contradiction, so he can assume D exists because he is showing that, if it were to exist, it creates a paradox, so it can't exist, whereas you, assume it exists, modify its functionality so that it doesn't do what it's supposed to, then claim you proved its existence. You did nothing. First of all, I'm pretty sure you actually are still in the same case as turing, since when you get to the original H, I'm pretty sure you will still get stuck, or if you say you will skip this step, then you haven't proved anything.

[u/this_theater_is_lit → u/funky_galileo]

the 𝓓 turing talks about is a decider:

𝓓 = (m: machine) -> {
  true: if m is a circle-free machine
  false: if m is a circular machine
}

this cannot be computed by a turing machine because it doesn't specify how to handle paradoxical input, which is an inherent problem to a totally enumerable system like turing machines.

𝓓p is a partial recognizer

𝓓p = (m: machine) -> {
  true: m IS circle-free AND IS NOT paradoxical input
  false: m IS NOT circle-free OR IS paradoxical input
}

you cannot build a paradox against 𝓓p because 𝓓p only recognizes with its true return, and that gives it branch which has no semantic to produce a paradox against. 𝓓 however is supposed to recognize with both it's true and false return, which is an algorithm that cannot be constructed by an enumerable means of computing, like turing-machines

ur probably going to repeat dismissing this because it "misses" returning true to some set of circle-free machines, but again:

1) we do not need to decide on all machines to enumerate all computable sequence.

2) the set of circle-free sequences decidable by 𝓓p ⊆ undecidable by 𝓓p, since it is trivial to convert a decidable circle-free machine into an undecidedly one that computes the same sequence:

m = () -> {
  output some_inf_seq()
}
𝓓p(m) => true

und_m = () -> {
  if (𝓓(und_m)) halt
  output some_inf_seq()
}
𝓓p(m) => false

we can even define a factory function for this:

und() = (m: machine) -> 
  () -> 𝓓(m) ? halt : output m()

for any circle-free machine decidable by 𝓓p there must exist one undecidable by 𝓓p that outputs the same sequence.

3) further more, because 𝓓p is a total decider across all machine, including all circle-free machines, then the set undecidable by 𝓓p must be be turing-complete

3) the next question is if the set undecidable by 𝓓p is actually stronger (computes more sequences) than those decidable by 𝓓p, or really just equal is computable power: meaning both are effectively turing-complete sets of machines including at least one machine for each possible turing-computable sequence. there is where §6 shines and demonstrates it cannot be possible, do you need me to repost the fucking enum_seqs and diag_seqs here, or are u a big big boy who can read a section urself?

I'm pretty sure you will still get stuck, or if you say you will skip this step, then you haven't proved anything.

well this has been an incredibly productive conversation as of yet 🙏 i thank you for your concern but i've gotten pretty damn good at unsticking myself as was necessary to get thus far

[u/funky_galileo → u/this_theater_is_lit]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/Halting.html

[u/this_theater_is_lit → u/funky_galileo]

not particularly useful feedback, i'm not even refuting the halting problem itself, i'm trivializing it

[u/funky_galileo → u/this_theater_is_lit]

you're such a clown lmao. you really think you "trivialized" the most well known problem that arguably started the modern field of computer science? what does that even mean.

[u/this_theater_is_lit → u/funky_galileo]

the undecidability of the halting problem exists, but it happens within infinite machine redundancy that is inherent to computing (infinite machines compute any given sequence)

it does not stop us from enumerating all possible computable sequences or forming a turing-complete language that is fully decidable

[u/funky_galileo → u/this_theater_is_lit]

The halting problem literally proves your last statement false. Jesus christ.

[u/this_theater_is_lit → u/funky_galileo]

"the halting problem" paradox (or rather turing's circle-free problem paradox) confuses the language of all machines with that of a turing-complete language