[FOM] on Bas Spitters on "constructive impredicativity?"

[Harvey Friedman]

On 3/31/06 4:00 AM, "Bas Spitters" <spitters at cs.ru.nl> wrote:

> On Thursday 30 March 2006 21:43, Gabriel Stolzenberg wrote:

>>    As I recall, part of the story was that Harvey had proved that
>> every proof of Kruskal's theorem requires impredicativity.  Obviously,
>> I must be mistaken about this.  Is there some other result with which
>> I may be confusing this?

No, Stolzenberg is absolutely right about this.
> 
> There seem to be two issues here, Harvey can correct me if I am wrong.
> 1. Veldman proved, intuitionistically, Kruskal's theorem (as in the `theorem
> proved by Kruskal'). Harvey showed that an extension of this theorem with a
> `gap condition' cannot be proved in a predicative system (in the sense of
> Feferman-Schutte).

I showed that already Kruskal's theorem (without gap condition) cannot be
proved predicatively, under the Feferman/Schutte analysis. In fact, it
cannot be proved in ACA0 + Pi12-BI.

Kruskal's theorem with gap condition is called EKT = extended Kruskal's
theorem. This uses a higher level of impredicativity. In particular, it is
provable in Pi11-CA but not in Pi11-CA0. Or it is provable in ID_omega but
not in ID_<omega. The graph minor theorem also cannot be proved in Pi11-CA0.

> 2. "Predicativity" as used by Feferman-Schutte refers to a level of
> proof-theoretic strength. By type theorists the term is used for a kind of
> "non-circularity in definitions", as it was used originally by Russell.
> Martin-Löf's type theory  with enough inductive definitions is
> "impredicative" according to Feferman. In this sense one can say that there
> is a "predicative" (ie non-circular) proof of the extended Kruskal theorem.

I strongly recommend, for historical and other reasons, that people refrain
from using "predicative" for anything not falling under the scope of the
much much older and classically accepted analysis of Feferman/Schutte.

I am quite doubtful that you can prove Kruskal's theorem in anything that
Russell would have called "non-circularity in definitions". How does
Russell's idea of "non-circularity in definitions" differ from what is
classically called "predicativity"?

Harvey Friedman