Post History
#3: Post edited
- What makes the most sense to do somewhat depends on the context of this expression.
- What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ *isn't* a function of $\mathbf s$ but merely a total (multi-valued) relation on $\mathbf s$. Thus the Right solution is to address this head-on. You could do this by having $\mathbf e$ be a set-valued function or by having something like an $\mathsf{axis\_of}$ relation. Specifically, $$\mathbf e(\mathbf s) = \begin{cases}\mathbf \{\mathbf s / \lVert\mathbf s\rVert\}, & \lVert\mathbf s\rVert \neq 0 \\ \mathcal S^2, & \lVert\mathbf s\rVert = 0\end{cases}$$ or $$\mathsf{axis\_of}(\mathbf e, \mathbf s) \iff (\lVert\mathbf s\rVert = 0 \land e \in \mathcal S^2) \lor (\lVert\mathbf s\rVert \neq 0 \land e = \mathbf s / \lVert\mathbf s\rVert)$$ The latter formula could be simplified in various ways, e.g. $$\mathbf e \in \mathcal S^2 \land (\lVert\mathbf s\rVert \neq 0 \implies \mathbf e = \mathbf s/\lVert\mathbf s\rVert)$$ Incidentally, the definition of $\mathsf{axis\\_of}$ is a direct answer to your title question.
- Now I will talk about various less Right options. Why do this? First, it is perfectly valid and quite doable to do things the way I described above. But it will also feel weird and often be clumsy^[Things like Eugenio Moggi's monadic metalanguage would help partially recover some ergonomics for the set-valued function case.]. And all this for one particular edge case. Essentially, the (non-functional) relational nature of $\mathbf e$ pollutes everything it touches.
One only slightly less Right approach is to make an arbitrary choice. Unlike the situation with division of numbers (where we have a non-functional relation as well but in that case a partial, single-valued one), you have options. One way of doing this is to only partially axiomatize/specify the $\mathbf e$ function. This is easy enough to do informally, but I'll also explain how it would be done formally. Essenitally, you add $\mathbf e$ as a new function symbol^[If you're familiar with the notion or as an introduction to the notion, $\mathbf e$ is essentially a Skolem function for the formula $\forall\mathbf s\in\mathcal E.\exists \mathbf e.\mathsf{axis\_of}(\mathbf e, \mathbf s)$.] and add axioms $\forall\mathbf s \in \mathcal E.\mathbf e(\mathbf s) \in \mathcal S^2$ and $\forall\mathbf s \in \mathcal E.\lVert\mathbf s Verteq 0 \implies \mathbf e(\mathbf s) = \mathbf s / \lVert\mathbf s Vert$ where $\mathcal E$ will be the set of exponential coordinates^[Which is to say, add the axiom $\forall \mathbf s \in \mathcal E.\mathsf{axis\_of}(\mathbf e(\mathbf s), \mathbf s)$.]. The value of $\mathbf e(\mathbf 0)$ is not (logically) decidable from these axioms but it is a particular but unknown value constrained to lie in $\mathcal S^2$. That is, $\mathbf e(\mathbf 0) = \mathbf e(\mathbf 0)$ is true^[The relational equivalent of this would be $\mathsf{axis\_of}(\mathbf e, \mathbf s) \land \mathsf{axis\_of}(\mathbf e', \mathbf s) \implies \mathbf e = \mathbf e'$ which is false and the whole reason we're in this situation.]. Note how $1/0 = 1/0$ is ***not*** true. This seeming equation between expressions is actually shorthand for a predicate unrelated to equality. Of course, you could just specify the value, say $(1, 0, 0)$ (making clear that this choice is arbitrary). The only real downside to this is that it is technically possible to write theorems that depend on this choice.- Finally, you can do what is done for division of numbers: implicitly add constraints to restrict the relation to the domain on which it is single-valued and thus a function. That said, the situation isn't nearly as bad as for division. Per the previous paragraph, as long as $\mathbf e(\mathbf 0)$ is treated as having a consistent if unknown value — which is the natural thing to do — there won't be any problems.
- What makes the most sense to do somewhat depends on the context of this expression.
- What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ *isn't* a function of $\mathbf s$ but merely a total (multi-valued) relation on $\mathbf s$. Thus the Right solution is to address this head-on. You could do this by having $\mathbf e$ be a set-valued function or by having something like an $\mathsf{axis\_of}$ relation. Specifically, $$\mathbf e(\mathbf s) = \begin{cases}\mathbf \{\mathbf s / \lVert\mathbf s\rVert\}, & \lVert\mathbf s\rVert \neq 0 \\ \mathcal S^2, & \lVert\mathbf s\rVert = 0\end{cases}$$ or $$\mathsf{axis\_of}(\mathbf e, \mathbf s) \iff (\lVert\mathbf s\rVert = 0 \land e \in \mathcal S^2) \lor (\lVert\mathbf s\rVert \neq 0 \land e = \mathbf s / \lVert\mathbf s\rVert)$$ The latter formula could be simplified in various ways, e.g. $$\mathbf e \in \mathcal S^2 \land (\lVert\mathbf s\rVert \neq 0 \implies \mathbf e = \mathbf s/\lVert\mathbf s\rVert)$$ Incidentally, the definition of $\mathsf{axis\\_of}$ is a direct answer to your title question.
- Now I will talk about various less Right options. Why do this? First, it is perfectly valid and quite doable to do things the way I described above. But it will also feel weird and often be clumsy^[Things like Eugenio Moggi's monadic metalanguage would help partially recover some ergonomics for the set-valued function case.]. And all this for one particular edge case. Essentially, the (non-functional) relational nature of $\mathbf e$ pollutes everything it touches.
- One only slightly less Right approach is to make an arbitrary choice. Unlike the situation with division of numbers (where we have a non-functional relation as well but in that case a partial, single-valued one), you have options. One way of doing this is to only partially axiomatize/specify the $\mathbf e$ function. This is easy enough to do informally, but I'll also explain how it would be done formally. Essentially, you add $\mathbf e$ as a new function symbol^[If you're familiar with the notion or as an introduction to the notion, $\mathbf e$ is essentially a Skolem function for the formula $\forall\mathbf s\in\mathcal E.\exists \mathbf e.\mathsf{axis\_of}(\mathbf e, \mathbf s)$.] and add axioms $\forall\mathbf s \in \mathcal E.\mathbf e(\mathbf s) \in \mathcal S^2$ and $\forall\mathbf s \in \mathcal E.\lVert\mathbf s Vert
- eq 0 \implies \mathbf e(\mathbf s) = \mathbf s / \lVert\mathbf s Vert$ where $\mathcal E$ will be the set of exponential coordinates^[Which is to say, add the axiom $\forall \mathbf s \in \mathcal E.\mathsf{axis\_of}(\mathbf e(\mathbf s), \mathbf s)$.]. The value of $\mathbf e(\mathbf 0)$ is not (logically) decidable from these axioms but it is a particular but unknown value constrained to lie in $\mathcal S^2$. That is, $\mathbf e(\mathbf 0) = \mathbf e(\mathbf 0)$ is true^[The relational equivalent of this would be $\mathsf{axis\_of}(\mathbf e, \mathbf s) \land \mathsf{axis\_of}(\mathbf e', \mathbf s) \implies \mathbf e = \mathbf e'$ which is false and the whole reason we're in this situation.]. Note how $1/0 = 1/0$ is ***not*** true. This seeming equation between expressions is actually shorthand for a predicate unrelated to equality. Of course, you could just specify the value, say $(1, 0, 0)$ (making clear that this choice is arbitrary). The only real downside to this is that it is technically possible to write theorems that depend on this choice.
- Finally, you can do what is done for division of numbers: implicitly add constraints to restrict the relation to the domain on which it is single-valued and thus a function. That said, the situation isn't nearly as bad as for division. Per the previous paragraph, as long as $\mathbf e(\mathbf 0)$ is treated as having a consistent if unknown value — which is the natural thing to do — there won't be any problems.
#2: Post edited
- What makes the most sense to do somewhat depends on the context of this expression.
- What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ *isn't* a function of $\mathbf s$ but merely a total (multi-valued) relation on $\mathbf s$. Thus the Right solution is to address this head-on. You could do this by having $\mathbf e$ be a set-valued function or by having something like an $\mathsf{axis\_of}$ relation. Specifically, $$\mathbf e(\mathbf s) = \begin{cases}\mathbf \{\mathbf s / \lVert\mathbf s\rVert\}, & \lVert\mathbf s\rVert \neq 0 \\ \mathcal S^2, & \lVert\mathbf s\rVert = 0\end{cases}$$ or $$\mathsf{axis\_of}(\mathbf e, \mathbf s) \iff (\lVert\mathbf s\rVert = 0 \land e \in \mathcal S^2) \lor (\lVert\mathbf s\rVert \neq 0 \land e = \mathbf s / \lVert\mathbf s\rVert)$$ The latter formula could be simplified in various ways, e.g. $$\mathbf e \in \mathcal S^2 \land (\lVert\mathbf s\rVert \neq 0 \implies \mathbf e = \mathbf s/\lVert\mathbf s\rVert)$$ Incidentally, the definition of $\mathsf{axis\\_of}$ is a direct answer to your title question.
- Now I will talk about various less Right options. Why do this? First, it is perfectly valid and quite doable to do things the way I described above. But it will also feel weird and often be clumsy^[Things like Eugenio Moggi's monadic metalanguage would help partially recover some ergonomics for the set-valued function case.]. And all this for one particular edge case. Essentially, the (non-functional) relational nature of $\mathbf e$ pollutes everything it touches.
One only slightly less Right approach is to make an arbitrary choice. Unlike the situation with division of numbers (where we have a non-functional relation as well but in that case a partial, single-valued one), you have options. One way of doing this is to only partially axiomatize/specify the $\mathbf e$ function. This is easy enough to do informally, but I'll also explain how it would be done formally. Essenitally, you add $\mathbf e$ as a new function symbol and add axioms $\forall\mathbf s \in \mathcal E.\mathbf e(\mathbf s) \in \mathcal S^2$ and $\forall\mathbf s \in \mathcal E.\lVert\mathbf s Verteq 0 \implies \mathbf e(\mathbf s) = \mathbf s / \lVert\mathbf s Vert$ where $\mathcal E$ will be the set of exponential coordinates^[Which is to say, add the axiom $\forall \mathbf s \in \mathcal E.\mathsf{axis\_of}(\mathbf e(\mathbf s), \mathbf s)$.]. The value of $\mathbf e(\mathbf 0)$ is not (logically) decidable from these axioms but it is a particular but unknown value constrained to lie in $\mathcal S^2$. That is, $\mathbf e(\mathbf 0) = \mathbf e(\mathbf 0)$ is true^[The relational equivalent of this would be $\mathsf{axis\_of}(\mathbf e, \mathbf s) \land \mathsf{axis\_of}(\mathbf e', \mathbf s) \implies \mathbf e = \mathbf e'$ which is false and the whole reason we're in this situation.]. Note how $1/0 = 1/0$ is ***not*** true. This seeming equation between expressions is actually shorthand for a predicate unrelated to equality. Of course, you could just specify the value, say $(1, 0, 0)$ (making clear that this choice is arbitrary). The only real downside to this is that it is technically possible to write theorems that depend on this choice.- Finally, you can do what is done for division of numbers: implicitly add constraints to restrict the relation to the domain on which it is single-valued and thus a function. That said, the situation isn't nearly as bad as for division. Per the previous paragraph, as long as $\mathbf e(\mathbf 0)$ is treated as having a consistent if unknown value — which is the natural thing to do — there won't be any problems.
- What makes the most sense to do somewhat depends on the context of this expression.
- What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ *isn't* a function of $\mathbf s$ but merely a total (multi-valued) relation on $\mathbf s$. Thus the Right solution is to address this head-on. You could do this by having $\mathbf e$ be a set-valued function or by having something like an $\mathsf{axis\_of}$ relation. Specifically, $$\mathbf e(\mathbf s) = \begin{cases}\mathbf \{\mathbf s / \lVert\mathbf s\rVert\}, & \lVert\mathbf s\rVert \neq 0 \\ \mathcal S^2, & \lVert\mathbf s\rVert = 0\end{cases}$$ or $$\mathsf{axis\_of}(\mathbf e, \mathbf s) \iff (\lVert\mathbf s\rVert = 0 \land e \in \mathcal S^2) \lor (\lVert\mathbf s\rVert \neq 0 \land e = \mathbf s / \lVert\mathbf s\rVert)$$ The latter formula could be simplified in various ways, e.g. $$\mathbf e \in \mathcal S^2 \land (\lVert\mathbf s\rVert \neq 0 \implies \mathbf e = \mathbf s/\lVert\mathbf s\rVert)$$ Incidentally, the definition of $\mathsf{axis\\_of}$ is a direct answer to your title question.
- Now I will talk about various less Right options. Why do this? First, it is perfectly valid and quite doable to do things the way I described above. But it will also feel weird and often be clumsy^[Things like Eugenio Moggi's monadic metalanguage would help partially recover some ergonomics for the set-valued function case.]. And all this for one particular edge case. Essentially, the (non-functional) relational nature of $\mathbf e$ pollutes everything it touches.
- One only slightly less Right approach is to make an arbitrary choice. Unlike the situation with division of numbers (where we have a non-functional relation as well but in that case a partial, single-valued one), you have options. One way of doing this is to only partially axiomatize/specify the $\mathbf e$ function. This is easy enough to do informally, but I'll also explain how it would be done formally. Essenitally, you add $\mathbf e$ as a new function symbol^[If you're familiar with the notion or as an introduction to the notion, $\mathbf e$ is essentially a Skolem function for the formula $\forall\mathbf s\in\mathcal E.\exists \mathbf e.\mathsf{axis\_of}(\mathbf e, \mathbf s)$.] and add axioms $\forall\mathbf s \in \mathcal E.\mathbf e(\mathbf s) \in \mathcal S^2$ and $\forall\mathbf s \in \mathcal E.\lVert\mathbf s Vert
- eq 0 \implies \mathbf e(\mathbf s) = \mathbf s / \lVert\mathbf s Vert$ where $\mathcal E$ will be the set of exponential coordinates^[Which is to say, add the axiom $\forall \mathbf s \in \mathcal E.\mathsf{axis\_of}(\mathbf e(\mathbf s), \mathbf s)$.]. The value of $\mathbf e(\mathbf 0)$ is not (logically) decidable from these axioms but it is a particular but unknown value constrained to lie in $\mathcal S^2$. That is, $\mathbf e(\mathbf 0) = \mathbf e(\mathbf 0)$ is true^[The relational equivalent of this would be $\mathsf{axis\_of}(\mathbf e, \mathbf s) \land \mathsf{axis\_of}(\mathbf e', \mathbf s) \implies \mathbf e = \mathbf e'$ which is false and the whole reason we're in this situation.]. Note how $1/0 = 1/0$ is ***not*** true. This seeming equation between expressions is actually shorthand for a predicate unrelated to equality. Of course, you could just specify the value, say $(1, 0, 0)$ (making clear that this choice is arbitrary). The only real downside to this is that it is technically possible to write theorems that depend on this choice.
- Finally, you can do what is done for division of numbers: implicitly add constraints to restrict the relation to the domain on which it is single-valued and thus a function. That said, the situation isn't nearly as bad as for division. Per the previous paragraph, as long as $\mathbf e(\mathbf 0)$ is treated as having a consistent if unknown value — which is the natural thing to do — there won't be any problems.
#1: Initial revision
What makes the most sense to do somewhat depends on the context of this expression. What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ *isn't* a function of $\mathbf s$ but merely a total (multi-valued) relation on $\mathbf s$. Thus the Right solution is to address this head-on. You could do this by having $\mathbf e$ be a set-valued function or by having something like an $\mathsf{axis\_of}$ relation. Specifically, $$\mathbf e(\mathbf s) = \begin{cases}\mathbf \{\mathbf s / \lVert\mathbf s\rVert\}, & \lVert\mathbf s\rVert \neq 0 \\ \mathcal S^2, & \lVert\mathbf s\rVert = 0\end{cases}$$ or $$\mathsf{axis\_of}(\mathbf e, \mathbf s) \iff (\lVert\mathbf s\rVert = 0 \land e \in \mathcal S^2) \lor (\lVert\mathbf s\rVert \neq 0 \land e = \mathbf s / \lVert\mathbf s\rVert)$$ The latter formula could be simplified in various ways, e.g. $$\mathbf e \in \mathcal S^2 \land (\lVert\mathbf s\rVert \neq 0 \implies \mathbf e = \mathbf s/\lVert\mathbf s\rVert)$$ Incidentally, the definition of $\mathsf{axis\\_of}$ is a direct answer to your title question. Now I will talk about various less Right options. Why do this? First, it is perfectly valid and quite doable to do things the way I described above. But it will also feel weird and often be clumsy^[Things like Eugenio Moggi's monadic metalanguage would help partially recover some ergonomics for the set-valued function case.]. And all this for one particular edge case. Essentially, the (non-functional) relational nature of $\mathbf e$ pollutes everything it touches. One only slightly less Right approach is to make an arbitrary choice. Unlike the situation with division of numbers (where we have a non-functional relation as well but in that case a partial, single-valued one), you have options. One way of doing this is to only partially axiomatize/specify the $\mathbf e$ function. This is easy enough to do informally, but I'll also explain how it would be done formally. Essenitally, you add $\mathbf e$ as a new function symbol and add axioms $\forall\mathbf s \in \mathcal E.\mathbf e(\mathbf s) \in \mathcal S^2$ and $\forall\mathbf s \in \mathcal E.\lVert\mathbf s\rVert \neq 0 \implies \mathbf e(\mathbf s) = \mathbf s / \lVert\mathbf s\rVert$ where $\mathcal E$ will be the set of exponential coordinates^[Which is to say, add the axiom $\forall \mathbf s \in \mathcal E.\mathsf{axis\_of}(\mathbf e(\mathbf s), \mathbf s)$.]. The value of $\mathbf e(\mathbf 0)$ is not (logically) decidable from these axioms but it is a particular but unknown value constrained to lie in $\mathcal S^2$. That is, $\mathbf e(\mathbf 0) = \mathbf e(\mathbf 0)$ is true^[The relational equivalent of this would be $\mathsf{axis\_of}(\mathbf e, \mathbf s) \land \mathsf{axis\_of}(\mathbf e', \mathbf s) \implies \mathbf e = \mathbf e'$ which is false and the whole reason we're in this situation.]. Note how $1/0 = 1/0$ is ***not*** true. This seeming equation between expressions is actually shorthand for a predicate unrelated to equality. Of course, you could just specify the value, say $(1, 0, 0)$ (making clear that this choice is arbitrary). The only real downside to this is that it is technically possible to write theorems that depend on this choice. Finally, you can do what is done for division of numbers: implicitly add constraints to restrict the relation to the domain on which it is single-valued and thus a function. That said, the situation isn't nearly as bad as for division. Per the previous paragraph, as long as $\mathbf e(\mathbf 0)$ is treated as having a consistent if unknown value — which is the natural thing to do — there won't be any problems.