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 you need to account for syntactically possible but theoretically impossible algebras for computation. In so doing I have gone further and repeatedly stated that because division by zero is not actually possible in fields, the author should not have tried to use such a rigorous system to justify the practical, syntactical requirements of a programming language. It doesn't make sense to try and refute mathematical theory as the preamble of a programming language manifesto.
> 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.
> 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.
[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.
>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).
Look at for example the set of real numbers. If you add the complex numbers to it, you can no longer speak of the real numbers. The real numbers form a subset of the complex numbers. The same thing happens if you add definitions to a field. You create something which has mayber has a field as a subset, but you can no longer speak of a field.
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]
Undefined is just undefined, no value, not a magic one, or just a random one, or one you prefer. Just void, the empty set.
To understand it, look for example at the graph of y = sqrt(x), where x and y are real numbers. You see no points at negative x. Its undefined in the domain x < 0. Yes you can say at x < 0, y = 3, that is now my definition sqrt(), but then you no longer have the sqrt function mathematicians talk about. The same thing applies to fields and 1/x.
>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]
Now you apply boolean logic to the result of calculations, numbers and non-numbers, not on statements. I can also ask what is 5 AND true? Is that true? The question doesn't make sense, so the answer is: depends on the programming language.
> Look at for example the set of real numbers. If you add the complex numbers to it, you can no longer speak of the real numbers.
What does this have to do with adding axioms? You don't get the complex numbers from the real numbers by adding axioms. For example, the following is provable for the reals, but not for complex numbers:
∀x,y . x < y ∨ x > y ∨ x = y
> You create something which has mayber has a field as a subset, but you can no longer speak of a field.
No. The class of all fields are all objects satisfying the field axioms. If you add axioms, you get get a subset of those fields. Each and every one of them is a field.
> Undefined is just undefined
I'm not looking for handwaving. Formal mathematics is math that can be done mechanically. Write down the axioms for undefined. Again -- I'm not saying it hasn't been done, but it's certainly not part of standard first-order logic, and it is unnecessary.
> To understand it, look for example at the graph
I understand what undefined means in informal mathematics. Try to see what it means in formal mathematics. But the important point is, try to understand why it is unnecessary in formal mathematics in most cases.
> Now you apply boolean logic to the result of calculations, numbers and non-numbers, not on statements.
No. You can write 1/x < 5 ∨ x > 20.
> The question doesn't make sense, so the answer is: depends on the programming language.
There is no such thing as "doesn't make sense" in formal math, even though there is such a thing in informal math. That's the whole point. Either the expression is ill-formed, i.e. not in the language or a "syntax error", or it must make some sense.
This is why it's useful and easy to say something is undefined in informal math, but not as useful and not as easy to do that in formal math.
>What does this have to do with adding axioms? You don't get the complex numbers from the real numbers by adding axioms. For example, the following is provable for the reals, but not for complex numbers:
> ∀x,y . x < y ∨ x > y ∨ x = y
Since R is a subset of C, you can write C as R with additional axioms. See for example:
>I'm not looking for handwaving. Formal mathematics is math that can be done mechanically. Write down the axioms for undefined. Again -- I'm not saying it hasn't been done, but it's certainly not part of standard first-order logic, and it is unnecessary.
You are trying to define the undefined in a formal system. Undefined is just the absence of a definition. Not 0, 3 , 2pi
> No. You can write 1/x < 5 ∨ x > 20.
Yes, those are valid mathematical statements. 5 ∨ TRUE, or undefined V TRUE, I doubt it.
> There is no such thing as "doesn't make sense" in formal math, even though there is such a thing in informal math. >That's the whole point. Either the expression is ill-formed, i.e. not in the language or a "syntax error", or it must make some sense.
Well in language, in which I am corresponding with you, there is such a thing as 'makes no sense'.
You are somehow trying to capture everything in your logical system only to try to prove that 1/0 = 0 is part of a field, which it isn't. I've made my point here, it was nice talking to you.
> Since R is a subset of C, you can write C as R with additional axioms.
That's not even remotely how it works. You may want to read up on logical theories and models[1].
> Well in language, in which I am corresponding with you, there is such a thing as 'makes no sense'.
Yes, and for the same reason we can have such a thing as "undefined" (that means more than merely 'not specified') in informal mathematics -- because both English and informal math are informal. But we are talking about formal languages[2], which do not have such a thing.
What exactly are you looking for me to say here?