> On May 11, 3:57 pm, kleptomaniac6...@hotmail.com wrote:
>

>> I meant full second order arithmetic to be the theory PA+comprehension
>> +second order induction axiom.

>
> 2nd-order logic *already has* a definition, and it *is not* in terms
> of
> "comprehension". It is just in terms of 2nd-order quantifiers
> quantifying
> over "all possible" 1st-order subclasses of the obect-level domain.
>

>> I was wondering what you got with PA +comprehension+first order
>> arithmetic consequences of second order arithmetic.

>
> Second order arithmetic IS CATEGORICAL, so as soon as you say
> "first order arithmetic consequences of second order arithmetic",
> you have said ALL that there is to say. That ALREADY IS ALL the
> 1st-order truths of the 1st-order language of arithmetic.
>

>> In other words, what sort of theorems are provable in
>> second order arithmetic but not the latter system.

>
> EVERYthing that is provable in second order arithmetic is provable
> in "the latter system" BECAUSE you have DEFINED "the latter system"
> TO INCLUDE "first order arithmetic consequences of second order
> arithmetic".
> "consequences of second order arithmetic" MEANS "everything that
> is provable by second order arithmetic".