FOM: Second-order logic -- exchange with Simpson

[Joe Shipman]

Shipman:

In your last post you allude to a set of axioms and inference rules for
second-order logic S without completely specifying it.  Choose your
favorite recursive S (e.g. with full 2nd order comprehension, your
favorite choice scheme, etc.).  We know that with respect to the
standard semantics, S is sound but incomplete.  Can you come up with a
sentence Phi that ZF proves is a second-order validity using the
standard semantics (or that ZFC proves is a validity if your S included
Choice) but which is not derivable from S?  Such a sentence would
exhibit the superiority of set theory to second-order logic, unless your
personal set of axioms and inference rules S can be augmented by other
*logically* motivated  ones to create a new system S' such that S' |-
Phi (in which case maybe S shouldn't have been your favorite system of
second-order logic).  Conversely, if you can't come up with such an
example, then the "incompleteness" of second-order logic doesn't seem
any more important than the incompleteness of first-order ZFC

++++++++++++++++++++++++++++++++++++++++++++++++++++++

Simpson:

 > Can you come up with a sentence Phi that ZF proves is a
 > second-order validity using the standard semantics (or that ZFC
 > proves is a validity if your S included Choice) but which is not
 > derivable from S?

How about Phi = Con(S)?

Let S(ZF) be the set of 2nd-order sentences A such that ZF proves that
A is valid with respect to the standard semantics.  I think that in
one of your postings you asked for a natural axiomatization of S(ZF).
Trivially S(ZF) is r.e. and therefore has a recursive axiomatization,
but I don't know of any natural recursive axiomatization of it.  I
didn't answer your posting, because I didn't have a good answer.

Of course S(ZF) is different from S(ZFC), S(ZF+V=L), etc etc, so one
would expect that a natural axiomatization of S(ZF) would somehow have
to include some sort of translation of ZF.  The method should then
also apply mutatis mutandis to give natural axiomatizations of
S(ZFC), S(ZF+V=L), etc.

+++++++++++++++++++++++++++++++++++++++++++++++++++++

Shipman:

>  > Can you come up with a sentence Phi that ZF proves is a
>  > second-order validity using the standard semantics (or that ZFC
>  > proves is a validity if your S included Choice) but which is not
>  > derivable from S?
>
> How about Phi = Con(S)?

Well, this will depend on what your S actually is.  Obviously S cannot
prove Con(S), the question is whether ZF can prove Con(S).  Is your
favorite S weaker than ZF? If so, how much weaker?  Is it weaker than Z?

> Of course S(ZF) is different from S(ZFC), S(ZF+V=L), etc etc, so one
> would expect that a natural axiomatization of S(ZF) would somehow have
> to include some sort of translation of ZF.  The method should then
> also apply mutatis mutandis to give natural axiomatizations of
> S(ZFC), S(ZF+V=L), etc.
>

Not necessarily -- a natural axiomatization of second-order logic might
turn out to have the same strength as ZF or ZFC even though it was in no
way motivated by set theory.  The first step towards investigating this
should surely be taking the most powerful second-order-logic proof system
out there and determining its logical strength.

A different kind of "strength" is measured by the Lowenheim number for
second-order logic (which is independent of the particular axiomatization
but may represent some sort of upper bound).  Nobody's answered this query
of mine either.

++++++++++++++++++++++++++++++++++++++++++++++++++++

Simpson:

> Well, this will depend on what your S actually is.  Obviously S cannot
> prove Con(S), the question is whether ZF can prove Con(S).  Is your
> favorite S weaker than ZF? If so, how much weaker?  Is it weaker than Z?

I don't have a favorite S.  In Shapiro's book, S is typically
something like first-order logic + full comprehension + full choice +,
optionally, the existence of a well-ordering of the universe.  This S
is of the same strength as Z_2, second-order arithmetic, provided you
define `strength' in an appropriate way.  So it is certainly weaker
than Z.  For this S you could take Phi to be something like `if X is a
set and E is a binary relation on X and (X,E) is isomorphic to
(V_omega,epsilon), then (X,E) satisfies Con(Z_2)'.  This Phi is not
provable in S (look at a model of Z_2 + not-Con(Z_2)), but ZF proves
that Phi is valid in second-order logic with the standard semantics.

> Not necessarily -- a natural axiomatization of second-order logic might
> turn out to have the same strength as ZF or ZFC even though it was in no
> way motivated by set theory.

I see obstacles to finding such an axiomatization.

+++++++++++++++++++++++++++++++++++++++++++++++++++++

Shipman:What obstacles?