Communities

Writing
Writing
Codidact Meta
Codidact Meta
The Great Outdoors
The Great Outdoors
Photography & Video
Photography & Video
Scientific Speculation
Scientific Speculation
Cooking
Cooking
Electrical Engineering
Electrical Engineering
Judaism
Judaism
Languages & Linguistics
Languages & Linguistics
Software Development
Software Development
Mathematics
Mathematics
Christianity
Christianity
Code Golf
Code Golf
Music
Music
Physics
Physics
Linux Systems
Linux Systems
Power Users
Power Users
Tabletop RPGs
Tabletop RPGs
Community Proposals
Community Proposals
tag:snake search within a tag
answers:0 unanswered questions
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
votes:4 posts with 4+ votes
created:<1w created < 1 week ago
post_type:xxxx type of post
Search help
Notifications
Mark all as read See all your notifications »

Review Suggested Edit

You can't approve or reject suggested edits because you haven't yet earned the Edit Posts ability.

Approved.
This suggested edit was approved and applied to the post over 1 year ago by Peter Taylor‭.

4 / 255
  • 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 &mdash; which is the natural thing to do &mdash; 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 &mdash; which is the natural thing to do &mdash; there won't be any problems.

Suggested over 1 year ago by trichoplax‭