Return to Question

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)

The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when $x^2$ is restricted on the domain and codomain to $[0, \infty)$.

In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.

In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.

The exponential function is defined by a particular Taylor series, and the logarithm function could be defined by an analytic continuation of a particular Taylor series. Thus, one could try to define the square root as the function $$e^{\frac{1}{2} \ln(x)}$$ However, because $\ln(x)$ is undefined at $x = 0$, that function is only defined on the open interval $(0, \infty)$. Similarly to the previous attempt, in classical mathematics, one could use excluded middle to extend the function to $[0, \infty)$, but that isn't possible in constructive mathematics.

Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?

This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields. If the latter is the case, then one might have to equip Cauchy complete Archimedean ordered fields with the additional structure of a principal square root function in order to do constructive Euclidean geometry.

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)

The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when $x^2$ is restricted on the domain and codomain to $[0, \infty)$.

In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.

In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. (In constructive mathematics, the inverse function theorem still holds for $x^2$ because $x^2$ is uniformly differentiable on every closed subinterval of $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.

The exponential function is defined by a particular Taylor series, and the logarithm function could be defined by an analytic continuation of a particular Taylor series. Thus, one could try to define the square root as the function $$e^{\frac{1}{2} \ln(x)}$$ However, because $\ln(x)$ is undefined at $x = 0$, that function is only defined on the open interval $(0, \infty)$. Similarly to the previous attempt, in classical mathematics, one could use excluded middle to extend the function to $[0, \infty)$, but that isn't possible in constructive mathematics.

Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?

This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields. If the latter is the case, then one might have to equip Cauchy complete Archimedean ordered fields with the additional structure of a principal square root function in order to do constructive Euclidean geometry.

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)

The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when restricted on the domain and codomain to $[0, \infty)$.

In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.

In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.

Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?

This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields. If the latter is the case, then one might have to equip Cauchy complete Archimedean ordered fields with the additional structure of a principal square root function in order to do constructive Euclidean geometry.

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)

The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when $x^2$ is restricted on the domain and codomain to $[0, \infty)$.

In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.

In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.

The exponential function is defined by a particular Taylor series, and the logarithm function could be defined by an analytic continuation of a particular Taylor series. Thus, one could try to define the square root as the function $$e^{\frac{1}{2} \ln(x)}$$ However, because $\ln(x)$ is undefined at $x = 0$, that function is only defined on the open interval $(0, \infty)$. Similarly to the previous attempt, in classical mathematics, one could use excluded middle to extend the function to $[0, \infty)$, but that isn't possible in constructive mathematics.

Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?

This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields. If the latter is the case, then one might have to equip Cauchy complete Archimedean ordered fields with the additional structure of a principal square root function in order to do constructive Euclidean geometry.

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)

The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when restricted on the domain and codomain to $[0, \infty)$.

In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.

In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.

Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?

This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields.

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple Cauchy complete Archimedean ordered fields, which are not provable to be equivalent to each other: one cannot in general prove that the Dedekind real numbers embeds into the initial Cauchy complete Archimedean ordered field. (By Cauchy complete we mean complete by Cauchy sequences, not Cauchy nets.)

The principal square root function is a function defined on the non-negative elements $[0, \infty)$ of a Cauchy complete Archimedean ordered field $\mathbb{R}$ such that it is a two-sided inverse of the square function $x^2$ when restricted on the domain and codomain to $[0, \infty)$.

In classical mathematics, one could prove that the principal square root function exists by proving the fundamental theorem of algebra for any Cauchy complete Archimedean ordered field. However, in constructive mathematics, the fundamental theorem of algebra cannot in general be proven for Cauchy complete Archimedean ordered fields.

In classical mathematics, there is an alternative to proving that the principal square root function exists: by first proving that zero has a square root, and that there exists a two-sided inverse function of $x^2$ on the positive elements $(0, \infty)$ of $\mathbb{R}$. The square root of zero is zero in any integral domain, and because in any Cauchy complete Archimedean ordered field the square function $x^2$ is continuously differentiable on the open interval $(0, \infty)$ and its derivative $2x$ is always positive on the open interval $(0, \infty)$, by the inverse function theorem, there exists a two-sided inverse defined on $(0, \infty)$. Then we use excluded middle to show that if the principal square root function is defined at $0$ and defined on the domain $(0, \infty)$, then it is defined on $[0, \infty)$. However, in constructive mathematics, by definition there is no excluded middle, so we cannot prove the last step.

Is there a way of proving that the principal square root function on the non-negative elements of a Cauchy complete Archimedean ordered field actually exists? I might be missing something very obvious. Or is it not provable in constructive mathematics that such a function exists in all Cauchy complete Archimedean ordered fields?

This is fairly important because it is one of the functions used in defining the Euclidean metric in finite-dimensional vector spaces over Cauchy complete Archimedean ordered fields. If the latter is the case, then one might have to equip Cauchy complete Archimedean ordered fields with the additional structure of a principal square root function in order to do constructive Euclidean geometry.