[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?

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)
```