[FOM] formalized metalanguage

[Jesse Alama]

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?

Jesse

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

http://merak.pb.bialystok.pl/mmlquery/fillin.php?entry=GOEDELCP:35&comment=Goedel+Completeness+Theorem++

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)