Martin Escardó came up with the following puzzle. Is there a constructive proof of the following statement:
For every h : (N -> N) -> N there exist f, g : N -> N and k : N such that h f = h g and f k != g k.
This is a positive way of saying that there is no injection h from the Baire space to natural numbers. It is easy to come up with a proof in the following cases:
(a) assuming classical logic (b) assuming even a modest amount of continuity principles (such as all maps are sequentially continuous, but also less will do)
But can we have a Bishop-style proof, or a counter-model? Note that the effective topos is not a counter-model because h is supposed to be extensional (so in particular it is not allowed to map (the realizer of) a function to its realizer).
> Martin Escardó came up with the following puzzle. Is there a > constructive proof of the following statement:
> For every h : (N -> N) -> N there exist f, g : N -> N and k : N > such that h f = h g and f k != g k.
> This is a positive way of saying that there is no injection h from the > Baire space to natural numbers. It is easy to come up with a proof in > the following cases:
> (a) assuming classical logic > (b) assuming even a modest amount of continuity principles (such as > all maps are sequentially continuous, but also less will do)
> But can we have a Bishop-style proof, or a counter-model? Note that > the effective topos is not a counter-model because h is supposed to be > extensional (so in particular it is not allowed to map (the realizer > of) a function to its realizer).
> I believe there is no such Bishop-style constructive proof.
> Regards, > Martin
> On 01/06/11 13:03, Andrej Bauer wrote: >> Martin Escardo came up with the following puzzle. Is there a >> constructive proof of the following statement:
>> For every h : (N -> N) -> N there exist f, g : N -> N and k : N >> such that h f = h g and f k != g k.
>> This is a positive way of saying that there is no injection h from the >> Baire space to natural numbers. It is easy to come up with a proof in >> the following cases:
>> (a) assuming classical logic >> (b) assuming even a modest amount of continuity principles (such as >> all maps are sequentially continuous, but also less will do)
>> But can we have a Bishop-style proof, or a counter-model? Note that >> the effective topos is not a counter-model because h is supposed to be >> extensional (so in particular it is not allowed to map (the realizer >> of) a function to its realizer).
It depends on how we understand injection. In the strict Markov constructive approach, every function N--> N is an algorithm and thus, has its code, so there is a natural injection in this sense
Of course, it is not possible to have an algorithm that would assign the same number every time two algorithms compute the same function. The impossibility comes from the impossibility to have a zero-checker, i.e., to check whether an (everywhere defined) algorithm f: N -> N always returns 0.
________________________________________ From: constructivenews@googlegroups.com [constructivenews@googlegroups.com] On Behalf Of Fred Richman [rich...@fau.edu] Sent: Wednesday, June 01, 2011 12:15 PM To: constructivenews@googlegroups.com Subject: Re: A puzzle
Is there a constructive proof of the weaker theorem that there is no injection from N -> N to N?
> I believe there is no such Bishop-style constructive proof.
> Regards, > Martin
> On 01/06/11 13:03, Andrej Bauer wrote: >> Martin Escardo came up with the following puzzle. Is there a >> constructive proof of the following statement:
>> For every h : (N -> N) -> N there exist f, g : N -> N and k : N >> such that h f = h g and f k != g k.
>> This is a positive way of saying that there is no injection h from the >> Baire space to natural numbers. It is easy to come up with a proof in >> the following cases:
>> (a) assuming classical logic >> (b) assuming even a modest amount of continuity principles (such as >> all maps are sequentially continuous, but also less will do)
>> But can we have a Bishop-style proof, or a counter-model? Note that >> the effective topos is not a counter-model because h is supposed to be >> extensional (so in particular it is not allowed to map (the realizer >> of) a function to its realizer).
I think it is made clear in the original post (not mine) that "injection" means an extensional function, specifically precluding the natural injection to which you refer (the stuff about realizers in an effective topos).
I don't think I understand the import of the second statement. While it is contradictory in the strict Markov constructive approach for there to exist an injection from N --> N into N, the original question referred to Bishop-style constructive mathematics.
> It depends on how we understand injection. In the strict Markov > constructive approach, every function N--> N is an algorithm and thus, has > its code, so there is a natural injection in this sense
> Of course, it is not possible to have an algorithm that would assign the > same number every time two algorithms compute the same function. The > impossibility comes from the impossibility to have a zero-checker, i.e., > to check whether an (everywhere defined) algorithm f: N -> N always > returns 0.
> ________________________________________ > From: constructivenews@googlegroups.com > [constructivenews@googlegroups.com] On Behalf Of Fred Richman > [rich...@fau.edu] > Sent: Wednesday, June 01, 2011 12:15 PM > To: constructivenews@googlegroups.com > Subject: Re: A puzzle
> Is there a constructive proof of the weaker theorem that there is no > injection from N -> N to N?
> --Fred
>> I believe there is no such Bishop-style constructive proof.
>> Regards, >> Martin
>> On 01/06/11 13:03, Andrej Bauer wrote: >>> Martin Escardo came up with the following puzzle. Is there a >>> constructive proof of the following statement:
>>> For every h : (N -> N) -> N there exist f, g : N -> N and k : N >>> such that h f = h g and f k != g k.
>>> This is a positive way of saying that there is no injection h from the >>> Baire space to natural numbers. It is easy to come up with a proof in >>> the following cases:
>>> (a) assuming classical logic >>> (b) assuming even a modest amount of continuity principles (such as >>> all maps are sequentially continuous, but also less will do)
>>> But can we have a Bishop-style proof, or a counter-model? Note that >>> the effective topos is not a counter-model because h is supposed to be >>> extensional (so in particular it is not allowed to map (the realizer >>> of) a function to its realizer).
In Russian constructivism/effective topos the proof is easy, since all functions are sequentially continuous in the effective topos (and those from N→N to N are also δ-ε continuous). So I don't think Russian constructivism really sheds any light here.
The question is, how would Bishop marry the classical proof with one relying on a continuity principle? Note that Ishihara's tricks don't seem helpful here. I am not at all convinced that there is no constructive proof because I have great trouble imagining what a counter-model might look like.
Sorry for answering out of sync, we studied the original Bishop's book in detail, I am not 100% sure about formalization. Let me give one more try, I may be out of sync again.
If we had an injective mapping I: (N->N)-> N, then, since equality on N is clearly decidable, we will be able to check whether mapping f:N->N and g:N->N are equal or not, by comparing I(f) and I(g). In particular, this applies to mappings f,g:N -> {0,1}, when g is always 0. In this case, I(f) = I(g) <-> exists n(f(n)=0), so we would have a statement
forall n (Pn \/ ~Pn) --> (exists n Pn \/ ~exists n Pn)
which is as non-constructive as they make them (all Bishop's counterexamples are based on this). Maybe this is not valid in formalized Bishop, but at least it reduces the original question to the more fundamental ones like decidability of equality of real numbers (or binary sequences), and this is not directly related to continuity.
________________________________________ From: constructivenews@googlegroups.com [constructivenews@googlegroups.com] On Behalf Of Andrej Bauer [andrej.ba...@andrej.com] Sent: Thursday, June 02, 2011 7:07 AM To: constructivenews@googlegroups.com Subject: Re: A puzzle
In Russian constructivism/effective topos the proof is easy, since all functions are sequentially continuous in the effective topos (and those from N→N to N are also δ-ε continuous). So I don't think Russian constructivism really sheds any light here.
The question is, how would Bishop marry the classical proof with one relying on a continuity principle? Note that Ishihara's tricks don't seem helpful here. I am not at all convinced that there is no constructive proof because I have great trouble imagining what a counter-model might look like.
It is certainly true that if we had an injection from N -> N to N, then we could prove LPO. So we can't prove the existence of such an injection within Bishop's mathematics. That is not the same as saying that we can derive a contradiction from the existence of such an injection. Because LPO is provable in classical mathematics, it is consistent with Bishop's mathematics.
I'm out of my depth here, but is there any reason to think that one can refute, within Bishop's mathematics, the proposition that any discrete set is embeddable in N? Even assuming LPO?
A classical proof that N -> N cannot be embedded in N uses the law of excluded middle to show that such an embedding would make N -> N countable, which we know is impossible. However, I don't see how LPO would suffice. A virtue, as I see it, of considering the weak question is that we put ourselves in a semiclassical environment (we have LPO) so we are not so tempted to worry about continuity principles.
> Sorry for answering out of sync, we studied the original Bishop's book in > detail, I am not 100% sure about formalization. Let me give one more try, > I may be out of sync again.
> If we had an injective mapping I: (N->N)-> N, then, since equality on N is > clearly decidable, we will be able to check whether mapping f:N->N and > g:N->N are equal or not, by comparing I(f) and I(g). In particular, this > applies to mappings f,g:N -> {0,1}, when g is always 0. In this case, I(f) > = I(g) <-> exists n(f(n)=0), so we would have a statement
> forall n (Pn \/ ~Pn) --> (exists n Pn \/ ~exists n Pn)
> which is as non-constructive as they make them (all Bishop's > counterexamples are based on this). Maybe this is not valid in formalized > Bishop, but at least it reduces the original question to the more > fundamental ones like decidability of equality of real numbers (or binary > sequences), and this is not directly related to continuity.
> ________________________________________ > From: constructivenews@googlegroups.com > [constructivenews@googlegroups.com] On Behalf Of Andrej Bauer > [andrej.ba...@andrej.com] > Sent: Thursday, June 02, 2011 7:07 AM > To: constructivenews@googlegroups.com > Subject: Re: A puzzle
> In Russian constructivism/effective topos the proof is easy, since all > functions are sequentially continuous in the effective topos (and > those from N→N to N are also δ-ε continuous). So I > don't think Russian > constructivism really sheds any light here.
> The question is, how would Bishop marry the classical proof with one > relying on a continuity principle? Note that Ishihara's tricks don't > seem helpful here. I am not at all convinced that there is no > constructive proof because I have great trouble imagining what a > counter-model might look like.
In the language of Bishop's book, you have proved that there does _not_ exist an injection from N -> N to N. But you haven't proved that there does not exist an injection from N -> N to N. Note the placement of italics, which make for a weaker statement.
The following is intended to contribute to the discussion whether continuity is needed to prove that all functions f : (N -> N) -> N are non-injective.
Let X be a set (we are mainly interested in X : = N -> N) which is non-countable (every f : N -> X is non-surjective) and has property
E: for every f : X -> N the image Im(f) is countable.
Then every f : X -> N is non-injective.
Below you find a proof and detailed definitions.
I'm mainly interested in property E which seems to be a weakening of the statement that every f : X -> N is continuous, but doesn't mention topology. I'll be grateful for any hints as to where a property like E is discussed.
Ulrich
Definitions ===========
We let N be the set of natural numbers, "=" means "equal" and "#" means "apart". We don't specify these relations precisely, but only assume that "=" is symmetric and transitive and "#" is symmetric.
A function f : X -> Y is
* injective if for all x,x' in X, if x # x', then f x # f x' * surjective if for all y in Y there exists x in X such that f x = y * non-injective if there exist x,x' in X such that x # x', but f x = f x' * non-surjective if there exists y in Y such that for all x in X, f x # y
A set X is
* countable if there exists a surjective f : N -> X * discrete if there exists an injective f : X -> N * non-countable if all f : N -> X are non-surjective * non-discrete if all f : X -> N are non-injective
(my apologies if these definitions do not exactly conform with the conventions used in the literature on constructive mathematics)
A set X has property E if for all f : X -> N the image Im(f) := {f x | x in X} is countable.
Theorem (Countable Choice) ======= If X is non-countable and has property E, then X is non-discrete.
Proof ===== Let f : X -> N. We show that f is non-injective. Since X has property E, there exists a surjective g : N -> Im(f). Hence (1) for all n in N exists x in X, f x = g n (2) for all x in X exists n in N, f x = g n. By (1) and Countable Choice, there exists h : N -> X such that (3) for all n in N, f(h n) = g n. Since X is non-countable, there exists x0 in X such that (4) for all n in N, h n # x0. By (2), there exists n0 in N such that (5) f x0 = g n0. Set x1 := h n0. Then x1 # x0, by (4), and f x1 = f(h n0) = g n0 = f x0, by (3) and (5).
Corollary (Countable Choice) ========= If N -> N has property E, then N -> N is non-discrete.
Proof ===== By diagonalization, N -> N is non-countable. Hence the Theorem applies. Here we assume that for N the relations "=" and "#" have their usual meanings, and for f,g : N -> N we define f = g :<=> for all n in N, f n = g n, f # g :<=> exists n in N, f n # g n.
Discussion of property E ======================== Property E for N -> N follows from the assumption that all functions f : (N -> N) -> N are continuous. We let g : N -> (N -> N) simply enumerate a countable dense subset of N -> N (e.g. all functions that are eventually 0). Then (f o g) : N -> Im(f) is surjective. So, E is somehow a weak continuity statement. How weak is it? Has it been considered before? If yes, how is it called (forgive my ignorance of the literature)? The nice thing about E is that (a) it doesn't assume any structure on X (such as a topology), and (b) classically, it holds for all non-empty sets (more precisely, inhabited sets).
Of course, non-discreteness of N -> N follows directly (without using countable choice) from the assumption that all f : (N -> N) -> N are continuous.
> In Russian constructivism/effective topos the proof is easy, since all > functions are sequentially continuous in the effective topos (and > those from N→N to N are also δ-ε continuous). So I don't think Russian > constructivism really sheds any light here.
> The question is, how would Bishop marry the classical proof with one > relying on a continuity principle? Note that Ishihara's tricks don't > seem helpful here. I am not at all convinced that there is no > constructive proof because I have great trouble imagining what a > counter-model might look like.
> The following is intended to contribute to the discussion > whether continuity is needed to prove that all functions > f : (N -> N) -> N are non-injective.
> Let X be a set (we are mainly interested in X : = N -> N) > which is non-countable (every f : N -> X is non-surjective) > and has property
> E: for every f : X -> N the image Im(f) is countable.
> Then every f : X -> N is non-injective.
> Below you find a proof and detailed definitions.
> I'm mainly interested in property E which seems to be a weakening > of the statement that every f : X -> N is continuous, but > doesn't mention topology. I'll be grateful for any hints as to > where a property like E is discussed.
> Ulrich
> Definitions > ===========
> We let N be the set of natural numbers, > "=" means "equal" and "#" means "apart". > We don't specify these relations precisely, but only assume that > "=" is symmetric and transitive and "#" is symmetric.
> A function f : X -> Y is
> * injective if for all x,x' in X, if x # x', then f x # f x' > * surjective if for all y in Y there exists x in X such that f x = y > * non-injective if there exist x,x' in X such that x # x', > but f x = f x' > * non-surjective if there exists y in Y such that for all x in X, > f x # y
> A set X is
> * countable if there exists a surjective f : N -> X > * discrete if there exists an injective f : X -> N > * non-countable if all f : N -> X are non-surjective > * non-discrete if all f : X -> N are non-injective
> (my apologies if these definitions do not exactly conform with > the conventions used in the literature on constructive mathematics)
> A set X has property E if for all f : X -> N > the image Im(f) := {f x | x in X} is countable.
> Theorem (Countable Choice) > ======= > If X is non-countable and has property E, then X is non-discrete.
> Proof > ===== > Let f : X -> N. We show that f is non-injective. > Since X has property E, there exists a surjective g : N -> Im(f). > Hence (1) for all n in N exists x in X, f x = g n > (2) for all x in X exists n in N, f x = g n. > By (1) and Countable Choice, there exists h : N -> X such that > (3) for all n in N, f(h n) = g n. > Since X is non-countable, there exists x0 in X such that > (4) for all n in N, h n # x0. > By (2), there exists n0 in N such that > (5) f x0 = g n0. > Set x1 := h n0. Then x1 # x0, by (4), and f x1 = f(h n0) = g n0 = f x0, > by (3) and (5).
> Corollary (Countable Choice) > ========= > If N -> N has property E, then N -> N is non-discrete.
> Proof > ===== > By diagonalization, N -> N is non-countable. Hence the Theorem applies. > Here we assume that for N the relations "=" and "#" have their usual > meanings, and for f,g : N -> N we define > f = g :<=> for all n in N, f n = g n, > f # g :<=> exists n in N, f n # g n.
> Discussion of property E > ======================== > Property E for N -> N follows from the assumption that all functions > f : (N -> N) -> N are continuous. We let g : N -> (N -> N) simply > enumerate a countable dense subset of N -> N (e.g. all functions > that are eventually 0). Then (f o g) : N -> Im(f) is surjective. > So, E is somehow a weak continuity statement. How weak is it? > Has it been considered before? If yes, how is it called (forgive my > ignorance of the literature)? The nice thing about E is that > (a) it doesn't assume any structure on X (such as a topology), and > (b) classically, it holds for all non-empty sets (more precisely, > inhabited sets).
> Of course, non-discreteness of N -> N follows directly > (without using countable choice) from the assumption that > all f : (N -> N) -> N are continuous.
> On 02/06/11 14:07, Andrej Bauer wrote: >> In Russian constructivism/effective topos the proof is easy, since all >> functions are sequentially continuous in the effective topos (and >> those from N→N to N are also δ-ε continuous). So I don't think Russian >> constructivism really sheds any light here.
>> The question is, how would Bishop marry the classical proof with one >> relying on a continuity principle? Note that Ishihara's tricks don't >> seem helpful here. I am not at all convinced that there is no >> constructive proof because I have great trouble imagining what a >> counter-model might look like.
The diagonalisation argument proves no surjection from S to S -> V (under the assumption that V has a self-mapping with no fixed point). Classically (using full AC), this means no injection from S -> V to S. The question is whether the latter can also be proved constructively.
When V is the set of truth values (so S -> V is the power set of S), then we can do this (impredicatively), using an argument that may be found in Proposition 2.8.8 of Paul Taylor's Practical Foundations of Mathematics (and summarised by me at <http://ncatlab.org/nlab/show/Cantor%27s+theorem>). But the argument doesn't generalise to arbitrary V.
So here we're considering the case where V is the set of natural numbers, and also specialising to the case where S is the same set.
(OK, that's all pretty obvious, but maybe Taylor's proof is of interest. By the way, at the end of the Interpretation section on the nLab page, I made reference to a post by Paul about interpreting Cantor's Theorem. I no longer know where that post is; I added my remarks in 2009 July.)
In this message I want to put this question in context.
Paulo Oliva gave a very nice talk at MFPS last week, in which he extracted, using the dialectica interpretation of the negative translation, a system-T+bar-recursion realizer of non-injectivity from a classical proof with countable choice, *without* assuming continuity. However, in order to have bar recursion (to interpret countable choice via the double negation shift) one needs to assume something (continuity is enough, majorizability is enough too, and other more general things may also be enough).
Then Paulo asked me to advertise the puzzle to functional programmers: can they come up with a program directly, without the detour of extracting a program from a (classical) proof? Yes, they can (in the Agda mailing list), it turns out, but the three proposed solutions used continuity (although apparently two of the (correct) proposers were not really familiar with continuity, it seems - they just used intuition).
In that message to the other list, I claimed to believe that there was no (pure) constructive proof of that, and Andrej then thought about this and decided to put the question to you in this list. I think it is an interesting problem.
Ulrich made the connection with continuity more explicit and topology-free, and this is nice, as I said (but I would say that, of course). Is there a direct connection with majorizability (other than the indirect connection mentioned above) too?
> I agree that non-injectivity sounds like a weakening of continuity, > Ulrich. Your topology-free, topological view of the situation is nice. > Martin
> On 02/06/11 18:07, Ulrich Berger wrote: >> The following is intended to contribute to the discussion >> whether continuity is needed to prove that all functions >> f : (N -> N) -> N are non-injective.
>> Let X be a set (we are mainly interested in X : = N -> N) >> which is non-countable (every f : N -> X is non-surjective) >> and has property
>> E: for every f : X -> N the image Im(f) is countable.
>> Then every f : X -> N is non-injective.
>> Below you find a proof and detailed definitions.
>> I'm mainly interested in property E which seems to be a weakening >> of the statement that every f : X -> N is continuous, but >> doesn't mention topology. I'll be grateful for any hints as to >> where a property like E is discussed.
>> Ulrich
>> Definitions >> ===========
>> We let N be the set of natural numbers, >> "=" means "equal" and "#" means "apart". >> We don't specify these relations precisely, but only assume that >> "=" is symmetric and transitive and "#" is symmetric.
>> A function f : X -> Y is
>> * injective if for all x,x' in X, if x # x', then f x # f x' >> * surjective if for all y in Y there exists x in X such that f x = y >> * non-injective if there exist x,x' in X such that x # x', >> but f x = f x' >> * non-surjective if there exists y in Y such that for all x in X, >> f x # y
>> A set X is
>> * countable if there exists a surjective f : N -> X >> * discrete if there exists an injective f : X -> N >> * non-countable if all f : N -> X are non-surjective >> * non-discrete if all f : X -> N are non-injective
>> (my apologies if these definitions do not exactly conform with >> the conventions used in the literature on constructive mathematics)
>> A set X has property E if for all f : X -> N >> the image Im(f) := {f x | x in X} is countable.
>> Theorem (Countable Choice) >> ======= >> If X is non-countable and has property E, then X is non-discrete.
>> Proof >> ===== >> Let f : X -> N. We show that f is non-injective. >> Since X has property E, there exists a surjective g : N -> Im(f). >> Hence (1) for all n in N exists x in X, f x = g n >> (2) for all x in X exists n in N, f x = g n. >> By (1) and Countable Choice, there exists h : N -> X such that >> (3) for all n in N, f(h n) = g n. >> Since X is non-countable, there exists x0 in X such that >> (4) for all n in N, h n # x0. >> By (2), there exists n0 in N such that >> (5) f x0 = g n0. >> Set x1 := h n0. Then x1 # x0, by (4), and f x1 = f(h n0) = g n0 = f x0, >> by (3) and (5).
>> Corollary (Countable Choice) >> ========= >> If N -> N has property E, then N -> N is non-discrete.
>> Proof >> ===== >> By diagonalization, N -> N is non-countable. Hence the Theorem applies. >> Here we assume that for N the relations "=" and "#" have their usual >> meanings, and for f,g : N -> N we define >> f = g :<=> for all n in N, f n = g n, >> f # g :<=> exists n in N, f n # g n.
>> Discussion of property E >> ======================== >> Property E for N -> N follows from the assumption that all functions >> f : (N -> N) -> N are continuous. We let g : N -> (N -> N) simply >> enumerate a countable dense subset of N -> N (e.g. all functions >> that are eventually 0). Then (f o g) : N -> Im(f) is surjective. >> So, E is somehow a weak continuity statement. How weak is it? >> Has it been considered before? If yes, how is it called (forgive my >> ignorance of the literature)? The nice thing about E is that >> (a) it doesn't assume any structure on X (such as a topology), and >> (b) classically, it holds for all non-empty sets (more precisely, >> inhabited sets).
>> Of course, non-discreteness of N -> N follows directly >> (without using countable choice) from the assumption that >> all f : (N -> N) -> N are continuous.
>> On 02/06/11 14:07, Andrej Bauer wrote: >>> In Russian constructivism/effective topos the proof is easy, since all >>> functions are sequentially continuous in the effective topos (and >>> those from N→N to N are also δ-ε continuous). So I don't think Russian >>> constructivism really sheds any light here.
>>> The question is, how would Bishop marry the classical proof with one >>> relying on a continuity principle? Note that Ishihara's tricks don't >>> seem helpful here. I am not at all convinced that there is no >>> constructive proof because I have great trouble imagining what a >>> counter-model might look like.
I tried to come up with a counter-example. There is apparently no proof of this, or someone would have found it by now. Therefore there is a counter-example (non-constructive argument there). Perhaps someone can complete the following.
Let h(f) be (the smallest index for) the proof that f is total. (If you want a model of HAS, then the proof should be in HAS; if you want IZF, then an IZF proof; etc.)
Problems: h is supposed to be total and extensional. So, think that you're living in the bottom node of a Kripke model, where you have some nice, even classical model, say of ZF, even ZFC, even ZFC + V=L. If f is some function which is not provably total, then there is a model in which f is not total. Append that as a successor node to bottom in the K model. So f is no longer total, even at bottom, and hence h(f) need not be defined. Now suppose f=g but not provably so. So there is a model in which f≠g. Append that as a successor node. Now even at bottom f≠g.
Biggest problem with this idea: Connecting terms in the language, that can provably stand for functions and might be proven to be total or not (such as formulas proven to have unique solutions, depending on your set-up), with actual functions in an actual model. The bottom node would have to have several copies of any function. For instance, the constant function 0 has many inequivalent descriptions, such as “f(n) = 0” and “f(n) = 0 as long as there is no proof < n of an inconsistency in ZF, else 1” and so on. So perhaps the bottom node could best stand being some sort of term model.
-----Original Message----- From: constructivenews@googlegroups.com [mailto:constructivenews@googlegroups.com] On Behalf Of Andrej Bauer Sent: Thursday, June 02, 2011 9:07 AM To: constructivenews@googlegroups.com Subject: Re: A puzzle
In Russian constructivism/effective topos the proof is easy, since all
functions are sequentially continuous in the effective topos (and
those from N→N to N are also δ-ε continuous). So I don't think Russian
constructivism really sheds any light here.
The question is, how would Bishop marry the classical proof with one
relying on a continuity principle? Note that Ishihara's tricks don't
seem helpful here. I am not at all convinced that there is no
constructive proof because I have great trouble imagining what a
Ulrich's contribution is indeed very nice. It helps us not to think about continuity. One small remark:
> E: for every f : X -> N the image Im(f) is countable.
> The nice thing about E is that [....] > (b) classically, it holds for all non-empty sets (more precisely, inhabited sets).
When I was a kid I learnt from Dana Scott that a set S is countable if there exists an onto map f : N -> 1 + S. Here 1 + S is the disjoint union of a singleton set and S. This definition is nice because it incorporates the empty set seamlessly, and it allows so "enumerate nothing" whenever that is convenient. I recommend teaching and defining countable in this way.
For example, with this definition of countable, classically every set hap property E.
>When I was a kid I learnt from Dana Scott that a set S is countable if >there exists an onto map f : N -> 1 + S. Here 1 + S is the disjoint >union of a singleton set and S. This definition is nice because it >incorporates the empty set seamlessly, and it allows so "enumerate >nothing" whenever that is convenient. I recommend teaching and >defining countable in this way.
Classical authorities disagree about whether the empty set is countable; it's interesting that constructivists, who have many classically equivalent options to choose from, agree on which to use but still disagree on this. (But at least we agree that inhabited finite sets are countable.)
I agree with Andre, but I've seen it worded differently: S is __countable__ if there are a decidable subset C of N and a surjection C to S. The nice thing about this is that it immediately generalises to a condition for a class of cardinalities to be a class of "small" cardinalities: it must be closed under decidable subsets and arbitrary quotients. (But then again, Andre's wording could be used here too.)
>> E: for every f : X -> N the image Im(f) is countable.
Speaking synthetically topologically, this looks like a weakening of "X is overt".
Let Sigma be an open-subset classifier, for example the closure of 2 under countable suprema. If Sigma is countably based, then every overt subset of N is countable, if I am not mistaken. Images of overt sets are overt. So, if X is overt then it has property E.
I will bet a beer that Ulrich's results can be reformulated using overtness, and then generalized.
I like the definition of "countable" that Andrej Bauer attributes to Dana Scott. But then I'm not surprised when Dana Scott comes up with something good.
Toby Bartels wrote: > Classical authorities disagree about whether the empty set is countable; > it's interesting that constructivists, who have many classically > equivalent options to choose from, agree on which to use but still > disagree on this. (But at least we agree that inhabited finite sets are > countable.)
I wonder how much disagreement there actually is on this. It seems to me that the model is the definition of "recursively enumerable" as the domain of a partial recursive function, which allows the set to be empty. I realize that Bishop gave the wrong definition, but isn't that ancient history?
After all what's in Jaap's book on realizability is called the van den Berg - Lubarsky - Streicher model of CZF validates that every set is subcountable, i.e. can be enumerated by a subset of N. So one can consistently have that N^N is subcountable. But, alas, this model validates that there can't be monic enumeration of N^N by a subset of N. That's really irritating.
The assumption that N->N can be embedded into N entails LPO but is
inconsistent with full
classical logic. Actually \Sigma_1^1 predicates on N can't be
decidable since otherwise we could apply second Cantor. Coquand and
Palmgren (1997) some time ago considered sheaf models over measure
spaces as models for such intermediate logics. Possibly, that's a good
place to look at?
Martin Escardo and Andrej Bauer asked if one could prove that
For every h : (N --> N) --> N there exist f, g : N --> N and k : N such that h f = h g and f k != g k.
using constructive logic, ie without excluded middle or continuity principles.
Ulrich Berger had an interesting idea but I haven't managed to absorb it yet. The following is based on Vladek Kreinovich's comments.
However, since this is not my usual kind of mathematics and I have had other things on my mind recently (my 80-year old children formerly known as parents and a local political issue that you can see at www.monad.me.uk) so please would someone else check whether this is ok. If it's not then maybe someone can turn it into a correct proof.
===
In order to give an answer to the question it is not necessary to study the general function-space N-->N, whatever that may mean. It is sufficient to consider some class of total functions that is enumerated by a binary function
epsilon: N --> (N-->N) or epsilon: N x N --> N
I call the composite
delta = h.epsilon : N --> (N--> N) --> N
a TRACE.
If a function delta: N --> N arises in this way from some h:(N-->N)-->N then it is EXTENSIONAL in the sense that, for all p, q: N,
(All k. epsilon p k = epsilon q k) ==> delta p = delta q.
We also call such a function DISCRIMINATING if, for all p, q: N,
(Some k. epsilon p k != epsilon q k) ==> delta p != delta q.
Since equality on N is decidable, this is equivalent to, for all p, q: N,
(All k. epsilon p k = epsilon q k) <== delta p = delta q
and also to
All n p k. (epsilon p k = epsilon q k \/ delta p != delta q).
Therefore an extensional discriminating trace delta for the class that is enumerated by epsilon makes
(All k. epsilon p k = epsilon q k) <==> delta p = delta q
for all p, q :N.
Now suppose that this class of total functions is sufficiently expressive that there are p, q:N for which
epsilon p k = 1 if k is the code of a proof of contradiction 0 if k is not such a code
epsilon q k = 0 for all k.
Then (All k. epsilon p k = epsilon q k)
is the statement of consistency of the logic, which is not decidable.
Hence this class has no extensional discriminating trace.
Any extensional trace therefore fails to be discriminating, ie
not All p q k. (epsilon p k = epsilon q k \/ delta p != delta q),
whence
not All p q k. not not (epsilon p k = epsilon q k \/ delta p != delta q)
not not Some p q k. not (epsilon p k = epsilon q k \/ delta p != delta q)
and
not not Some p q k. (epsilon p k != epsilon q k /\ delta p = delta q)
since equality on N is decidable.
By Markov's principle we may delete the "not not" to obtain a solution to the puzzle.
Your proof holds in constructive mathematics with Markov principle, but the question was, if I remember correctly, about Bishop's version where Markov's principle is no longer postulated
-----Original Message----- From: constructivenews@googlegroups.com [mailto:constructivenews@googlegroups.com] On Behalf Of Paul Taylor Sent: Saturday, June 11, 2011 8:15 AM To: constructivenews@googlegroups.com Subject: A puzzle
Martin Escardo and Andrej Bauer asked if one could prove that
For every h : (N --> N) --> N there exist f, g : N --> N and k : N such that h f = h g and f k != g k.
using constructive logic, ie without excluded middle or continuity principles.
Ulrich Berger had an interesting idea but I haven't managed to absorb it yet. The following is based on Vladek Kreinovich's comments.
However, since this is not my usual kind of mathematics and I have had other things on my mind recently (my 80-year old children formerly known as parents and a local political issue that you can see at www.monad.me.uk) so please would someone else check whether this is ok. If it's not then maybe someone can turn it into a correct proof.
===
In order to give an answer to the question it is not necessary to study the general function-space N-->N, whatever that may mean. It is sufficient to consider some class of total functions that is enumerated by a binary function
epsilon: N --> (N-->N) or epsilon: N x N --> N
I call the composite
delta = h.epsilon : N --> (N--> N) --> N
a TRACE.
If a function delta: N --> N arises in this way from some h:(N-->N)-->N then it is EXTENSIONAL in the sense that, for all p, q: N,
(All k. epsilon p k = epsilon q k) ==> delta p = delta q.
We also call such a function DISCRIMINATING if, for all p, q: N,
(Some k. epsilon p k != epsilon q k) ==> delta p != delta q.
Since equality on N is decidable, this is equivalent to, for all p, q: N,
(All k. epsilon p k = epsilon q k) <== delta p = delta q
and also to
All n p k. (epsilon p k = epsilon q k \/ delta p != delta q).
Therefore an extensional discriminating trace delta for the class that is enumerated by epsilon makes
(All k. epsilon p k = epsilon q k) <==> delta p = delta q
for all p, q :N.
Now suppose that this class of total functions is sufficiently expressive that there are p, q:N for which
epsilon p k = 1 if k is the code of a proof of contradiction 0 if k is not such a code
epsilon q k = 0 for all k.
Then (All k. epsilon p k = epsilon q k)
is the statement of consistency of the logic, which is not decidable.
Hence this class has no extensional discriminating trace.
Any extensional trace therefore fails to be discriminating, ie
not All p q k. (epsilon p k = epsilon q k \/ delta p != delta q),
whence
not All p q k. not not (epsilon p k = epsilon q k \/ delta p != delta q)
not not Some p q k. not (epsilon p k = epsilon q k \/ delta p != delta q)
and
not not Some p q k. (epsilon p k != epsilon q k /\ delta p = delta q)
since equality on N is decidable.
By Markov's principle we may delete the "not not" to obtain a solution to the puzzle.
> is the statement of consistency of the logic, which is not decidable.
> Hence this class has no extensional discriminating trace.
Here you implicitlly assumed that there are no non-computable functions, I think. So the proof probably covers a large class of models in which (externally) every map is computable.
I wasn't very sure about the application of Godel's theorem in my proof, but Vladik has told me privately that he thinks that it's ok.
On the other hand, his criticism about my use of Markov's principle would have been reasonable had someone else produced a definitive answer to Andrej's question, but they haven't. I just wanted to contribute to a group solution, as if we had been working face-to-face on the whiteboard in the common room in Ljubljana.
Andrej commented
>> Then >> (All k. epsilon p k = epsilon q k)
>> is the statement of consistency of the logic, which is not decidable.
>> Hence this class has no extensional discriminating trace.
> Here you implicitlly assumed that there are no non-computable > functions, I think. So the proof probably covers a large class of > models in which (externally) every map is computable.
I thought that it might be clearer to confine our attention to a smaller class of functions than N-->N, namely one that is enumerated but contains a proof tester.
The proof tester takes a number (code, input stream) and, like a referee, tests whether it is a valid (LaTeX document containing a) proof of inconsistency. This isn't about non-computable functions. It's old-fashioned recursion/proof theory.
My proof sort of says that any extensional trace function (N->N)->N has to assign the same trace to the proof tester as to the constantly zero function. This isn't quite right, because it could just jump in with what it magically knows to be a code for a proof of inconsistency.
So maybe the situation is that that result is valid under Markov's principle but not without it. Perhaps we could use Godel's theorem again to show the latter.
The idea is to use Joel Hamkin's infinite time Turing machine. These are powerful enough to compute canonical realizers for total realized maps. I hope I did not make any mistakes. Also, I am kind of trusting Joel that the s-m-n and u-t-m theorems holds for infinite time Turing machines. It would be nice to have an alternative description of the computational model that made the PCA structure more obvious.
