FOM: Reasoning in second-order logic -- two queries

[Joe Shipman]

Simpson:
>This is really a burden-of-proof issue.  If you claim that X is logic,
>then it's up to you to exhibit the axioms and rules of inference of X.
>In the case of X = so-called `second-order logic', nobody has done
>this.  Without this, to claim that `second-order logic' is logic is to
>rewrite the dictionary.

Can one define axioms and rules of inference for second logic that are
"natural" (i.e. logical rather than set-theoretical in concept and
motivation) that allow one to derive at least as many validities as ZF
does?  That is, that allow one to derive any sentence Phi such that ZF
|- "Phi is a second-order validity"?

What are the best known upper and lower bounds for the Lowenheim number
of second-order logic?

-- Joe Shipman