Timeline for Subset Collection axiom
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 11, 2021 at 0:44 | history | edited | LSpice | CC BY-SA 4.0 |
Name of reference
|
| Oct 10, 2021 at 23:58 | vote | accept | ToucanIan | ||
| Oct 10, 2021 at 19:37 | answer | added | aws | timeline score: 3 | |
| Oct 9, 2021 at 9:08 | history | edited | YCor | CC BY-SA 4.0 |
removed capitals from title
|
| Oct 9, 2021 at 7:57 | comment | added | Hanul Jeon | It justifies the existence of function sets, which is usually proven under the axiom of power set. Unfortunately, I do not know any other use of this axiom except for the justification for the existence of Dedekind reals. I believe (and Aczel intended) the type-theoretic interpretation fortifies constructive (and predicative) manner of $\mathsf{CZF}$. | |
| Oct 9, 2021 at 5:59 | comment | added | ToucanIan | @HanulJeon So what does this axiom do for a constructive mathematician? How does this in anyway replace the power set axiom? | |
| Oct 9, 2021 at 5:37 | comment | added | Hanul Jeon | If I understand your question correctly (that is, a way to extract information about $c$ from $a$, $b$, and the multivalued function), the answer would be: extracting information is seemingly unlikely. | |
| Oct 9, 2021 at 3:43 | comment | added | ToucanIan | I will check out this type theoretic interpretation. | |
| Oct 9, 2021 at 3:43 | comment | added | ToucanIan | @HanulJeon how does one get any information about subsets out of this notion of multivalued functions? | |
| Oct 9, 2021 at 3:09 | comment | added | Hanul Jeon | You may convince yourself by examining how to interpret Subset Collection under Aczel's type-theoretic interpretation of $\mathsf{CZF}$ (and, in fact, it is the focal motivation for Constructive ZF.) | |
| Oct 9, 2021 at 3:05 | comment | added | Hanul Jeon | Then we may state Subset Collection as follows: for a given definable collection of multi-valued functions $\{R_u: a\rightrightarrows b\}$ parametrized by $u\in V$, we can find a set $c$ such that $c$ contains every "image" of $a$ under $R_u$. Honestly, however, neither Subset Collection nor Fullness is handy for me. | |
| Oct 9, 2021 at 3:02 | comment | added | Hanul Jeon | One way to put syntactic sugar to Subset Collection is to use the notion of multi-valued function (a relation $R\subseteq A\times B$ for classes $A$ and $B$ is a multi-valued function from $A$ to $B$ means for each $a\in A$ there is (not necessarily unique) $b\in B$ such that $(a,b)\in R$.) I prefer to denote it as $R:A\rightrightarrows B$. | |
| Oct 9, 2021 at 2:33 | history | asked | ToucanIan | CC BY-SA 4.0 |