On formally undecidable traits of intelligent machines

Building on work by Alfonseca et al. (2021), the paper studies the conditions necessary for it to be logically possible to prove that an arbitrary artificially intelligent machine will exhibit certain behavior. To do this, the paper develops a formalism like -- but mathematically distinct from -- the theory of formal languages and their properties. The formalism affords a precise means for not only talking about the traits we desire of machines (such as them being intelligent, contained, moral, and so forth), but also for detailing the conditions necessary for it to be logically possible to decide whether a given arbitrary machine possesses such a trait or not. Contrary to Alfonseca et al.'s (2021) results, Rice's theorem from computability theory cannot in general be used to determine whether an arbitrary machine possesses a given trait or not. Therefore, it is not necessarily the case that deciding whether an arbitrary machine is intelligent, contained, moral, and so forth is logically impossible, but this theoretical control will become increasingly difficult to obtain as advanced AI systems remain genuine black boxes. Since under no agreeable definition of “desired intelligent machines” will the trait be semantic, no version of Rice’s theorem can formally forbid one from deciding it — so more research in this direction is paramount, particularly toward precisifying the definitions inherent to our desires for intelligent machines; otherwise no means will ever be found to decide such traits.