FOM: Re: Midwest Model Theory Meeting

[Vaughan Pratt]

Charlie Silver:
>What is being asked for, I think, is something like formal number theory,
>with axioms and such.  That is, the language needs to be specified, and
>the axioms and rules need to specified.  For example, what would be the
>language for your calculus?  And what would the rules be?  My *guess*
>is that the problem could be solved by the Gaussian method in a kind of
>second-order system  of arithmetic without induction (the original point
>was to eliminate induction).

As a metaquestion, is this sort of passage from a specific solution to a
formal system at the core of the reverse mathematics program, or merely
peripheral to it?  My take on reverse mathematics makes it the former,
so if that's not correct it would be good to know.

Vaughan Pratt