[FOM] formalized metalanguage

Jesse Alama alama at stanford.edu
Thu Jan 26 17:46:36 EST 2006

Some large libraries of formal mathematics (for example, the MIZAR
library) contain developments of parts of mathematical logic (as of
late 2004, for example, MIZAR's proof library contains a development
of first-order logic leading to the completeness theorem).  Are these
examples of formalization similar to what you had in mind?


PS The MIZAR homepage can be found at http://www.mizar.org .  You can
browse the actual proof using a web browser by going to


Chris Gray <cpgray at library.uwaterloo.ca> writes:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

Jesse Alama (alama at stanford.edu)

More information about the FOM mailing list