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.

  • 2
    $\begingroup$ I am nowhere close to expert, but have you consulted papers by Soloman Feferman? Possibly the first two papers listed in the references here math.stanford.edu/~feferman/papers/ResponseToHellman.pdf would be relevant. As you might already know, there is not universal agreement on what predicative mathematics means; for example MO user Nik Weaver has argued vigorously against the Feferman-Schuette analysis. Hopefully he or another expert will show up here to address your question (which is excellent by the way). $\endgroup$ – Todd Trimble May 10 '14 at 12:06
  • $\begingroup$ @Todd Thank you! I've seen Feferman's entry in the "Handbook of the Philosophy of Mathematics and Logic" but not the papers, will try to get them too. What's in the Handbook is an example of what I said - very well written, understandable, with lots of examples, but for a mathematician like me way too informal to make me feel confident... $\endgroup$ – მამუკა ჯიბლაძე May 10 '14 at 13:41
  • $\begingroup$ I had expected to see Per Martin-Lof mentioned here rather than Sol Feferman. Are different meanings of (im)predicativity being discussed here? $\endgroup$ – Paul Taylor May 11 '14 at 8:41
  • $\begingroup$ @Paul Definitely if there are different meanings I want to hear them all :) $\endgroup$ – მამუკა ჯიბლაძე May 11 '14 at 9:01
  • 2
    $\begingroup$ I'm reminded of the multilingual comments in this thread: mathoverflow.net/a/16957/2926 Google translate is fun because the results are sometimes pretty funny. When I applied it to Georges Elencwajg's comment in Russian, it began "Expensive colleges, ..." (pretty sure it was supposed to be "Dear colleagues, ..."). $\endgroup$ – Todd Trimble May 11 '14 at 21:34

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.

  • $\begingroup$ Thank you! I decided to accept this one - your link certainly contains a rigorous description of certain formal system and its distinguishing properties. I have to study it carefully before I can decide whether it is understandable for me :D $\endgroup$ – მამუკა ჯიბლაძე May 14 '14 at 6:50

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.

  • $\begingroup$ Thank you for the informative answer! You are right, your exposition is very clear but I am looking for some more formal approach. Let me also try to read some of the intriguing references in your links, I will then (hopefully :) ) return back with further comments/questions $\endgroup$ – მამუკა ჯიბლაძე May 11 '14 at 5:37

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.

  • $\begingroup$ I hadn't seen this paper by Smith. It's really nice! He is sophisticated, clever, witty, and in my opinion, absolutely spot-on. I wish I could write like that. $\endgroup$ – Nik Weaver May 12 '14 at 3:21
  • 1
    $\begingroup$ However, I think you have slightly misinterpreted him (at least I hope so). I don't see anything in the paper about predicativism only amounting to accepting conservative extensions of PA. Rather, when he talks about "going beyond ACA${}_0$" I think he means "passing to full second order arithmetic and beyond". $\endgroup$ – Nik Weaver May 12 '14 at 3:23
  • $\begingroup$ At any rate, there's nothing in the paper to suggest that a predicativist given the natural numbers couldn't go beyond PA to the extent of accepting PA + Con(PA), for example. The whole business of ordinal analysis is about this kind of relatively modest extension. $\endgroup$ – Nik Weaver May 12 '14 at 3:24
  • $\begingroup$ @NikWeaver, see the end of page 3. Smith's primary argument is that: if you are realist about that mathematics which is indispensable for science, then you are committed to ACA$_0$. Smith would probably argue that this does not commit you to Con(PA), since that is not needed for science. I don't like the whole argument about indispensability and commitment myself, but Smith endorses it as a meaningful argument, and Weyl and Feferman have done much the same. $\endgroup$ – Matt F. May 12 '14 at 22:28
  • $\begingroup$ E.g. Weyl at the very end of Das Kontinuum: "um exakte Wissenschaft solcher Gegenstandsgebiete zu ermöglichen, in denen Kontinua eine Rolle spielen", to make possible an exact science of those subject areas in which continua play a role. archive.org/stream/daskontinuumkrit00weyluoft/… $\endgroup$ – Matt F. May 12 '14 at 22:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.