One example a bit closer to what you seek might be:
- George Tourlakis, Lectures in Logic and Set Theory, volumes 1 and 2, Cambridge studies in advanced mathematics, vol. 83. Cambridge University Press, Cambridge, UK, 2003.
You can see my review, which appeared in the Bulletin of symbolic logic, vol. 11, iss. 2, p. 241, 2005:
This is a detailed two-volume development of mathematical logic and set theory, written from a formalist point of view, aimed at a spectrum of students from the third-year undergraduate to junior graduate level. Volume 1 presents the heart of mathematical logic, including the Completeness and Incompleteness theorems along with a bit of computability theory and accompanying ideas. Tourlakis aspires to include “the absolutely essential topics in proof, model and recursion theory” (vol. 1, p. ix). In addition, for the final third of the volume, Tourlakis provides a proof of the Second Incompleteness Theorem “right from Peano’s axioms,...gory details and all,” which he conjectures “is the only complete proof in print [from just Peano arithmetic] other than the one that was given in Hilbert and Bernays (1968)” (vol. 1, p. x). In the opening page of Chapter II, Tourlakis provides a lucid explanation of the proof in plain language, before diving into the details and emerging a hundred pages later with the provability predicate, the derivability conditions and a complete proof. Tempering his formalist tendencies, Tourlakis speaks “the formal language with a heavy 'accent' and using many 'idioms' borrowed from 'real' (meta)mathematics and English,” in a mathematical argot (vol. 1, p. 39). In his theorems and proofs, therefore, he stays close to the formal language without remaining inside it.