[FOM] Predicativity, constructivity, Kruskal

[Bas Spitters]

Dear Gabriel, Harvey, and others,

Both of you were, of course, right on Kruskal. It is not provable in the 
Feferman-Schutte system.  I'll elaborate on a few of the issues we discussed 
before, hoping not to introduce more confusion, and end with a question for 
Gabriel.
(I would like to mention that I had helpful offline discussions with Peter 
Aczel and Thierry Coquand, of course all errors are mine.)


Predicativity:
========
There seem to be at least four relevant levels here (in increasing strength):
1) FS: Feferman-Schutte
2) ID1: theory of inductive definitions (first level). This has the same 
strength as the Kleene-Vesley system FIM. This is what Wim Veldman used for 
his proof of the Kruskal theorem.
3) ID2, ID3, etc: All of these count as predicative in type theory (a la 
Martin-L"of).
4) HA2, IZF, quite definitely impredicative.
In what follows I'll write generalised predicative for stages 2 and 3. As 
mentioned before type-theorists tend to talk about just "predicative" in this 
case.

Coq type theory:
===========
Before I stated that the Coq type theory is predicative. Although this is the 
common terminology and I made some reservations, maybe I should elaborate.

Coq has two sorts, a non-computational one, Prop, and a computational one, 
Set. (In fact, it has infinitely many sorts, but I am simplifying a bit). Very 
little influence from a Prop-term on a Set-term is allowed.
The sort Prop is impredicative, in the sense that the Calculus of 
Constructions is. Set, by default, is not, it behaves much like Martin-L"of's 
type theory. 
There are, at least, two ways to encode the logic:
* Encode the logic in the sort Prop. This allows impredicative reasoning. 
However, the (intensional) axiom of choice seems not to be derivable, unlike 
usually in type theory. In fact, it seems that even the axiom of unique 
choice is not derivable.
* Encode the logic in the sort Set. This gives a generalised predicative type 
theory much like Martin-L"of's. Thus the (intensional) axiom of choice is 
derivable.

The Coq-developers call their type theory "predicative" when Set is 
generalised predicative(, but Prop is not). The version where both Prop and 
Set are impredicative is naturally called impredicative.

Since v8.0 (2005?) the default type theory in Coq is the "predicative" one.

Question for Gabriel:
=============
On Monday 27 March 2006, Gabriel Stolzenberg wrote:
> Now, I am very comfortable with impredicative
> definitions.  In fact, I think some of them are marvelous.

In the above terminology, which flavour of "impredicativity" did you have in 
mind? And what, in your opinion, would Bishop have agreed with?
* ID1: Bishop does seem to have used this in the definition of Borel set in 
his '67 book. Of course, this theory was later replaced by the Bishop-Cheng 
theory.
* more generalized inductive definitions, IDn, etc: This is what Thierry 
Coquand used in his proof of Kruskal's theorem that you liked and more 
generally what type theorists tend to be happy with.
* IZF: This is what Bishop may, or may not, have had in mind in his definition 
of the completion of a uniform space. At least, it seems natural to use the 
power set construction when reading this.
[This being said, I believe that there are constructions of the completion 
that do not use the powerset, in both constructive type theory and set 
theory. I'd have to look for the precise references.]

Bas