Timeline for Formalizations of the idea that something is a function of something else?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 10, 2018 at 17:09 | comment | added | Michael Bächtold | Interesting. I'll need to think about that. A first spontaneous question: wouldn't every new variable introduced after $x$ then automatically be a function of $x$? Or how could you introduce a variable $z$ after $x$, and assume that it is not a function of $x$? | |
| Aug 10, 2018 at 17:01 | comment | added | Tim Campion | "Assume that $y$ is a function of $x$" is actually a simpler statement, because $y$ is not already floating around somewhere before you stipulate this -- rather, $y$ is introduced as something that depends only on $x$. It would be formalized as follows. Assume we have a context $\Gamma$, and $\Gamma \vdash X$. Then "Assume that $y$ is a function of $x$ (relative to $\Gamma$)" means that $\Gamma, x:X \vdash Y$ and you're expanding the context to $\Gamma, x:X,y:Y$. In that sense, it's a completely ordinary statement. | |
| Aug 10, 2018 at 8:04 | comment | added | Michael Bächtold | "...which seems like overkill" ... maybe. When I teach, I would like to say: "assume that y is a function of x". Wouldn't this then be a statement at the meta-meta level? | |
| Aug 10, 2018 at 7:43 | comment | added | Michael Bächtold | Thanks. Could you explain why you say that the usual definition of "function" in set theory is external? (Do you mean the definition of a map, i.e. a subset of the cartesian product $A\times B$, or the meta-definition of "function of" I gave in my question?). | |
| Aug 9, 2018 at 22:45 | history | answered | Tim Campion | CC BY-SA 4.0 |