[FOM] formalized metalanguage
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
Jesse Alama (alama at stanford.edu)
More information about the FOM