Timeline for Are real numbers countable in constructive mathematics?
Current License: CC BY-SA 2.5
45 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 16, 2021 at 6:47 | comment | added | Andrej Bauer | @red_trumpet: you are assuming that for all real numbers $x$ and rationals $c$ either $c < x$ or $c \geq x$. This is an instance of Excluded middle which is not provable constructively (you can only use those instances of excluded middle that you can prove). | |
| Jul 15, 2021 at 21:25 | comment | added | red_trumpet | I'm not versed in that stuff and I wonder what you mean by "this is ok by Countable choice". Couldn't you just say pick the first option if $c < x$ and the second option if $c \geq x$? Then everything is well-defined so there is no need for a Choice? | |
| Jun 15, 2020 at 7:27 | history | edited | CommunityBot |
Commonmark migration
|
|
| Jul 6, 2010 at 13:07 | comment | added | Vag | @Andrej Bauer: I've stated exactly the same in previous comment. | |
| Jul 6, 2010 at 13:02 | comment | added | Vag | @Carl Mummet: "I was talking about sets of natural numbers" Sorry. (and I swept that comment under the rug) (I just forgot that $w$ means Nats) | |
| Jul 6, 2010 at 12:57 | comment | added | Andrej Bauer | @Vag: You can define a set of lambda terms which denote real numbers (this set is not r.e.). Then you can define a map $f$ from this set to the reals, i.e., a functional relation (I think you would call this left unique right total, or the other way around, I am not sure). You cannot define a map going from reals to lambda terms constructively. You cannot show thow that $f$ is surjective, and you cannot show that $f$ is not surjective. You need additional assumptions to conclude anything specific about $f$. | |
| Jul 6, 2010 at 12:52 | comment | added | Vag | So I can define constructive undecidable uncomputable predicate "every sequence corresponds to some lambda term". But I'm unable to prove constructively that this relation is right unique, nor left total. Right? | |
| Jul 6, 2010 at 12:48 | comment | added | Vag | @Andrej Bauer: "your set of lambda terms denoting the real numbers is not definable in your sense" Yes, and this is the whole point of my question: there is no constructive function from series to lambda terms. | |
| Jul 6, 2010 at 12:43 | comment | added | Vag | I've never thought about some undecidable predicate P(x) as about definition of some subset of A. When I talked about definition of subset of A, I've talked about characteristic function. My bad. | |
| Jul 6, 2010 at 12:24 | comment | added | Vag | @Andrej Bauer: "at this point you should consult the literature and come back telling us which particular" Unified Theory of Types by Zhaohui Luo. I formalize all my home reasoning in Agda wiki.portal.chalmers.se/agda for example vag.biz.nf/theories/AgdaIsTuringComplete.html | |
| Jul 6, 2010 at 12:24 | comment | added | Carl Mummert | @Vag: I don't know what it would even mean for that set to be enumerable. I was talking about sets of natural numbers. | |
| Jul 6, 2010 at 12:21 | comment | added | Carl Mummert | @Andrej Bauer: I politely disagree with "But that is no way to talk about real numbers or any sort of real math. " and point to the reverse mathematics program. The results that I have seen in constructive reverse mathematics can be all viewed as results about subsystems of HA${}^\omega$ plus fragments of classical logic. | |
| Jul 6, 2010 at 12:16 | comment | added | Carl Mummert | @Vag: as Andrej Bauer was saying, few constructivists look at things that way. They would say the set is obviously definable, but membership in it cannot be decided. Given that they can't even prove that an arbitrary element is either in the set or not in the set, why would they assume every set is decidable? | |
| Jul 6, 2010 at 12:14 | comment | added | Andrej Bauer | @Vag: and as Carl mentions, your set of lambda terms denoting the real numbers is not definable in your sense. The only difference seems to be that you call "constructive" what I call "decidable". Constructive is a wider notion than decidable. | |
| Jul 6, 2010 at 12:13 | comment | added | Andrej Bauer | @Vag: at this point you should consult the literature and come back telling us which particular formal system of constructive mathematics you have in mind. You are certainly not talking about intuitionistic HOL (higher-order logic) with natural numbers, because that is the internal language of a topos, and everything I wrote can be done in a topos. | |
| Jul 6, 2010 at 12:11 | comment | added | Andrej Bauer | @Carl: thank you for pointing out the difference. Obviously, Vag is thinking of something like $HA^\omega$ and sets given as characteristic maps into $\lbrace 0, 1 \rbrace$. But that is no way to talk about real numbers or any sort of real math. At any rate, the phrase "constructive mathematics" does not normally mean $HA^\omega$. | |
| Jul 6, 2010 at 12:10 | comment | added | Carl Mummert | @Vag: seeing your most recent comment, now I am sure you should simply read Andrej's comments as proving what you agree with, namely that certain sets of lambda terms don't exist. In many branches of constructive mathematics, they are very willing to have sets that do not have characteristic functions, while if you think of sets as a data type "Set" then you are really thinking about characteristic functions, not sets. In your original proof, the "set" of lambda terms that encode real numbers is another set you cannot prove to exist, because there is no effective decision procedure for it. | |
| Jul 6, 2010 at 12:08 | comment | added | Andrej Bauer | @Vag: finally we arrive at the point of misunderstanding. This is a constructive definition. You think that all predicates must be decidable in constructive mathematics, or perhaps that subsets can only be formed by decidable predicates, but that is not the case. That is not what constructive mathematics is. | |
| Jul 6, 2010 at 12:05 | comment | added | Carl Mummert | There is a tension in constructive systems between these principles: (1) every sufficiently well-defined property of an element of $\omega$ determines a subset of $\omega$ and (2) every subset of $\omega$ can be enumerated. Constructive set theories such as IZF validate (1) and not (2). However, constructive systems such as HA<sup>$\omega$</sup> validate (2) and not (1). In that setting, "sets" are actually coded by their characteristic functions in $2^\omega$, and of course if you have the characteristic function of a set you can enumerate it, since equality on the set {0,1} is decidable. | |
| Jul 6, 2010 at 12:02 | comment | added | Vag | "such that ts=0 for all lambda terms s (of type ) form a set which is not r.e." -- this is not constructive definition since termination of any term is undecidable. | |
| Jul 6, 2010 at 11:57 | comment | added | Carl Mummert | @Vag: it might be clearer (I don't know) if, instead of reading Andrej Bauer's argument as showing that some set is not enumerable, you read it as showing that certain "sets" don't actually exist. See my next comment. | |
| Jul 6, 2010 at 11:52 | comment | added | Andrej Bauer | If you want a non-r.e. set of lambda terms: those lambda terms $t$ (of type $\mathbb{N} \to \mathbb{N}$ if you have types) such that $t s = 0$ for all lambda terms $s$ (of type $\mathbb{N}$) form a set which is not r.e. | |
| Jul 6, 2010 at 11:46 | comment | added | Andrej Bauer | @Vag: Your argument for "every set of lambda terms is r.e." is too vague for me to understand. Or perhaps you're using the wrong definition of r.e. A set is r.e. if there is an algorithm enumerating all its elements (with repetitions) and no other elements. The set of natural numbers that are codes of noh-halting Turing machines is not r.e. This is in every book on computability, see for example Roger's "Theory of Recursive functions and Effective Computability". | |
| Jul 6, 2010 at 11:01 | comment | added | Vag | @Andrej Bauer: huge thanks for reference to the book. | |
| Jul 6, 2010 at 10:57 | comment | added | Vag | @Andrej Bauer: "Where is this argument of yours that all sets are r.e.?" Any variable name might be serialized to chain of bits. So inductively defined lambda term might be serialized to chain of bits. So, any lambda term may be serialized. Chain of bits is equivalent to a natural number. So there are injective mapping from lambda terms to natural numbers. So, for some given lambda term, if some algorithm will count from one to infinity it eventually riches a number for that term. This implies any set of lambda term recursively enumerable. | |
| Jul 6, 2010 at 10:50 | comment | added | Vag | @Andrej Bauer: "infinitely long discussion". I haven't intended that. Sorry for such an impression. I'll stop asking questions in comments now. | |
| Jul 6, 2010 at 10:29 | comment | added | Andrej Bauer | @Vag: I am not sure we're meant to have an infinitely long discussion in the comment's area. Chaitin's number $\Omega$ cannot be shown to exist constructively because there is a model of constructive mathematics (namely the effective topos) in which $\Omega$ does not exist. | |
| Jul 6, 2010 at 10:27 | comment | added | Andrej Bauer | @Vag: Where is this argument of yours that all sets are r.e.? The set of codes of non-halting Turing machines isnot r.e. Regarding reals and lambda terms: you cannot prove in pure IHOL that every real has a lambda term denoting it, you need something like the formal Church's thesis to prove that. I think it would be helpful if we agreed on what is meant by "constructive" here. There are many kinds of constructivism. Have you had a look at the literature, for example at the Bridges and Richman's "Varities of Constructivism" or Troelstra and van Dalen's "Constructivism in mathematics"? | |
| Jul 6, 2010 at 10:08 | comment | added | Vag | Is this possible to build lambda term that represents Chaitin number $\Omega$? | |
| Jul 6, 2010 at 9:47 | comment | added | Vag | I use word "constructive" to describe any reasoning in intuitionistic HOL that is not inside $\neg \neg$. | |
| Jul 6, 2010 at 9:41 | comment | added | Vag | At least two pure constructive ways exist to state one-to-oneness of given relation 1) pair of functions f and g that f o g = id and g o f = id and 2) state that relation is left total, right total, left unique and right unique. (2) is strictly weaker than (1). | |
| Jul 6, 2010 at 9:29 | comment | added | Vag | @Andrej Bauer: "to build" means to devise a formula in constructive subset of HOL which 1) being given any object, decides is this object a lambda term or not and 2) states that there exists an one-to-one relation P between lambda terms built in (1) and reals. Important thing that one-to-onenness might be stated in various ways, maybe that matters? (e.g. vag.biz.nf/theories/Rel.html#2174 ) And how to live with my steel argument about enumerability of any set of lambda terms? | |
| Jul 6, 2010 at 9:06 | comment | added | Andrej Bauer | @Vag: even constructively speaking, we can of course define many different sets. There is absolutely nothing problematic about considering the set of those $\lambda$-terms that have some well-defined property. Perhaps you think that constructively we are only allowed to define those sets which can somehow be "constructed" in a very explicit way (enumerated perhaps)? Is that what is puzzling you? You used the phrase "build a set". What do you mean by that? My arguments are entirely standard with respect to Bishop-style constructivism. | |
| Jul 6, 2010 at 8:53 | comment | added | Vag | @Andrej Bauer: I do not understand why you claim that this is possible to build such a set of lambda terms that represents all possible converging sequences. | |
| Jul 6, 2010 at 8:41 | comment | added | Andrej Bauer | @Vag: Well, not every set of lambda terms can be r.e., as there are uncountably many such sets. If the set of lambda terms representing nested sequences whose widths converge to zero were r.e., then we could solve the Halting problem. (Given a machine $T$, construct a term representing the sequence $[a_n, b_n]$ such that $[a_n,b_n] = [0,2^{-n}]$ if $T$ has not stopped within $n$ steps and $[a_n,b_n] = [0,2^{-k}]$ if it stopped at step $k \leq n$. Then $T$ diverges iff the term represents a real number, so we can semidecide non-halting as well as halting. This is a standard argument.) | |
| Jul 6, 2010 at 8:27 | comment | added | Vag | @Andrej Bauer: But I still do not understand. Any lambda term may be serialized to natural number. This implies that ANY set of lambda terms is recursively enumerable. Right? | |
| Jul 6, 2010 at 8:09 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
fixed the condition for non-r.e. of nested sequences to include convergence to 0
|
| Jul 6, 2010 at 8:08 | comment | added | Andrej Bauer | @Vag: agreed, I was not precise enough. The set of lambda terms which represent sequences of nested intervals whose widths converge to 0 is not recursively enumerable. | |
| Jul 6, 2010 at 7:17 | comment | added | Vag | Set of lambda terms which represent sequences of nested intervals with rational endpoints IS recursively enumerable. But there are no function from series to lambda terms. | |
| Jul 6, 2010 at 6:33 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
Fixed initial interval from [0,2] to [0,1].
|
| Jul 6, 2010 at 6:31 | comment | added | Andrej Bauer | @Carl: I have wondered about it myself on several occasions. I do not know a proof of uncountability of Dedekind reals which avoids choice. I asked around and never got an answer so as far as I am concerned, this is an open question. | |
| Jul 6, 2010 at 6:28 | comment | added | Vag | Thanks! Convergence fixed. It was not "fushy" but mountain sized flaw. | |
| Jul 5, 2010 at 23:16 | comment | added | Carl Mummert | +1. This is a fine proof in Bishop's system. Do you know how the proof goes in CZF without countable choice? I assume the uncountability of the Dedekind reals is provable there, but I'm not very familiar with the system. | |
| Jul 5, 2010 at 23:06 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
Fixed indices in math.
|
| Jul 5, 2010 at 22:47 | history | answered | Andrej Bauer | CC BY-SA 2.5 |