[FOM] formalized metalanguage

[Richard Heck]

> Chris Gray wrote:
>
>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.
>
>[snip]
>
>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
>  
>
I wondered about this same issue as well. Obviously, the arithmetization
of meta-mathematics is all about formalizing meta-logic, but there is
something intuitively unnatural about that approach. And of course,
there are all kinds of strange problems that arise there, of the sort
familiar from Feferman's early work. Recently, though, I found some
material that satisfied me a little better.

There is a paper by Feferman, "Finitary Inductively Presented Logics",
on his web site that echoes (in ways I seem to remember him mentioning)
Quine's presentation in "Mathematical Logic". Probably unsurprisingly,
he is also interested there in the same kinds of issues that drove his
early papers on arithmetization, but this is a completely different
approach. (Speaking of which, his paper "My Route to Arithmetization",
which is more a conversational piece, provides some historical
background I, anyway, found interesting.) The theory in question, which
Feferman calls FS_0, turns out to be of the same strength as I\Sigma_1,
and Feferman sketches a proof in FS_0 of G\"odel's second incompleteness
theorem, in the form:

    If S extends FS_0, then: FS_0 \vdash Con_S \to \neg Prov_S(\chi_S),

where \chi_S is the canonical consistency statement for S.

FS_0 gives you a basic theory of syntax. How much more you can do will
depend upon how much more you're prepared to assume. Feferman mentions
that a great deal of countable model theory can (by established methods)
be formalized in FS_0 + Weak K\"onig's Lemma (which is conservative over
PRA, by a result of Harvey's) or, again, in a natural extension FS_1
that yields a conservative extension of PA. Apparently, Paolo Mancosu
showed that even FS_0 will yield non-trivial portions thereof. (I don't
know whether Paolo ever published those results. Drop him a note---he's
at Berkeley---if you're interested.)

Formalization of Tarski-type truth-theories in such a framework would be
straightforward. Of course, the usual limitative results will require us
to add expressive resources to the language of FS_0 if we're going to
get a truth-theory for it, but adding "satisfies" and appropriate axioms
should suffice.

Richard

-- 
==================================================================
Richard G Heck, Jr
Professor of Philosophy
Brown University
http://bobjweil.com/heck/
==================================================================
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:
http://dudu.dyn.2-h.org/nist/gpg-enigmail-howto