Timeline for What is the relationship (if any) between constructivism, finitism and predicativism?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 24 at 9:40 | comment | added | user21820 | I think it's impossible to reach ZFC strength by any means that can be considered predicative. At the best, ZFC with only bounded Specification and Replacement. The reason is that Replacement makes absolutely no sense unless you already believe in something as strong as ZFC. | |
| Jan 18, 2023 at 2:41 | comment | added | user44143 | 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. | |
| Jan 17, 2023 at 19:11 | history | became hot network question | |||
| Jan 17, 2023 at 14:52 | comment | added | Timothy Chow | (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. | |
| Jan 17, 2023 at 14:50 | comment | added | Timothy Chow | 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. | |
| Jan 17, 2023 at 13:38 | comment | added | user44143 | 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. | |
| Jan 17, 2023 at 11:48 | comment | added | Robert Furber | 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. | |
| Jan 17, 2023 at 11:07 | history | asked | Gro-Tsen | CC BY-SA 4.0 |