I don't have any problem with the general idea expressed below and my objection doesn't apply at all to the free category construction, but I just wanted to point out that seeing constructible numbers as infinite decimals just does not work. Bishop in his book Constructive Analysis, gives an example of two numbers with constructible decimal expansion of which no single digit of the sum is (currently) constructible. I don't think this problem would arise in pi^2, but who knows. At any rate, for him a constructible is given by a sequence of rationals q_1,q_2,..., whose numerators and denominators are recursively enumerable sequences of integers and for which |q_n - q_m| < 1/n + 1/m. When you add two such sequences, you have to take every second term of the sum and multiplication involves more drastic trimming. Moreover, division is possible only if you can prove that eventually |q_n| > 1/N for some fixed N. So what you get is a local ring, not a field. On Thu, 9 Jun 2005, Steve Vickers wrote:
Dear Bill,
Most constructivists would not have problems with this, despite the fact that at any finite stage of the construction you have only a finite approximation to the infinite category. Eventually (in finite time) you can get any finite part of the category, including the knowledge of any finite set of the equalities between objects or morphisms, and that is normally considered good enough.
Computationally, a programming language such as Haskell is happy to deal with infinite objects. The computations never terminate, but every finite approximation to the object is obtained in finite time. For instance, one function might generate the decimal expansion of pi and another function may take that as input and calculate its square.
In topos-valid constructivism the way it works is this. In an arbitrary elementary topos you can't always construct the free categories over graphs. But as soon as you admit a natural numbers object other free algebra constructions, such as the free category, come along with it.
Regards,
Steve Vickers.
Galchin Vasili wrote:
Hello,
Let G be a directed graph that either has an infinite # of nodes or has edges which are loops.
Would a constructist recognize the existence of G's free category?
Thank you, Bill Halchin
10-Jun-2005 11:54:26 -0300,6270;000000000000-0000000e