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](http://jdh.hamkins.org/tourlakisbookreview/), 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.

> [more, including criticism...](http://jdh.hamkins.org/tourlakisbookreview/)