|
|
Re: Axiomization of Number Theory
Posted:
Jul 31, 2003 4:51 AM
|
|
Mike Oliver <oliver@math.ucla.edu> wrote in message news:<3F28B5F4.B4009893@math.ucla.edu>...
> Andrew Boucher wrote:
>
> > I've seen a distinction made between "semantical" second-order logic and
> > "deductive" second-order logic.
> > Here on FOM for instance (the thread is appropriately entitled "SOL
> > Confusion"):
> > http://www.cs.nyu.edu/pipermail/fom/2000-September/004354.html
> >
> > I'll leave others to say what they're talking about, but I'm referring
> > to "deductive" second-order Peano Arithmetic - the proof system and the
> > theorems which can be generated from PA2.
>
> Well, it seems to me that it's no longer obvious what one means by
> "the proof system" in this case. "Deductive" second-order logic could
> plausibly refer to any r.e. way of generating sematically correct
> second-order conclusions, whereas I gather that you want to restrict
> it to systems that generate conclusions that hold in all two-sorted
> first-order models of the axioms. So I really think "two-sorted first-order
> logic" is a more accurate description than "deductive second-order logic".
>
My impression was that I was using standard terminology, e.g Simpson
speaks of "Second-Order Arithmetic" and Shapiro makes a case for
"Second-Order Logic". Boolos uses this terminology as well. While
"deductive" second-order Peano Arithmetic *could* refer to any r.e.
way as you say, in practice it is not widely used that way, to my
knowledge anyway. Instead it refers (again in practice) to the
specific deductive system I have described, with little- and
big-letters (i.e. two sorts), with comprehension. In any case, I
can't think of any other interpretation of what people mean should
they ask whether PA2 can prove such or such theorem.
But I could well be wrong, since I may well not have a standard view
of what is "standard".
|
|
