请输入您要查询的字词:

 

单词 113CauchyReals
释义

11.3 Cauchy reals


The Cauchy reals are, by intent, the completion of under limits of Cauchy sequencesPlanetmathPlanetmath.In the classical construction of the Cauchy reals, we consider the set 𝒞 of all Cauchy sequences in and then form a suitable quotient 𝒞/.Then, to show that 𝒞/ is Cauchy completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we consider a Cauchy sequence x:𝒞/, lift it to a sequencePlanetmathPlanetmath of sequences x¯:𝒞, and construct the limit of x using x¯. However, the lifting of x to x¯ usesthe axiom of countable choice (the instance of (LABEL:eq:ac) where X=) or the law of excluded middleMathworldPlanetmathPlanetmath, which we may wish to avoid.Every construction of reals whose last step is a quotient suffers from this deficiency.There are three common ways out of the conundrum in constructive mathematics:

  1. 1.

    Pretend that the reals are a setoid (𝒞,), i.e., the type ofCauchy sequences 𝒞 with a coincidence relationMathworldPlanetmathPlanetmathPlanetmath attached to it byadministrative decree. A sequence of reals then simply is a sequence of Cauchysequences representing them.

  2. 2.

    Give in to temptation and accept the axiom of countable choice. After all, the axiomis valid in most models of constructive mathematics based on a computational viewpoint,such as realizability models.

  3. 3.

    Declare the Cauchy reals unworthy and construct the Dedekind reals instead.Such a verdict is perfectly valid in certain contexts, such as in sheaf-theoretic models of constructive mathematics.However, as we saw in \\autorefsec:dedekind-reals, the constructive Dedekind reals have their own problems.

Using higher inductive types, however, there is a fourth solution, which we believe to be preferable to any of the above, and interesting even to a classical mathematician.The idea is that the Cauchy real numbers should be the free complete metric space generated by .In general, the construction of a free gadget of any sort requires applying the gadget operationsMathworldPlanetmath repeatedly many times to the generatorsPlanetmathPlanetmathPlanetmath.For instance, the elements of the free groupMathworldPlanetmath on a set X are not just binary productsPlanetmathPlanetmathPlanetmathPlanetmath and inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of elements of X, but words obtained by iterating the product and inverse constructions.Thus, we might naturally expect the same to be true for Cauchy completion, with the relevant “operation” being “take the limit of a Cauchy sequence”.(In this case, the iteration would have to take place transfinitely, since even after infinitely many steps there will be new Cauchy sequences to take the limit of.)

The argument referred to above shows that if excluded middle or countable choice hold, then Cauchy completion is very special: when building the completion of a space, it suffices to stop applying the operation after one step.This may be regarded as analogous to the fact that free monoids and free groups can be given explicit descriptions in terms of (reduced) words.However, we saw in \\autorefsec:free-algebras that higher inductive types allow us to construct free gadgets directly, whether or not there is also an explicit description available.In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we show that the same is true for the Cauchy reals (a similar technique would construct the Cauchy completion of any metric space; see \\autorefex:metric-completion).Specifically, higher inductive types allow us to simultaneously add limits of Cauchy sequences and quotient by the coincidence relation, so that we can avoid the problem of lifting a sequence of reals to a sequence of representatives.

随便看

 

数学辞典收录了18232条数学词条,基本涵盖了常用数学知识及数学英语单词词组的翻译及用法,是数学学习的有利工具。

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 15:51:24