FOM: HA*

[Neil Tennant]

Both Bill Tait and Sol Feferman have asked what the system HA* is, so here
is a reference:

H. Friedman and A. Scedrov, `Arithmetic Transfinite Induction and
Recursive Well Orderings', Advances in Mathematics, Vol. 56, No. 3, June
1985, pp. 283-294.  

The definition is given on p. 286 supra:

	HA* is obtained from HA by adding the schemata TI(R,A)
	for all well-founded primitive recursive (binary) relations
	(on natural numbers). Equivalently ... one can allow all 
	recursive well founded relations, given by their recursive
	indices. In fact, it suffices to let R be a primitive recursive
	well-ordering, i.e., a well-founded ordering linear on its field.

The schema TI(R,A) is in the language of HA (p. 285 infra):

	forall n (forall m (mRn -> A(m)) -> A(n))  ->  forall n A(n).

The main result of interest, to my mind, is part of Theorem 3.1 on p.292,
to the effect that for various strong intuitionistic theories T extending
HA (such as ZFI), T is conservative on arithmetic sentences over HA*.

Moreover, HA*, unlike its classical counterpart, is incomplete, although
complete for Pi_0_2 sentences. The schema of Church's Thesis

	forall n exists m A(n,m) -> exists e forall n A(n,{e}(n))

is consistent with and independent of HA*.

HA^omega is HA with the full omega rule. From p.287:

	From a classical viewpoint, HA^omega is the same as true
	arithmetic. From an intuitionistic viewpoint, it is not 
	clear what HA^omega is. In fact, under CT in the metatheory,
	it is equivalent to HA*.

These technical results reinforce the impression that the bivalence of
arithmetical truth has more to do with the use of classical logic than
with the constructive content of the numerical concepts involved, no
matter how strong the (intuitionistic) methods are by means of which we
derive assertions based on that content.

___________________________________________________________________
Neil W. Tennant
Professor of Philosophy and Adjunct Professor of Cognitive Science

http://www.cohums.ohio-state.edu/philo/people/tennant.html

Please send snail mail to:

		Department of Philosophy
		230 North Oval
		The Ohio State University
		Columbus, OH 43210

Work telephone 	(614)292-1591 
Private Fax 	(614)488-3198