FOM: Questions on higher-order logic

[JoeShipman@aol.com]

Here are some precisely posed questions that might help make the current 
discussion more clearly focused.  In the following, "standard semantics" is 
assumed, and I am working in first-order ZFC, using the definition of 
"second-order validity in standard semantics" given in the first chapter of 
Manzano's book.

1)  For which ordinals alpha is  the the truth set for V(alpha) Turing 
reducible to the set of second-order validities? 

2) Is the set of second-order validities reducible to the truth set of 
V(alpha) for any  alpha?  This seems unlikely at first, because GCH, a 
statement about arbitrarily high ranks of sets, is equivalent to the validity 
of a particular second-order sentence.  On the other hand, we know that if 
GCH holds high enough up (a supercompact cardinal) then it holds universally, 
so maybe it's not so unlikely.

3) Is the set of validities for 3rd-order-logic or for type theory stronger 
under Turing reducibility than the set of validities for SOL?

4) Let X be the set of sentences phi of SOL such that ZFC proves that phi is 
a second-order validity.  Is there a "reasonable" deductive calculus for SOL 
whose set of derivable validities is not contained in X?  (Here "reasonable" 
means that simply replacing ZFC by ZFC+Y for some set-theoretic Y in the 
above won't do.  Unlike the other four questions, this one is necessarily 
imprecise.)

5) Let X be the set of second-order validities.  Let Y be the set of 
statements "phi is a second-order validity" for phi in X.  Let Z be the 
closure of Y under logical implication.  Are any theorems of ZFC outside of 
Z?  (Such a theorem would refute a form of logicism.)

-- Joe Shipman