Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 10 of 10
To anybody who can think constructively (Mike at least):
Given a real number a, and let X be the Kuratowski-finite set {y,z} such that y=z iff a≠0 (in the strong sense of apartness). Consider the ring of polynomials with real coefficients and variables from the set X. Are the polynomials ay and az equal?
(The polynomial functions from ℝX to ℝ defined by them are certainly equal, but I’m asking about polynomials as formal expressions. For example, the polynomials x and x2 are not equal, even in the ring of one-variable polynomials with coefficients from 𝔽2.)
I must be missing something; why are the polynomial functions they define equal?
I believe the following argument shows that the polynomial functions are equal:
Let φ∈ℝX, we want to show aφ(y)=aφ(z). For any n≥1, we have a≠0 or |a|≤1n. In both cases the inequality |aφ(y)−aφ(z)|≤1n⋅|φ(y)−φ(z)| follows. As |φ(y)−φ(z)| is fixed, this shows that indeed |aφ(y)−aφ(z)|=0.
I don’t have an answer to the original question.
Nice argument! I’m afraid I don’t have an answer to the original question either, though. I don’t see any reason why they should be equal, but I don’t immediately see how to build a counterexample either.
I shouldn't be distracting myself with this, but what does "=" mean, here? Or is that part of the question, too?
Well, the real numbers are a set, as are Toby’s set X and the polynomial ring, so = means equality in those sets. Are you asking about how those sets are defined? The set X, for instance, is defined as the quotient of the two-element set {y,z} by the equivalence relation which sets y∼z iff a≠0 (and of course y∼y and z∼z unconditionally).
JC is right to ask; the question is what equality in ℝ[X] should be. Of course, ℝ[X] is the free commutative ℝ-algebra on the set X, but what’s an ℝ-algebra? If this is simply a set equipped with some operations and commutative diagrams (including one unary scalar multiplication operation for each real number), then ay=az in ℝ[X] iff a=0 or a≠0 (so if ay=az for every a, then the lesser limited principle of omniscience holds). However, if an ℝ-algebra is equipped with a tight apartness that all operations respect and a binary scalar multiplication operation ℝ×B→B that also respects it and the usual apartness on ℝ (in the sense of being strongly extensional), then ay=az necessarily. So that answers my question, I guess.
Hmm, I was about to say that I thought Ingo’s argument would work for polynomials too. Namely, define the norm of a polynomial to be the supremum of the absolute values of its coefficients. Then since either |a|<1n or a≠0, in both cases ‖ay−az‖<2n, and this holds for all n, so ‖ay−az‖=0 and thus ay=az. What definition of ℝ[X] is that using?
How do you know that this supremum exists? (It always exists as a lower real number, but the comparison law is invalid for those, so we must prove that the supremum is located.) In particular, the norm of ay−az is 0 if y=z, but this norm is a if y≠z.
With the second definition of ℝ[X] (with apartness), I we can prove that ay−az must have a located norm (although we can’t prove this for an arbitrary polynomial in ℝ[X]), so the argument will still go through; but not with the first definition.
Ah, right. (You can probably tell that I don’t work with constructive real numbers much.)
1 to 10 of 10