FOM: Questions on higher-order logic

[JoeShipman@aol.com]

Dear Bob,

Thank you very much for your answers to my questions, which turned out as I 
expected.  Now that the technical situation is clarified, I can make my 
philosophical points:

My question:
>> 1)  For which ordinals alpha is  the the truth set for V(alpha) Turing 
reducible to the set of second-order validities? <<
  
Your answer (excerpted): 
>>  (a) If alpha is weakly characterizable, then the truth set of V(alpha) is 
Turing reducible to the set of second-order validities.
    (b) If V=L, then there is a countable ordinal alpha such that the truth 
set of V(alpha) is not recursive in the set of second order validities. 
[Indeed, if V=L, for every set of integers X, there is a countable ordinal 
alpha such that X is recursive in the truth set of V(alpha). If X is the 
beta^{th} real with respect to the usual well-ordering of the reals of L, it 
suffices to take alpha = omega + beta.] <<

Comment:
This shows that the set of second-order validities is a very informative set 
indeed, and that practically all mathematical questions not involving higher 
set theory are determined by (2nd-order) logic alone.  I am wondering if 
Borel Determinacy, which requires UNcountable ranks, might be the lowest 
reasonable exception (see further comments at question 5).

My question:
>> 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.<<
 
Your answer (excerpted):
>>  The answer to the question which is the first sentence of 2) is YES. 
Indeed, if gamma is the sup of the characterizable ordinals, then the set of 
second-order validities is recursive in the truth set of V(beta) for any beta 
which is >= gamma. 
... 
    I remark that if kappa is a strong cardinal [and a fortiori if kappa is 
supercompact], then kappa >  gamma. Indeed, if kappa is strong, then for 
every ordinal delta, there is a beta < kappa such that V(beta) is 
elementarily equivalent to V(delta).<<

Comment:
This is so high up that it is not easy to make the case that SOL is 
"reducible to set theory".  By the way, your last sentence implies that there 
are at most kappa "elementary equivalence classes" for kappa the first strong 
cardinal; how much can this be improved?  (Obviously there are at most 
continuum-many possible truth sets for V(delta) as delta ranges over the 
ordinals, but elementary equivalence is a stronger property than having the 
same true sentences.)


My question: 
>>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?<<
 
Comment:  Since the answer is no, we might as well stick to SOL and not 
higher types in this discussion.

My question:
>> 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.) <<
 
Your answer: 
>>  Instead of asking about second-order validities here you could ask about 
true assertions that a Turing machine doesn't halt. So I take it the question 
is really asking "Is there something fundamentally different than our 
intuitions about sets which can be brought to bear on such questions?
 
I certainly don't know of such a fundamental new concept. It would be rash to 
deny the existence of such a priori.<<

Comment:
You're right about what I'm "really asking", but it's not as good to just ask 
about assertions that a Turing machine doesn't halt, because I'm also 
interested in questions like GCH which is equivalent to the validity of a 
second-order sentence but has no new arithmetical consequences.  Even if we 
can't think of any way to get new arithmetical truths without going the large 
cardinal route, we might be able to address questions like GCH in another 
way.  (My own preferred new axiom is the existence of an atomless measure on 
the continuum, which gets you BOTH new arithmetical consequences and a 
refutation of CH; but for the purposes of this discussion I am contemplating 
"logical" axioms in the framework of SOL instead).

My question:
>> 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.)<<
 
Your answer:
>>  In what follows, I will sketch the proof that there is a theorem of ZFC 
which is not in Z.<<
 (Sketch of proof omitted)

This is the answer I expected but I am surprised that the theorem is so 
elaborate and  artificial.  It would be nice to be able to point to such a 
theorem that was of independent interest (such as Borel determinacy, which 
requires uncountably many iterations of the powerset operation to prove and 
so is not obviously equivalent to the validity of a sentence of SOL).


Conclusion:

Someone who accepts the notions of arbitrary subset and arbitrary relation on 
a set as clear and determinate is not going to be bothered by the argument 
that the set of second-order validities "depends on the underlying set 
theory", properly viewing that as set theory's problem rather than SOL's.  

The argument that there is no complete deductive calculus is also not so 
pertinent, because after all the completeness of the predicate calculus 
doesn't get you very far in the development of mathematics, you have to 
assume some nonlogical axioms and then you face incompleteness.  The appeal 
of SOL is that you seem to be able to get a long way without any "nonlogical" 
axioms.  

This logicist approach to FOM has many advantages.  It seems to me that there 
are only two good arguments against it relative to the standard foundations 
via 1st-order ZFC:

1) All the deductive calculi for SOL that I have seen don't seem to allow the 
derivation of anything you can't already get with ZFC, and furthermore I 
don't know any that approach ZFC's power except simply taking sentences phi 
which ZFC proves are 2nd-order validities (my 4th question was to clarify 
this; I'd like to be proved wrong here).

2) On the other hand, there ARE theorems of ZFC which could not be derived 
even with an oracle for second-order validity, so the ZFC approach is 
stronger in a sense (my 5th question was to clarify this, though I'd like to 
see a simpler example).

-- Joe Shipman