Draft:Predicativism

This page is about Predicativism. For Impredicativism, contrary of Predicativism, see Impredicativity.

Predicativism is a philosophical concept formed by the three philosophers Henri Poincaré, Bertrand Russell and Hermann Weyl. By definition, it is a concept that rejects the definitions that rely on totality, meaning definitions that describe something to referring to the set that it belongs to. Russell was first to bring a slogan related to the idea; "Vicious circle principle". This principle explains thus:

"No class can contain elements which are definable only in terms of the class itself. Another way to say this is that we do not accept any entity which cannot be defined without referring to a class to which it belongs."

History

The idea of predicativism originated in the early 20th century as a foundational response to various set-theoretic paradoxes, including those of Cantor, Burali-Forti, and Richard. Henri Poincaré, Bertrand Russell, and Hermann Weyl each maintained that mathematical definitions must not involve circularity—specifically, they must not refer to totalities that include the object being defined. In 1906, Poincaré formulated what became known as the vicious-circle principle: no object should be defined by quantifying over a collection that includes that very object. Russell arrived at a similar conclusion independently, stating that whatever pertains to a class must not be a member of that class itself.

This distinction led to the notion of impredicative versus predicative definitions. A definition is impredicative if it defines an object using a totality that includes the object. For example, saying “n is the smallest number not definable in fewer than twenty words” is impredicative because it refers to the set of all definable numbers, including n itself. Conversely, a definition is predicative if it avoids such self-reference. Poincaré rejected impredicative definitions because they presuppose completed infinities—that is, they assume that all mathematical objects exist as a whole in advance. His position was that mathematical entities should be constructed incrementally from prior, already-defined objects, thereby avoiding circularity.

Hermann Weyl advanced this program in his 1918 work Das Kontinuum, which presented a rigorous predicative reconstruction of real analysis. He shared Poincaré’s “definitionist” view, insisting that all mathematical objects must be explicitly defined, with the sole exception of the natural numbers, which he treated as a fundamental, undefinable base. Weyl rebuilt substantial portions of classical 19th-century analysis—including the existence of maxima and minima, the mean-value theorem, Riemann integration, and the fundamental theorem of calculus—without impredicative set constructions. His system corresponds to the second-order arithmetic subsystem ACA₀ (Arithmetical Comprehension Axiom), which is predicatively valid. This system can be formalized by the second‐order arithmetic subsystem ACA₀ (arithmetical comprehension). Although Weyl’s work was soon eclipsed by Brouwer’s intuitionism and Hilbert’s formalist program, the foundational interest in predicativism was revived decades later by Solomon Feferman. Beginning in the 1960s, Feferman offered precise formalizations of predicative systems and demonstrated that key principles in arithmetic—such as induction and categoricity—can be justified without appealing to impredicative reasoning. This demonstrated that, contrary to the prevailing view, substantial and rigorous mathematical foundations are attainable within a predicative framework.

Formal system of predicativism

• Weyl's system: Weyl, in 1918, developed a system that allows reasoning about sets of real numbers, but only those that can be clearly defined (i.e., no vague or circular definitions). This system is similar to a logical system called $ACA_{0}$, which only allows sets defined using basic arithmetic formulas. Weyl showed that most of 19th-century real analysis (which deals with continuous functions and limits) can be done in this system. However, more advanced topics like modern Banach or Hilbert spaces, which involve more complex functions, cannot be handled here.

• Ramified analysis Feferman-Schütte hierarchy: Inspired by Poincaré’s idea of building up mathematics step by step, Kreisel and Feferman designed a system where each new level of reasoning is allowed only after proving that the step is safe. These levels are labeled by ordinals (which are a way to count far beyond natural numbers). The key limit is an ordinal called Γ₀ (Gamma-zero), which marks the boundary of what can be justified without circular reasoning (i.e., predicatively). Systems like $ACA_{0}$ stay below this boundary, while $ATR_{0}$ (Arithmetic Transfinite Recursion), which is just one axiom, reaches exactly $\Gamma _{0}$ and can prove statements that $ACA_{0}$ cannot. So, $ATR_{0}$ is considered to lie at the outer edge of predicative reasoning.

• Subsystem of second-order arithmetic: In the study of the foundations of mathematics, some simplified systems are used to classify how much strength a theory has. Predicative mathematics mostly fits inside weaker systems like $RCA_{0}$, $WKL_{0}$, and $ACA_{0}$. These systems are built on different assumptions about what sets exist. ACA₀ is particularly important—it’s powerful enough for most of classical analysis as Weyl knew it and is seen as the exact match for predicative analysis. Feferman also introduced more advanced but still predicative systems, such as EFSC and EFSC*, which extend basic number theory with carefully controlled sets. Other systems like IR and the W hierarchy add structured types but remain within predicative limits by avoiding definitions that refer to themselves.

• Constructive and explicit system: Predicative reasoning overlaps with some types of constructive mathematics, which focus on building objects step by step. For example, Bishop’s constructive mathematics fits well within predicative limits. Feferman’s theory of explicit mathematics also works this way—it’s a framework for talking about operations and classes in a way that avoids impredicative definitions. A specific version, called $\Gamma _{0}$, has the same strength as $ACA_{0}$ and thus aligns with predicative thinking. These systems highlight how predicativism supports both computational clarity and rigorous logic.

Predicative vs Impredicative system

Predicative systems avoid circular definitions. A definition is predicative if it only talks about sets or numbers that are already known or "smaller" in some clear way—either constructively or within a hierarchy.

By contrast, impredicative definitions allow you to define something by referring to a total collection that includes the object being defined. This can lead to circularity. For example, in second-order arithmetic or Zermelo–Fraenkel set theory (ZF), it's possible to define a set by talking about all sets, even if the one you're defining is part of that collection. This is considered impredicative.

The Internet Encyclopedia of Philosophy put it this way:

"A definition is impredicative if it generalizes over a totality to which the entity being defined belongs. Otherwise, it is predicative."

— 

Historically, mathematicians like Poincaré, Russell, and Weyl thought impredicative definitions were flawed or logically circular. However, later thinkers like Gödel accepted them, especially under a philosophical stance called realism (which assumes mathematical objects exist independently of us).

In terms of strength, impredicative systems are more powerful—they can prove more theorems. In reverse mathematics, many theorems from real analysis require impredicative principles (like full arithmetical comprehension or $\Pi _{1}^{1}$-comprehension). On the other hand, most predicative results can be handled in weaker systems like $WKL_{0}$ or $ACA_{0}$.

Rule in foundation and proof theory

Predicative arithmetic has been central to the development of foundational and proof-theoretic research, especially in clarifying the extent of mathematics that can be carried out without invoking impredicative assumptions. Unlike Hilbert’s program, which accepted the full scope of classical logic while seeking finitary consistency proofs, predicativism imposes a stricter philosophical constraint: definitions must not be circular or reference totalities containing the defined object. Despite this restriction, Solomon Feferman and Geoffrey Hellman demonstrated that core arithmetic truths—including the Peano axioms, mathematical induction, and the categoricity of the natural numbers—can all be established within a predicative framework.

Throughout the twentieth century, predicative analysis became a focal point in reverse mathematics and broader foundational investigations. A key discovery in this area is that many classical mathematical theorems are equivalent either to ACA₀ (arithmetical comprehension axiom), which is predicatively acceptable, or to stronger, impredicative subsystems. Feferman noted that systems like ACA₀ and WKL₀ (Weak König’s Lemma) account for a wide range of results in real analysis, all of which fall within the proof-theoretic strength of primitive recursive arithmetic (PRA) or Peano arithmetic (PA).

Application and consequences

• Logic and reverse mathematics: The study of second-order arithmetic subsystems ($RCA_{0}$, $WKL_{0}$, $ACA_{0}$, $ATR_{0}$, etc.) is guided by predicative constraints. $ACA_{0}$ and Feferman’s IR represent predicative systems, while stronger ones like $\Pi _{0}^{1}-CA_{0}$ are impredicative. For example, statements like “every uncountable closed set has a perfect subset” or the comparability of countable well-orderings are equivalent to $ATR_{0}$, which exceeds predicative strength. In proof-theoretic terms, predicative systems are bounded by $\Gamma _{0}$, marking the limit of consistency strength achievable without impredicative methods.

• Computer science and type theory: Predicative principles appear in type-theoretic and computational settings. Many typed lambda calculi and proof assistants (e.g. predicative versions of Martin-Löf type theory) avoid impredicative universe constructions to ensure consistency. Predicative systems correspond to definable or computable classes: for example, Feferman’s theory of explicit mathematics $T_{0}$(predicative) is essentially the theory of computable functions (PA) in second-order guise. In complexity theory, “safe” or predicative recursion schemes characterize feasible (polynomial-time) functions. While not always discussed under the label “predicative arithmetic,” these computational frameworks share the same spirit of forbidding circular definitions.

• Constructive mathematics: There is a strong affinity between predicative and constructive approaches. Feferman observes that Bishop’s constructive analysis (BCM) can be viewed as a refinement of classical analysis on predicative grounds. In practice, many constructive theorems do not require impredicative existence proofs and align with predicative systems. Feferman’s survey notes substantial “predicative redevelopments” of analysis post-1960, paralleling constructive efforts, although he laments the lack of comprehensive texts on this. Both schools reject non-constructive omniscience principles, but predicativism allows classical logic (unlike intuitionism), aiming to salvage as much of classical mathematics as possible under predicative restrictions.

Comparison of formalization and limits

Formalizations of predicative arithmetic vary in strength. At the base is PRA (primitive recursive arithmetic), consistent with strict finitism. $RCA_{0}$ and $WKL_{0}$ are also predicatively acceptable. $ACA_{0}$, which includes full arithmetical comprehension, is stronger and still predicative. $ATR_{0}$ goes further by admitting transfinite recursion up to countable ordinals; it is not strictly predicative, as it proves the well-foundedness of all $\Gamma _{0}$-orderings, but it is predicatively reducible—any Π⁰₁ theorem it proves can be derived within a system like Feferman’s IR.

The Feferman–Schütte ordinal $\Gamma _{0}$ marks the standard boundary of predicative provability: systems with proof-theoretic ordinals below $\Gamma _{0}$ (like ACA₀ or $\Sigma _{1}^{0}-DC$. + bar induction) are predicatively justified. Systems equiconsistent with $ATR_{0}$ or $\Pi _{1}^{0}-CA_{0}$ surpass this bound. Some, like Nik Weaver, argue for broader interpretations of predicativity extending to ordinals like $\phi _{\omega }^{\Omega }$(0), but this remains disputed. In summary, predicative systems range from $ACA_{0}$ (fully predicative) to ATR₀ (predicatively reducible), while $\Pi _{1}^{0}-CA_{0}$ and beyond are impredicative, with ordinals like $\Omega ^{CK}$ and $\Gamma _{0}$ marking transitions in logical strength.

Reference

This page will be placed in the following categories if it is moved to the article namespace.

Categories:

• Mathematical analysis