5 ms·

I don't know what to tell you. You're continuing to argue but you seem to not be following my point. I've already long since told you we're in agreement that yo

• pron 8y ago
  > What exactly are you looking for me to say here? Very simple. Here is a theory of a field in FOL: ∀ x . x + 0 = x ∀ x . ∃ -x . x + (-x) = 0 ∀ x, y . x + y = y + x ∀ x, y, z . (x + y) + z = x + (y + z) ∀ x, y . x – y = x + (-y) ∀ x . 1x = x ∀ x . x ≠ 0 ⇒ ∃ x⁻¹ . xx⁻¹ = 1 ∀ x, y . xy = yx ∀ x, y, z . (xy)z = x(yz) ∀ x, y . y ≠ 0 ⇒ x/y = xy⁻¹ ∀ x, y, z . x(y + z) = xy + xz Do you claim that this formalization is unacceptable (i.e. it does not precisely and fully define what a field is)? If so, why? If not, can you write a single theorem in this theory that would be falsified if I added the axiom, ∀ x . x/0 = 0 ? If your answer to both questions is no, then your only point may be that the extended definition of the symbol / does not deserve the name "division" because it does not conform to our intuitive, informal notion. That's fine but is a long way from claiming that there is no acceptable formalization of fields or that division by zero introduces a mathematical contradiction or breaks equational laws. Note that you cannot say that the original theory defines a field while the extended one doesn't, because the latter's models are a subset of the former's. This then leaves open the matter of whether such a philosophical, aesthetic consideration trumps pragmatic ones or vice-versa, to which I don't think anyone has a universal answer, and it is not the issue, anyway.
  • blablablerg 8y ago
    In the definition of a field ∀ x . x/0 = undefined, not 0 or any other value you might prefer. A field is exactly defined by the field axioms: adding or removing any other axiom makes it no longer a field.
    • pron 8y ago
      > A field is exactly defined by the field axioms: adding or removing any other axiom makes it no longer a field. This is clearly not true. Adding axioms (as long as they don't introduce consistency) can only reduce the set of models. Anything that satisfies the larger theory also satisfies the smaller theory. This is exactly why a group is a monoid is a semigroup. This is why fields are rings. In fact, this is why the rationals or the reals are fields: they satisfy the field axioms, and more (for example, they are ordered). > In the definition of a field ∀ x . x/0 = undefined, not 0 or any other value you might prefer. What is "undefined"? First let's look at the logic itself: What is true ∨ undefined ? What is true ∧ undefined? Now at the theory: What is undefined + x ? What is 0 * undefined ? What is 0 = undefined ? etc.[0] While it is possible to formally define this magic non-value (sometimes written as ⊥ in the logics that contain it) as is done in some programming languages (and it has been done), this would entail adding quite a few more axioms to FOL and to the theory of fields. When people say FOL, they mean a particular language[1], one that is considered by mathematicians to be sufficient to formalize all of mathematics and has very particular syntax and semantics. FOL + undefined is a very different language, which much more complicated semantics. If you think that when people refer to FOL they refer to FOL + undefined, I challenge you to find any mention of it in descriptions of standard FOL. Similarly, if you think that by common theories, say fields or sets, people really mean field + undefined or ZFC + undefined (what is {undefined}? What is undefined ∈ {undefined}? etc.), I challenge you to find any mention of the complex axioms required in treatments of these common theories. But it's not just a matter of convention. The reason you won't find it in the standard logics/theories is that it's completely unnecessary. If you work it out, you'll find that the theory of fields I provided and the more complicated one involving undefined that you suggest is the common formalization are the very same theory, in the sense that they yield exactly the same theorems, except for those specifically involving undefined (i.e., your theory has more theorems than mine). You'll find that you cannot find a "bad" theorem that you can prove with the simple theory but cannot with the one involving undefined, and therefore it is unhelpful except for the purpose of satisfying a certain desire for intuition that requires significantly complicating the formal system.[2] There's a paper by Sol Feferman[3] reviewing formal systems with explicit handling of "undefined." AFAIK, they are rarely if ever used. Such semantics are certainly not part of the trusty-old FOL, considered the default language of formal mathematics. [0]: BTW, if you think that the meaning of every expression involving undefined is undefined, then you'll see that this doesn't work. For example, you have: x=0 ⇒ x(1/x)=1. This is a valid formula, and so it's true even when x=0, but then you have undefined on the right-hand side, so you want at least false ⇒ undefined to be equal to true. But A ⇒ B = ¬A ∨ B, which means you want at least true ∨ undefined = true. Similarly, you'll want at least 0 = undefined to be false etc. [1]: https://en.wikipedia.org/wiki/First-order_logic https://en.wikipedia.org/wiki/First-order_logic [2]: E.g., while in your theory you will be able to prove the rather useless theorem 1/0 ≠ 0, in my theory you will not be able to prove 1/0 = x for any x, so it really poses no issue. [3]: https://math.stanford.edu/~feferman/papers/definedness.pdf https://math.stanford.edu/~feferman/papers/definedness.pdf