Formal/rigorous treatment of (im)predicativity/predicativism

Question

There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative definition and Impredicativity)

Still I must confess I do not understand the concept well enough. All I've seen is a verbal explanation with a bunch of very clear examples. And being used to mathematics, I feel uncertain about it until I will have some formally defined entity, preferably some mathematical model of its behavior.

For example, I don't know whether there is a definition of predicativity which is sufficiently formal so that given a formula in any language whatsoever one would be able to tell whether it is predicative or not. I don't even know whether it makes sense to speak about predicativity of a formula since I've only seen discussions of (im)predicative definitions.

Seemingly predicativism must be closely related to constructivism, and again I could not find descriptions of precise relationship between these two. One of the things confusing me here is that e. g. in a programming language one might have perfectly correct self-referential construction of a datatype, so this seemingly will produce an example of a constructive impredicative definition.

Also I have vague feeling that predicativity must be somehow related to induction, in particular that any inductive definition must be predicative. Does this make sense and if yes is it correct? What about coinduction, is it related?

So to summarize, are there texts addressing these and similar questions from purely mathematical viewpoint? In particular, texts with systematic purely formal treatment of (im)predicativity? Ideal would be some mathematical (say, algebraic) structure which models behaviour of predicative vs. impredicative whatevers.

And let me add that although I've tagged this as reference request, I would be also grateful for on-the-spot explanations without any references.

Answer 1

I have a brief survey on predicativism here. But it may be more of the kind of "verbal" explanation that you've been unsatisfied with.

Maybe proof theoretic ordinals could provide the kind of rigorous account that you want. Are you familiar with this subject? The Wikipedia article might be a good place to start. The rough idea is that, given a formal system $S$ that interprets some minimal amount of number theory, we look at the recursive well-orderings of the natural numbers that can be proven to be well-orderings in $S$. The supremum of the corresponding ordinals is a countable ordinal which provides a basic measure of the deductive strength of $S$.

The relevance to your question is that, broadly speaking, systems with sufficiently small proof theoretic ordinal will be considered predicatively acceptable, while those whose proof theoretic ordinal is too large will not. As Todd alluded to in his comment, exactly where to draw the line, or whether there is an exact line to be drawn, has been controversial. However, there is no disputing that predicativism (in the historically primary sense that accepts countable constructions) sanctions Peano arithmetic, whose proof theoretic ordinal is $\epsilon_0$, and other systems in that neighborhood. Getting much beyond that point takes some work. I have argued here that predicatively acceptable constructions can get up to the small Veblen ordinal.

Answer 2

Solomon Feferman's papers provide formal systems for predicativity, most recently here. Other papers on his website and in his book In the Light of Logic have other expositions. These systems are predicative either by virtue of their ordinal analysis, or by virtue of being conservative over PA.

The subtypes $\{x\in T:\phi\}$ in these systems are the focal points for predicative restrictions. Either you can not form subtypes using $\phi$'s which quantify over types, or you can form those subtypes but don't have the axioms to prove much about them.

For examples, see the development of analysis in the cited paper. It proves the least upper bound principle for sequences of real numbers, but not for sets. The resulting development may be your best source for intuitions about predicativity which are backed up by a formal system.

Answer 3

Disclaimer: I'm just somebody who also tried to understand what is meant by predicativism, and have no other qualification for answering this question than having "browsed" some "writings" vaguely related to this question. I also use the words "predicative" and "impredicative" myself sometimes. While checking some papers by Randall Holmes, Adrian Richard David Mathias and Thomas Forster again during writing this answer, I noticed that I should not have used the word predicative to describe the simple theory of types TST and stratified formulas. They only conform to the weaker position of Frank P. Ramsey and Rudolf Carnap, who accepted the ban on explicit circularity, but argued against the ban on circular quantification.

---

What are impredicative definitions? In higher order logic, we want to turn predicates over "objects of rank $n$" into "objects of rank $n+1$". Henkin semantics has comprehension axioms ensuring the existence of objects corresponding to certain predicates. If a predicate over "objects of rank $n$" involves quantification over objects of rank $m>n$, then this predicate is defined impredicatively. By the predicative comprehension axiom scheme, one typically means the axiom scheme which ensures the existence of objects corresponding to all non-impredicative predicates. In the context of second order logic, the impredicative comprehension axiom scheme allows quantification over both first and second order variables.

It might make sense to distinguish between the philosophical position 'predicativism given the natural numbers', impredicative definitions (of "collections") and more general positions of 'predicativism' (related to ordinal analysis). Peter Smith argues convincingly that 'predicativism given the natural numbers' is a conceptually stable position that only amounts to accepting full first-order Peano Arithmetic and its (conservative) predicative extension $\mathsf{ACA}_0$. Peter Smith explicitly refers to Weyl's position from "Das Kontinuum" here. This position should not be confused with other uses of 'predicative reasoning (given the natural numbers)'. Nothing is said against these positions, but it gets clear that one can accept Weyl's position without in any way diminishing the case for not accepting stronger systems like $\mathsf{ACA}$.

There are also typical impredicative principles, like limitation of size or the unrestricted axiom schema of replacement. Let's say that these principles drastically increase the proof-theoretic consistency strength of the corresponding set theories. Hence from the point of view of ordinal-analysis, the distance to the "predicatively acceptable" systems is drastically increased, hence it makes sense to consider these as impredicative principles.