FOM: Questions on higher-order logic

[Robert M. Solovay]

Dear Joe,

	I am able to give answers to four of the five questions you raise.

On Thu, 31 Aug 2000 JoeShipman at aol.com wrote:

> 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? 

	I don't know a necessary and sufficient condition. But I can give
a sufficient condition that covers many examples.

	First, we say that alpha is characterizable if for some sentence
in the language of set-theory, alpha is the first ordinal beta such that
V(beta) models phi.

	Say that alpha is weakly characterizable if for some
characterizable ordinal beta greater than alpha, alpha is definable in
V(beta). [I am assuming that when we talk about V(alpha), we are talking
about the structure whose underlying set is V(alpha), and which has the
restriction of epsilon to V(alpha) as its only non-logical relation.]

	Then the following claims are easy to verify:

	(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.]

	As an example, if there are measurable cardinals, then the least
measurable cardinal is weakly characterizable but not characterizable.

> 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.

	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. 

	One simply asks if the second-order sentence whose validity one is
trying to ascertain is valid in V(beta). [A little fussiness is needed if
beta is not a limit ordinal to see this. I omit these details.]

	 In fact, the Turing jump of the set of second-order validities
is Turing reducible to the truth set of V(beta). This is obvious if beta
is greater than gamma [since then gamma is definable in V(beta)] and
fairly easy  even if beta = 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).

> 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?

	The answer is NO. This has been adequately explained by previous
respondents to your letter.

> 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.)

	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 certaintly don't know of such a fundamental new concept. It
would be rash to deny the existence of such a priori.

> 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.)

	In what follow, I will sketch the proof that there is a theorem of
ZFC which is not in Z.

	The first obervation is that there is a bound for the location of
members of Y in the Levy hierarchy. [This is completely evident since all
the members of Y are obtained by substituting the Godel numerals of
different sentences for phi in "phi is a second-order validity". In fact
these sentences are all Pi_2, but we won't need that.]

	Next we select a "sufficiently strong" finite subtheory T  of
ZFC. [Here "sufficiently strong" is whatever is needed to make the
following argument work. If you want definiteness, take all axioms of ZFC
whose Godel number is less than A(1000) where A is Ackerman's function.]

	Now we use the fact that there is a "partial truth
definition" which applies to all the axioms of T as well as to all the
sentences of X.

	Using this, we can formulate the following setnece Psi in the
language of ZFC. The theory whose axioms are X and the axioms of T is
consistent.

	Moreover, using the truth definition as well as cut-elimination,
one can easily prove Psi in ZFC. 

	Cut elimination is used to know that if
there is a proof of 0=1 in T + X, then there is one all of whose lines
have an a priori bound in the Levy hierarchy [say at most 2 more than the
bound on the axioms of T + X].

	But if Psi were provable from the sentences of X, we would get a
theory S able to prove its own consistency which was a subtheory of T +
X. S would consist of the axioms of T plus those members of X used in the
purported proof of Psi. But this would contradict Godel.

	I am using one slightly subtle fact here. We can choose T so that
it can prove all the 
	"snow is white" is true iff snow is white
theorems for any standard partial truth definition [even one that works
for the axioms of T.] The point is that T just has to be strong enough to
give the usual treatment of truth for Sigma_1 formulas for this to be so.

> -- Joe Shipman

	--Bob Solovay