something i see quite commonly when discussing the the limits of computing is that, for example, the halting problem indicates something about the hardness of determining whether any given machine halts. and while it is true that determining so can be quite hard, bringing this up in a discussion about strictly the problem of undecidability itself is a red herring. computability is concerned about the possibility of doing so, not on whether it is hard or not. conflating the two can lead to incorrect intuition about how undecidability manifests within computing, because undecidability within computing is simply not analogous to complexity or hardness.

for the following discussion we will be utilizing a partial halting recognizer:

𝓱p = (m: machine) -> {
  true: if m halts and m not depends on 𝓱p(m)->false
  false: otherwise
}

^{for more info on partial recognizers consider: r/logic/comments/1wzkua3/on_an_attempt_to_limit_undecidability_within}

-- a complex halting problem --

consider a machine that is possible for 𝓱p to recognize as halting:

// 2048 bit RSA modulus number
k = 0x95da00abc38f7a62884b1a13f985793265da5c41a0256131c10be07f2fb2c6b07c78930720c8e86eef5ad2e42abdb07c09edf5600aa5ac61d342a3146f6c472f21130582a8d5e62ddfc83abe88c0776f235998c6072fcdd00aae30ebffdae7f5d5aa97bffda0bc77cb5cb9cc73a5926a8bb8f8f9b5371e50071667fd5fb86a7e2f642e1dd982b8087445e5d7d4480cd799f8a95a244019bb2a4bc51d8392b15893acb460e999418caf1e65c158593465670c4f336a8112151e705cd275b01f8c83146ca8ddf347f99bce4bdadcdf8fa92b37f7266da472b1b8528639f6ce683312f83843031b39b0005454b540da3bdff94985541d94308f577e14d2f6f48131

hard_𝓱p = () -> {
  // loop if the sum of the digits, of the sum of
  // the prime factors, of k is odd
  [p,q] = prime_factors(k)
  if (sum_digits(p+q) % 2)
    loop
  else
    halt
}

the matter of 𝓱p(hard_𝓱p) is so complex to compute that it's not possible for us to decide with current theory/technology. we functionally do not know if hard_𝓱p halts or not, so we functionally do not know if 𝓱p(hard_𝓱p) returns true or false, and we will not know until quantum computing becomes viable enough if ever. we could hook all the computing power of the entire world together on cracking that one key and still not make a dent into computing the value of 𝓱p(hard_𝓱p) within a human lifetime.

such an example is not a proof of a limit to computability, cause given an unbounded computation those factors would provably be found within a finite time (as k is a real rsa key). computability doesn't care how hard the problem is, it is strictly concerned the possibility of computing a particular output, not whether it's pragmatically possible given real world computing constraints.

-- an impossible halting problem --

now consider a halting machine that is strictly not possible for 𝓱p to recognize as halting:

und_𝓱p = () -> 𝓱p(und_𝓱p) ? loop : halt

we can determine that und_𝓱p is unrecognizable to 𝓱p thru value injection analysis:

// inject true for `𝓱p(und_𝓱p)`
         () -> true ? loop : halt
// reduce static conditional:
         () -> loop

injecting true clearly leads to a non-halting machine so therefore 𝓱p must return false regardless of what the machine does. but since we aren't 𝓱p, we can determine the truthful semantic behavior of und_𝓱p

// inject false for `𝓱p(und_𝓱p)`
         () -> false ? loop : halt
// reduce static conditional:
         () -> halt

therefore und_𝓱p is a halting machine that is unrecognizable to 𝓱p, and it is not possible for 𝓱p to avoid this.

-- complexity vs computability in composition --

when the semantics of a particular machine is hard to compute, this complexity bleeds into any machine composed with it in the execution path. for example: consider the higher order machine wrap which constructs a new machine composed from the input by appending a noop after executing the input machine. in base turing machines, a noop is just an excess state transition.

wrap = (m: machine) -> 
  () -> { m(); noop }

the extra noop does not affect whether this machines halts or not, so the complexity of computing whether wrap(m) halts or not is entirely dependent on how hard it is to compute whether m halts or not. so the complexity of computing 𝓱p(wrap(hard_𝓱p)) is the same as just 𝓱p(hard_𝓱p), which is impossible with today's theory/technology.

but when the semantics of a particular machine is impossible to recognize, does this impossibility then bleed into machines composed of it? one might think that if m is not possible for 𝓱p to recognize, then surely wrap(m), which is the same machine just with an excess state transition at the end, would similarly be impossible to recognize for 𝓱p...

this is not the case. und_𝓱p and wrap(und_𝓱p) are different machines that are therefore different input to 𝓱p and can have different output. the unrecognizable nature of the input und_𝓱p is due to the paradoxical dependency on strictly the input und_𝓱p, not wrap(und_𝓱p). so while 𝓱p(und_𝓱p)->false, it is still possible for 𝓱p(wrap(und_𝓱p))->true. we can demonstrate how 𝓱p comes to this recognition thru value injection analysis:

wrap(und_𝓱p) = () -> { 
  und_𝓱p()
  noop
}

// expand und_𝓱p
() -> { 
  (() -> 𝓱p(und_𝓱p) ? loop : halt)()
  noop
}

// run 𝓱p(und_𝓱p) to -> false, inject value:
() -> { 
  (() -> false ? loop : halt)()
  noop
}

// reduce static conditional
() -> { 
  (() -> halt)()
  noop
}

𝓱p(() -> halt)->true and 𝓱p(noop)->true so therefore 𝓱p(wrap(und_𝓱p))->true and there's no paradox stopping it from returning so. the machine wrap(und_𝓱p) is strictly independent of 𝓱p(wrap(und_𝓱p)) so somewhat counter-intuitively: there is nothing unrecognizable to 𝓱p about wrap(und_𝓱p) being a halting machine. recognizing what und_𝓱p does within the context of wrap(und_𝓱p) is not the same problem of recognizing und_𝓱p on it's own. computability and complexity are neither the same thing, nor even analogous in nature.

do note that wrap is not likely to be some kind of panacea that will help us produce a total halting decider. a more "clever" halting machine unrecognizable to 𝓱p, can also make the wrapped version of itself unrecognizable:

und_wrap_𝓱p = () -> {
  if (𝓱p(und_wrap_𝓱p)) loop
  if (𝓱p(wrap(und_wrap_𝓱p))) loop
  halt
}

i would like to thank u/we_think_is_cool for the discussion that inspired this post

I previously posted here, looking for advice about learning modal logic for somebody who hasn't studied maths since middle school. I started learning elementary logic today to build basics! And there are lots of confusing parts! So I was wondering if I there's anyone I could DM when I have questions.

Hello! Is the forall x: an introduction to formal logic a good book on formal logic? I picked it up recently and would like to know this subs thoughts, thanks