> there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity Just to

> there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity Just to focus on this idea of 'a certain complexity', you may like Chaitin's Incompleteness Theorem: https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin's_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin'... which defines the "algorithmic information content" of a symbolic system (whether that's a programming language or a mathematical logic; which are actually the same thing via the Curry-Howard correspondence!) The theorem is a bit technical, but basically involves a program which enumerates all strings of symbols from a chosen alphabet (pretty easy: just a `while` loop that tries longer and longer string lengths, and a `for` loop which goes through the alphabet over and over to output every combination of that many symbols). We use this to define a program which enumerates all proofs of some chosen formal logic (these are just strings of symbols which obey all of that logic's rules, so we just filter the output of the above program). We use this to define a program which enumerates proofs of theorems of the form "all programs which output string s contain at least N instructions" (this is just a pattern-match against the end of the proof). N is a parameter, whilst s can be any string (different proofs can have different strings s). We use this to define a final program, which we'll call P. Running P with a parameter, like P(N), will run the above enumeration for that value of N, and halt once a single proof has been found. Just before halting, P will output whichever string s appears in the proof it found. Now is the interesting part: we count up all of the instructions used to define all of the above programs. Let's call this U (as per the Wikipedia link above). We'll define another number N0 where N0 > U + the number of instructions required to define N0 in a program; in other words, N0 is more than the number of instructions needed to define 'P(N0)'. (Keep in mind that we can generate very large numbers using programs with only a few instructions, so it's easy enough to find a a suitable value of N0). Finally, consider what happens if we run the program P(N0): If P(N0) halts, it will output some particular string s. That string is taken from a proof of the theorem "all programs which output string s contain at least N0 instructions". We know that program P(N0) contains fewer than N0 instructions, which would contradict such a theorem. The only way to avoid this contradiction (other than using an inconsistent logic) is if P(N0) never halts. If P(N0) never halts, that means it will keep enumerating proofs forever without ever finding one for any theorem of the form "all programs which output string s contain at least N0 instructions"; for any string s. This latter result is consistent, but shows that our chosen system of logic (whatever it is), must be severely limited. In particular, we know it is unable to prove statements of the form "all programs which output string s contain at least N instructions" where N >= N0 (in fact, there's a lower bound on N0 based on 'compressing' the above programs into the fewest number of instructions; although finding that lower bound is uncomputable due to the halting problem!). At first glance this doesn't look very important, but consider the pigeonhole principle: there are only a finite number of programs with fewer than N0 instructions; hence there are only a finite number of strings 's' which can provably be generated with fewer than N0 instructions. Almost all strings 's' require more than N0 instructions to generate. Now consider programs of the form 'enumerate all proofs until we find one for statement T, then output T and halt'. If such a program contains more than N0 instructions, then our chosen logic is unable to prove whether this program will halt or not. We can prove that whether or not this program halts is equivalent to whether or not T is provable, and hence the only way for this halting/looping question to be unprovable is for the statement T to be unprovable. Hence almost all statements are unprovable by our given system of logic, regardless of which logic we choose! Chaitin takes this further, to define a "halting probability", and essentially shows that all mathematical 'knowledge' can be distilled down to set of which bits, which tell us whether certain programs halt or not.