Kurt Gödel [1] has shown fundamental limits of mathematical logic and the unreality of the program of David Hilbert [2] by its incompleteness theorems published in 1931. Arthur Charlesworth tackles this theme’s development over decades and clarifies its impact to computer programs and the foundations of artificial intelligence (AI). After nonrigorous models and reasoning of the literature, in this paper, he develops further formalization of the actors and objects involved in computing, established in his previous paper in 2006 [3]. Throughout the paper, he treats the halting problem form of the original incompleteness theorems and gives a theorem about the capability of precisely defined agents and programs of computing. Beyond this theorem and its proof, the author provides a multifaceted discussion of the theme, which is enriched further in the electronic supplement of the paper.

To be didactic, first he illustrates his main theme and treatment by an analogous one respecting a game. To start, a brief, but imprecise proof of the conjecture about the game (named CHESS as a joke) is shown. On one hand, this “proof” shows clearly the way of thinking, but on the other hand it demonstrates the danger of nonrigorous treatment. Then, introducing the formalism, the precise proof is given.

An interesting characteristic of Charlesworth’s theorem is that the agents and the programs treated may be fallible. However, this attribute is restricted, as from the point of view of the halting problem they should be infallible. The reader can decide the importance of this aspect: at least it also conduces to the clarity and understandability of the proofs.

I recommend this paper for those who are interested in the foundations of AI and would benefit from a clear way of thinking about its notions through a multifaceted discussion.