So we can express concepts like “What is not known to be X is assumed to not be X” (where X could be “true” or “false” in the simplest example) in logical notation. Is this just an obsessive quest for conciseness, or is there some function for equations of this sort? It seems to me that one of the major reasons to re-encode something written in plain language as an equation is to remove dependence on a specific (human) language. But that can’t be possible here, you’re always tied to some language to provide the parameters for these logical equivalences. Still, this seems to have applications in encoding laws in computer-readable format (see https://arxiv.org/abs/2103.03198 ).