[FOM] formalized metalanguage

[Chris Gray]

I'm stumped.  I am looking for work on the formalization of metalogic and 
not having much luck.  This is something that people have done small 
experiments in from time to time, but has not been explored continuously 
by anyone.

An example is the final chapter (Syntax) of Quine's Mathematical Logic 
where he does some constructions beginning by introducing names for 
symbols in the object language and a concatenation operator to first-order 
logic with identity.

The trouble seems to be that there is no (as far as I'm aware) agreed upon 
term for such endeavors, and the relevant terms ('metalogic', 
'metamathematics', 'formal', etc.) don't separate the normal and extensive 
practice of informal metalogic from its formalization.

I'm hoping that someone may be aware of some more recent work along these 
lines, particularly formalizations of Tarski's semantics.

Chris Gray
University of Waterloo

"You put seven rabbits in a pen, add five more, and for a while the total
is twelve."  -W.V.O. Quine