Timeline for Predicative definition
Current License: CC BY-SA 2.5
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 23, 2019 at 12:18 | comment | added | Tommy R. Jensen | Let us continue this discussion in chat. | |
| Oct 23, 2019 at 11:46 | comment | added | Tommy R. Jensen | Behold my predicative definition of $\mathbb{N}$. Call a set $B$ in ZF "super-inductive" if $0\not\in B$ and $\{0\}\in B,$ and for every $x\in B$ also $x\cup \{x\}\in B.$ Let $A$ be the inductive set provided by AI. Then $B:=A\setminus \{0\}$ is super-inductive. Define $\mathbb{N}$ as the union of $\{0\}$ with the intersection set of all subsets of $B.$ | |
| Oct 22, 2019 at 23:04 | comment | added | Andreas Blass | (1) I don't think predicavists would consider "we may not be aware of" the impredicativity of a definition sufficient to make it predicative. They'd require definitions to quantify only over totalities known to not contain the entity being defined. (2) Once we've defined what a group is, we can perfectly well define, in the context of any group, "the identity element is the unique element x that satisfied xx=x." | |
| Oct 22, 2019 at 22:24 | comment | added | Tommy R. Jensen | (2) But we cannot state an axiom "x is an identity if xx=x" because it only captures the notion of a projection, which is not what we mean. And if we say "x is an identity if xx=x and for all y, if yy=y, then y=x", then this is also impredicative, because x is one of the possible values for y. | |
| Oct 22, 2019 at 22:23 | comment | added | Tommy R. Jensen | (1) This is true. But at the point in time at which we formulate the axioms, we may not be aware of the theorem that $\mathbb{N}$ is also among the sets being intersected. After all, the theorem is proved from the axioms, and this is one of them. In which case the statement that the definition is impredicative is itself what? Impredicative? | |
| Oct 22, 2019 at 14:03 | comment | added | Andreas Blass | @TommyR.Jensen (1) For any inductive set $A$, we have that $\mathbb N$ is an inductive subset of $A$, so it's one of the sets being intersected in the definition of $\mathbb N$. (2) In operator algebras, $xx=x$ characterizes projections, but in groups it characterizes the identity (just multiply both sides of $xx=x$ by $x^{-1}$). | |
| Oct 22, 2019 at 13:12 | comment | added | Tommy R. Jensen | quite, thanks! I still have to wrap my head around how it is that the intersection of the elements of the powerset of $A$ is not a predicative thing. After all, it might turn out to be different from all those subsets. That the intersection is itself inductive must be proven afterwards. By the way, the condition $xx=x$ in a group of linear maps seems to characterize a projection, not just the identity. | |
| Oct 22, 2019 at 12:09 | comment | added | Andreas Blass | @TommyR.Jensen In ZF, the axiom of infinity says there is an inductive set. Then one defines $\mathbb N$ as the intersection of all inductive subsets of an inductive set $A$, after proving that the resulting $\mathbb N$ is independent of the choice of $A$. | |
| Oct 22, 2019 at 11:26 | comment | added | Tommy R. Jensen | I would think that definition of $\mathbb{N}$ is not usual in set-theories like ZF, since it seems to assume a set of all inductive sets, to allow defining their intersection. It sounds similarly bad as the "set of all sets". | |
| Oct 21, 2019 at 3:13 | comment | added | Andreas Blass | @TommyR.Jensen The identity element of a group admits an alternative definition, as the only element satisfying xx=x, so one can avoid impredicativity there. As for induction, I don't claim to understand Nelson's work, but he might have been referring to the usual set-theoretic definition of $\mathbb N$ as the intersection of all sets that contain $0$ and are closed under successor. That definition, which implies the induction principle, is impredicative because $\mathbb N$ itself is a set that contains $0$ and is closed under successor. | |
| Oct 20, 2019 at 22:41 | comment | added | Tommy R. Jensen | Another instance that I wonder about is when Nelson in his 1986 pamphlet "predicative Arithmetic" states that "the principle of induction" is impredicative. How can induction fall into the scope of having an impredicative definition, given that "induction" is not a mathematical object? | |
| Oct 20, 2019 at 22:33 | comment | added | Tommy R. Jensen | The supremum and Russell's paradox seem classical examples. I wonder about the definition of the identity element in GroupTheory. It is an element e for which ex = xe = x for all x. Since in this definition there is a quantification over all elements x, including e itself, is it not also an example of an impredicative definition? In which case, is there some reason why this example would be less important, or at least less referred to, than the others? | |
| Sep 17, 2012 at 23:13 | vote | accept | CommunityBot | ||
| Sep 17, 2012 at 23:13 | vote | accept | CommunityBot | ||
| Sep 17, 2012 at 23:13 | |||||
| Aug 28, 2010 at 19:56 | vote | accept | CommunityBot | ||
| Aug 28, 2010 at 19:57 | |||||
| Aug 28, 2010 at 15:56 | history | answered | Andreas Blass | CC BY-SA 2.5 |