8
$\begingroup$

The terms “constructivism”, “finitism” and “predicativism” refer to ideas / currents in the philosophy of mathematics (or loosely defined conditions on a system of logic) that I think I understand informally as follows:

  • constructivism demands that an existential statement can only be proved by exhibiting an object witnessing it, a condition that requires, at the very least, the abandonment of the principle of excluded middle;

  • finitism accepts only finite objects (essentially, those that can be coded as natural numbers), and an even more radical version of finitism, ultrafinitism, only accepts natural numbers of reasonable size (a notion difficult to formalize, but certainly an ultrafinitist would not necessarily agree that Ackermann's function, or even the exponential function, is total);

  • predicativism is something like the requirement of avoiding self-referencing definitions, i.e., the idea that mathematical objects can only be defined by reference to previously-defined objects (for some kind of well-founded order on definitions/constructions).

Now I don't know how to make the above precise (except perhaps constructivism by means of the existence and disjunction properties), but I think I have some examples of formal systems that meet these various requirements, e.g.:

  • $\mathsf{HA}$ (Heyting arithmetic) and $\mathsf{CZF}$ (constructive ZF) are constructive; $\mathsf{IZF}$, on the other hand, is only weakly constructive.

  • $\mathsf{PA}$ (Peano arithmetic) is finitist, because it only speaks of natural numbers, just like $\mathsf{ZFC}$ with the axiom of Infinity removed; on the other hand, full $\mathsf{ZFC}$ is certainly not finitist. Some very weak subsystems of $\mathsf{PA}$ might be acceptable to ultrafinitists: $\mathsf{EFA}$ (elementary function arithmetic) is probably still too strong to qualify as “ultrafinitist”, but probably some variations of Buss's systems of bounded arithmetic can be acceptable?

  • $\mathsf{KP}$ (Kripke-Platek set theory) is, I believe, predicative for some reasonable definition of “predicative” (though I'm not quite sure how precisely defined the word is).

Now from these examples it appears that there is little relation between the first two terms: $\mathsf{CZF}$ is constructive but not finitist (let alone ultrafinitist), and on the other hand, $\mathsf{PA}$ is finitist but not constructive, and various systems of bounded arithmetic might even be ultrafinitist still without being constructive; as for predicativism, I imagine it is implied by finitism (though even that is not so clear to me), but $\mathsf{KP}$, if it is predicative, is certainly not finitist nor constructive, and I'm not sure whether $\mathsf{CZF}$ qualifies as “predicative”.

However, there still seems to be some connection between them:

  • On the one hand, some figures sympathetic to one of these “currents” also tend to appear sympathetic to another (beyond the mere basis of putting classical $\mathsf{ZFC}$ into question), e.g., I seem to understand that Vladimir Voevodsky was leaning towards both constructivism and ultrafinitism. Hermann Weyl may also be a name to mention here (concerning predicativism and at least one of the other two).

  • On the other hand, extensions of the constructive system $\mathsf{CZF}$ by various “large cardinal” axioms acquire, if I understand correctly, much less consistency strength then when formulated over $\mathsf{ZF}$ (see, e.g., Rathjen, Griffor & Palmgren, “Inaccessibility in constructive set theory and type theory”), which suggests that constructivism, even if it does not completely conflict with infinities, seems to “temperate” them somewhat. It is at least certainly relevant to note that $\mathsf{CZF}$ has (IIUC) the same consistency strength as $\mathsf{KP}$: see this other question on the matter.

So, question: is there some explainable relationship between constructivism, finitism and predicativism?

A related question (which maybe deserves a separate post as it is less about philosophy and more about actual mathematics — please advise), which would tend to suggest a negative answer to the above, is whether there are any fully constructive systems with the same consistency strength as $\mathsf{ZFC}$ or whether there is some explainable objection to finding such a system.

$\endgroup$
6
  • 2
    $\begingroup$ Kripke and Platek developed their theory not as an alternative foundation motivated by some supposed deficiency in ZF, but as a tool for proving theorems in higher recursion theory. See Kripke's abstracts. $\endgroup$ Commented Jan 17, 2023 at 11:48
  • $\begingroup$ There is a set theory called IZF, “intuitionist ZF” which is constructive in using intuitionist logic and is equiconsistent with ZFC. See my answer to a similar question here. $\endgroup$
    – user44143
    Commented Jan 17, 2023 at 13:38
  • 2
    $\begingroup$ Since you explicitly say that your question is philosophical and not mathematical, I doubt that there's a more precise answer than what you've already outlined. I'll note, though, that one reason for these different "isms" is that their historical motivations are somewhat different. A major motivation for finitism was Hilbert's program (in this context, it's often associated with PRA rather than PA). A major motivation for predicativism is to find a foundation broad enough to encompass all of "working mathematics" while avoiding anything that might smell paradoxical. $\endgroup$ Commented Jan 17, 2023 at 14:50
  • 1
    $\begingroup$ (continued) Constructivism is motivated in large part by a distaste for pure existence proofs that give almost no information about the object in question. Since these motivating questions are all rather distinct from each other, one should not expect that the proposed answers will enjoy any simple relationship. $\endgroup$ Commented Jan 17, 2023 at 14:52
  • 1
    $\begingroup$ IZF has at least one good claim to constructivity, namely the numerical existence property: if IZF proves that some number satisfies $\phi(n)$, then there is some numeral $t$ for which IZF proves $\phi(t)$. This is theorem 9.3 in Beeson’s Foundations of Constructive Mathematics, whose next section suggests thinking of IZF as the classically intelligible fragment of the constructive theory of the hereditarily extensional sets. $\endgroup$
    – user44143
    Commented Jan 18, 2023 at 2:41

0

You must log in to answer this question.