show/hide this revision's text 2 grammar

Rather than to a book, I point you to real formalizations in a set theory: I deem this appropriate given the question itself. Otherwise, downvote me please :)

I happen to have formalized in Mizar set theory (which is Tarski-Grothendieck, i.e. ZFC on steroids) the stuff you seem pointing to: language, wffs, interpretation, satisfaction relation, evaluation, sequent derivability, provability, etc...

In FOMODEL1: http://mizar.auburn.edu/version/current/html/fomodel1.html

you get most syntax (up to definition of atomic formula, or 0wff).

In FOMODEL2: http://mizar.auburn.edu/version/current/html/fomodel2.html

you will find the definition of satisfaction.

That is a series of five subsequent articles starting from scratch and getting to completeness theorem (and Lowenheim-Skolem, the latter only on my homepage, not submitted to Mizar people yet). The links point to hypertextual, proof-pruned versions. For full formalizations, look for the same files with the extension .miz in that same server.

Mizar formalizations are arguably among the most readable for the average mathematician (that's the factor that got myself started with it), that's why I thought you could find this stuff of some interest.
show/hide this revision's text 1 [made Community Wiki]

Rather than a book, I point you to real formalizations in a set theory: I deem this appropriate given the question itself. Otherwise, downvote me please :)

I happen to have formalized in Mizar set theory (which is Tarski-Grothendieck, i.e. ZFC on steroids) the stuff you seem pointing to: language, wffs, interpretation, satisfaction relation, evaluation, sequent derivability, provability, etc...

In FOMODEL1: http://mizar.auburn.edu/version/current/html/fomodel1.html

you get most syntax (up to definition of atomic formula, or 0wff).

In FOMODEL2: http://mizar.auburn.edu/version/current/html/fomodel2.html

you will find the definition of satisfaction.

That is a series of five subsequent articles starting from scratch and getting to completeness theorem (and Lowenheim-Skolem, the latter only on my homepage, not submitted to Mizar people yet). The links point to hypertextual, proof-pruned versions. For full formalizations, look for the same files with the extension .miz in that same server.

Mizar formalizations are arguably among the most readable for the average mathematician (that's the factor that got myself started with it), that's why I thought you could find this stuff of some interest.