Skip to main content
1 of 2
Carl Mummert
  • 9.7k
  • 1
  • 46
  • 68

Andrej Bauer points out that predicative constructions are more explicit and give more useful computational information, than impredicative ones. This has two further consequences that are of interest. I want to point these out as an answer to the implicit question asked by "alephomega".

  1. If a theorem about reasonable objects can be proven predicatively, this gives important information on the consistency strength (i.e. the proof-theoretic ordinal) associated with the theorem. Conversely, we know that some theorems such as Kruskal's theorem cannot be proven predicatively because these theorems lead to proof-theoretic ordinals that are too large. Thus the mathematical analysis of predicativity reveals the full complexity of results such as Kruskal's theorem, rather than obscuring it. This is separate from the philosophical analysis of predicativity.

  2. The "computability" consequences of a predicative proof can be extremely important. In the context of a countable group $G$, a "top-down" construction such as "intersect all subgroups of $G$ that contain the set $X$" will only naively give that the constructed object is $\Pi^1_1$ over $G\oplus X$. A bottom-up construction will usually show that the constructed object is actually arithmetical in G. Examination of the bottom-up proof can then give explicit bounds in the arithmetical hierarchy on the complexity of the constructed object. For example, in the case of a subgroup of a group $G$ generated by a subset $X$, the degree of the subgroup is no more than the Turing jump of $G \oplus X$; this is an enormously better bound than the naive $\Pi^1_1$ result.

Carl Mummert
  • 9.7k
  • 1
  • 46
  • 68