What do you get if you swap the second order induction axiom from full
second order arithmetic for the induction schema from Peano
Arithmetic? How much weaker is the resulting theory?

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

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

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

On May 11, 3:57 pm, kleptomaniac6... at (no spam) 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".

I mean second order arithmetic with comprehension axioms. It is a
system using first order logic.

On May 11, 6:58 pm, kleptomaniac6... at (no spam) hotmail.com wrote:
I mean second order arithmetic with comprehension axioms.
It is a system using first order logic.

Simpson treats second-order arithmetic as a first-order axiomatic
theory Z2, formulated in a (two-sorted) first-order language L2
(an extension of the usual first-order language of arithmetic,
obtained by adding atomic formulas of the form neX,
where n is a number variable and X is a set variable).
The axioms of Z2 are the usual first-order axioms
of Peano Arithmetic plus,
(i) Induction Axiom:
(ii) Full 2nd Order Comprehension Scheme:
EXAn[neX<-->phi(n)]

Look, my basic question, although a kind of weird one,
was what kind of system T would you get if you wrote down
the axioms for full second order arithmetic Z2 (the system
from reverse mathematics),

and then scribbled out the induction axiom,

and added "the first order arithmetic consequences of full
second order arithmetic"?

On May 15, 4:06 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:



On 2008-05-13, in sci.logic, Chris Menzel wrote:

On Tue, 13 May 2008 10:17:38 GMT, Aatu Koskensilta
aatu.koskensi... at (no spam) xortec.fi> said:
On 2008-05-11, in sci.logic, george wrote:

2nd-order logic *already has* a definition, and it *is not* in terms
of "comprehension".

It is apparent you simply don't know what you're talking about. Why,
then, go on about it, shouting random words in capitals with gay
abandon?

Curiously, he only used asterisks there. Perhaps his fingers are hoarse.

Ah, 'tis easily explained; I simply left out the portion of George's
post in which he indulged in his adorable habit of wanton shouting,
for it pains the sensitive eye so. Your observation is most observant,
though, revealing as it does some subtle distinction between emphasis
and shouting in proper Greenery.

Aatu, this is a slightly unrelated general query but I recall you
mentioned a while ago the system you would get by adding schematically
the apparatus for third order, fourth order, and generally nth order
arithmetic to second order arithmetic, to get the so called "omega
order arithmetic". If I recall correctly you said it was closely
related to Zermelo set theory. I have also read about systems of
simple, and non-simple type theory. How does "omega order arithmetic"
relate to such systems?

On May 15, 4:06 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:



On 2008-05-13, in sci.logic, Chris Menzel wrote:

On Tue, 13 May 2008 10:17:38 GMT, Aatu Koskensilta
aatu.koskensi... at (no spam) xortec.fi> said:
On 2008-05-11, in sci.logic, george wrote:

2nd-order logic *already has* a definition, and it *is not* in terms
of "comprehension".

It is apparent you simply don't know what you're talking about. Why,
then, go on about it, shouting random words in capitals with gay
abandon?

Curiously, he only used asterisks there. Perhaps his fingers are hoarse.

Ah, 'tis easily explained; I simply left out the portion of George's
post in which he indulged in his adorable habit of wanton shouting,
for it pains the sensitive eye so. Your observation is most observant,
though, revealing as it does some subtle distinction between emphasis
and shouting in proper Greenery.

Aatu, this is a slightly unrelated general query but I recall you
mentioned a while ago the system you would get by adding schematically
the apparatus for third order, fourth order, and generally nth order
arithmetic to second order arithmetic, to get the so called "omega
order arithmetic". If I recall correctly you said it was closely
related to Zermelo set theory. I have also read about systems of
simple, and non-simple type theory. How does "omega order arithmetic"
relate to such systems?

On May 27, 10:40 pm, Rupert <rupertmccal... at (no spam) yahoo.com> wrote:





On May 28, 12:28 am, kleptomaniac6... at (no spam) hotmail.com wrote:

On May 27, 2:09 pm, Rupert <rupertmccal... at (no spam) yahoo.com> wrote:

On May 27, 6:58 pm, kleptomaniac6... at (no spam) hotmail.com wrote:

On May 27, 12:33 am, Rupert <rupertmccal... at (no spam) yahoo.com> wrote:

On May 17, 6:57 am, kleptomaniac6... at (no spam) hotmail.com wrote:

On May 15, 4:06 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:

On 2008-05-13, in sci.logic, Chris Menzel wrote:

On Tue, 13 May 2008 10:17:38 GMT, Aatu Koskensilta
aatu.koskensi... at (no spam) xortec.fi> said:
On 2008-05-11, in sci.logic, george wrote:

2nd-order logic *already has* a definition, and it *is not* in terms
of "comprehension".

It is apparent you simply don't know what you're talking about. Why,
then, go on about it, shouting random words in capitals with gay
abandon?

Curiously, he only used asterisks there.  Perhaps his fingers are hoarse.

Ah, 'tis easily explained; I simply left out the portion of George's
post in which he indulged in his adorable habit of wanton shouting,
for it pains the sensitive eye so. Your observation is most observant,
though, revealing as it does some subtle distinction between emphasis
and shouting in proper Greenery.

Aatu, this is a slightly unrelated general query but I recall you
mentioned a while ago the system you would get by adding schematically
the apparatus for third order, fourth order, and generally nth order
arithmetic to second order arithmetic, to get the so called "omega
order arithmetic". If I recall correctly you said it was closely
related to Zermelo set theory. I have also read about systems of
simple, and non-simple type theory. How does "omega order arithmetic"
relate to such systems?

Omega order arithmetic is the resulting of adding the Peano axioms
(including a second-order induction axiom) to simple type theory..
Zermelo set theory is of approximately equal strength but slightly
stronger; it can prove the consistency of this system.

Okay, so how exactly does the non-simple type theory differ from the
simple type theory?

With simple type theory given one type T you have a type consisting of
all sets of objects of type T, and you have unrestricted comprehension
for the immediately higher type. With ramified type theory the sets of
objects of type T are divided into orders and you do not have
unrestricted comprehension. The resulting theory is a lot weaker.
Russell postulated the axiom of reducibility which effectively reduces
ramified type theory to simple type theory. We were talking about this
a few months back. Aatu posted some references which we could dig up
for you if you like. Reading the opening chapters of "Principia
Mathematica" might be helpful.

Ah, OK, that was when Russell wanted to avoid the so-called
"impredicative definitions".

Looking up on wikipedia about a simple theory of types, I came across
the following phrase: "Quantified variables range over only one type;
hence the underlying logic is first-order logic". What other logics
are being excluded here?

It's classical logic as opposed to intuitionistic, many-sorted as
opposed to one-sorted, and first-order as opposed to zeroth-order.
Saying that the underlying logic is first-order logic is a bit strange
in some ways because that means that you are counting the
comprehension axioms as nonlogical axioms.

Okay. I have never really understood very well the distinction between
second order arithmetic as described in the wikipedia article of the
same name, and second order arithmetic with second order logic.- Hide quoted text -

- Show quoted text -

On May 28, 5:45 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:





On 2008-05-28, in sci.logic, kleptomaniac6... at (no spam) hotmail.com wrote:

I dug up what Aatu said:
"Omega-order arithmetic, which allows sets of naturals, sets
of sets of naturals, sets of sets of sets of naturals and so on, is
equivalent to Zermelo set theory. Indeed, Zermelo set theory is not
conceptually particularly natural except when viewed in this light"

Are you talking about the same system?

Yes, and Rupert is correct. It is provable in Zermelo set theory, by a
simple induction argument, that for any n, there is a set that is the
result of iterating the powerset operation n times starting with the
naturals. For any finite subset of the axioms of omega-order
arithmetic there is then a model, and by compactness omega-order
arithmetic is consistent.

--
Aatu Koskensilta (aatu.koskensi... at (no spam) xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Okay. But what reason is there to say they are of approximately equal
strength?- Hide quoted text -

- Show quoted text -

On May 27, 3:22 pm, kleptomaniac6... at (no spam) hotmail.com wrote:
Okay. I have never really understood very well the distinction between
second order arithmetic as described in the wikipedia article of the
same name, and second order arithmetic with second order logic.-

On May 27, 8:21 pm, Rupert <rupertmccal... at (no spam) yahoo.com> wrote:
I don't think there is a distinction;

the issue is just which axioms
you count as logical axioms.

On May 27, 3:22 pm, kleptomaniac6... at (no spam) hotmail.com wrote:
Okay. I have never really understood very well the distinction between
second order arithmetic as described in the wikipedia article of the
same name, and second order arithmetic with second order logic.-
On May 27, 8:21 pm, Rupert <rupertmccal... at (no spam) yahoo.com> wrote:
I don't think there is a distinction;

OF COURSE there is a difference.

 the issue is just which axioms
you count as logical axioms.

That is not an issue and that is not the difference.
The difference IS EXPLAINED in the wikipedia article ITSELF,
so the original question is wrong in talking about the difference
between 2nd-order arithmetic "as described in the wikipedia article"
and anything else, the point being that there are differences WITHIN
the wikipedia article -- the article correctly talks about DIFFERENT
ways
of doing it.   Specifically, the article explains the difference this
way:

Semantics

Several different interpretations of the quantifiers are possible. If
second-order arithmetic is studied using the full semantics of second-
order logic then the set quantifiers range over all subsets of the
range of the number variables. If second-order arithmetic is
formalized using the semantics of first-order logic then any model
includes a domain for the set variables to range over, and this domain
may be a proper subset of the full powerset of the domain of number
variables.

Although second-order arithmetic was originally studied using full
second-order semantics, the vast majority of current research treats
second-order arithmetic in first-order predicate calculus. This is
because the model theory of subsystems of second-order arithmetic is
more interesting in the setting of first-order logic.

On Jun 3, 2:57 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:
On 2008-05-30, in sci.logic, kleptomaniac6... at (no spam) hotmail.com wrote:

So is it the case that in simple type theory with PA you cannot have,
for instance, the set consisting of all natural numbers and sets of
natural numbers, or the Cartesian product NxR?

Yes. However, using standard coding tricks talk of such sets can be
formulated in terms of sets of naturals, sets of sets of naturals, and
so on.

The difference between Zermelo set theory and omega-order arithmetic
is that in Zermelo set theory we can quantify over sets of arbitrary
order, while in omega-order theory all quantifiers are restricted to
sets of some specific order. In omega+1-order arithmetic, on the other
hand, we can quantify over sets of arbitrary finite order, and thus
carry out any argument that goes through in Zermelo set
theory.

There is no quotable example of a theorem in ordinary mathematics that
was expressible in the omega-order language of arithmetic and provable
in Zermelo set theory but not in omega-order arithmetic.

--
Aatu Koskensilta (aatu.koskensi... at (no spam) xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

What about ordered pairs? Presumably you couldn't have (5,9) defined
as {5,{5,9}} anymore.

On Tue, 3 Jun 2008 10:27:59 -0700 (PDT), kleptomaniac6... at (no spam) hotmail.com
kleptomaniac6... at (no spam) hotmail.com> said:



On Jun 3, 2:57 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:
On 2008-05-30, in sci.logic, kleptomaniac6... at (no spam) hotmail.com wrote:

So is it the case that in simple type theory with PA you cannot have,
for instance, the set consisting of all natural numbers and sets of
natural numbers, or the Cartesian product NxR?

Yes. However, using standard coding tricks talk of such sets can be
formulated in terms of sets of naturals, sets of sets of naturals, and
so on.

The difference between Zermelo set theory and omega-order arithmetic
is that in Zermelo set theory we can quantify over sets of arbitrary
order, while in omega-order theory all quantifiers are restricted to
sets of some specific order. In omega+1-order arithmetic, on the other
hand, we can quantify over sets of arbitrary finite order, and thus
carry out any argument that goes through in Zermelo set
theory.

There is no quotable example of a theorem in ordinary mathematics that
was expressible in the omega-order language of arithmetic and provable
in Zermelo set theory but not in omega-order arithmetic.

--
Aatu Koskensilta (aatu.koskensi... at (no spam) xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

What about ordered pairs? Presumably you couldn't have (5,9) defined
as {5,{5,9}} anymore.

The usual definition (from Kuratowski) is {{5},{5,9}}.

On Tue, 3 Jun 2008 10:27:59 -0700 (PDT), kleptomaniac6... at (no spam) hotmail.com
kleptomaniac6... at (no spam) hotmail.com> said:



On Jun 3, 2:57 pm, Aatu Koskensilta <aatu.koskensi... at (no spam) xortec.fi
wrote:
On 2008-05-30, in sci.logic, kleptomaniac6... at (no spam) hotmail.com wrote:

So is it the case that in simple type theory with PA you cannot have,
for instance, the set consisting of all natural numbers and sets of
natural numbers, or the Cartesian product NxR?

Yes. However, using standard coding tricks talk of such sets can be
formulated in terms of sets of naturals, sets of sets of naturals, and
so on.

The difference between Zermelo set theory and omega-order arithmetic
is that in Zermelo set theory we can quantify over sets of arbitrary
order, while in omega-order theory all quantifiers are restricted to
sets of some specific order. In omega+1-order arithmetic, on the other
hand, we can quantify over sets of arbitrary finite order, and thus
carry out any argument that goes through in Zermelo set
theory.

There is no quotable example of a theorem in ordinary mathematics that
was expressible in the omega-order language of arithmetic and provable
in Zermelo set theory but not in omega-order arithmetic.

--
Aatu Koskensilta (aatu.koskensi... at (no spam) xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

What about ordered pairs? Presumably you couldn't have (5,9) defined
as {5,{5,9}} anymore.

The usual definition (from Kuratowski) is {{5},{5,9}}.