Ultimately, of course, Tolkien's constructed languages Entish, Quenya, and Sindarin must be used as the source of semantic distinctions here: it would hardly be appropriate in context to rely upon English-language definitions, after all. Fortunately, Hilbert had introduced Tolkien to the works of Bertrand Russell and Alfred North Whitehead, inspiring him to construct each language with precise logical foundations about which it was possible to prove meaningful theorems, and hope was held out that every statement about the language (e.g., "Enydi ier helda'") could be proven true or false by a formal process which would then be automated.
Further, in Tolkien's lifetime, Kurt Gödel showed that the provability of statements in any formal language of interest to be sharply limited. This work naturally inspired Alan Turing, a passionate lover of Elves and Men alike, to develop his own followup paper in the field now known as computer science, of which he is well known as a founder. Less well-known is Turing's post-war monograph inspired by the Hilbert-Tolkien correspondence, in which he applies a similar diagonalization argument to the languages discussed above and shows the aforementioned question of nudity to be ultimately unresolvable; it is titled
"On decidable languages, with an application to the Entkleidungsproblem".
