[FOM] Predicativity, constructivity, Kruskal
spitters at cs.ru.nl
Sun Apr 2 16:41:51 EDT 2006
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
(I would like to mention that I had helpful offline discussions with Peter
Aczel and Thierry Coquand, of course all errors are mine.)
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
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
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
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
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
* 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.]
More information about the FOM