I am trying to find a proof of Gödel's second incompleteness theorem for an axiomatic theory T of finite strings from some fixed alphabet Γ, where Γ is, or is similar to, the set of symbols required to write T-sentences. I'm not fussy about what function and predicate symbols are taken as primitive in T (probably at least concatenation, but whatever it takes to make the proof easier). It is also fine (and preferred, if it simplifies the proof at all) if Γ is not finite (with a function symbol to construct variable names) but the union of a finite set with an infinite set of variables $x_1,x_2,\ldots$ (as is often done in the definition of FOL).
Something similar was mentioned in the following question answer as "the computer scientist's dream formulation", but for "lisp-like data": https://math.stackexchange.com/a/2095088/330299
Paulson wrote a computer checked proof of the incompleteness theorems for a theory of hereditarily finite sets, documented in these two papers: