A puzzle

[Andrej Bauer]

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).

With kind regards,

Andrej

[Martin Escardo]

I believe there is no such Bishop-style constructive proof.

Regards,
Martin

[Fred Richman]

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

[Kreinovich, Vladik]

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: construc...@googlegroups.com [construc...@googlegroups.com] On Behalf Of Fred Richman [ric...@fau.edu]
Sent: Wednesday, June 01, 2011 12:15 PM
To: construc...@googlegroups.com
Subject: Re: A puzzle

[Fred Richman]

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.

--Fred

[Andrej Bauer]

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.

With kind regards,

Andrej

[Kreinovich, Vladik]

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: construc...@googlegroups.com [construc...@googlegroups.com] On Behalf Of Andrej Bauer [andrej...@andrej.com]
Sent: Thursday, June 02, 2011 7:07 AM

To: construc...@googlegroups.com
Subject: Re: A puzzle

In Russian constructivism/effective topos the proof is easy, since all

[Fred Richman]

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.

--Fred

[Toby Bartels]

Vladik:

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.

--Toby

[Ulrich Berger]

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.

[Martin Escardo]

I agree that non-injectivity sounds like a weakening of continuity,
Ulrich. Your topology-free, topological view of the situation is nice.
Martin

[Toby Bartels]

No answer, but some thoughts about context.

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.)

--Toby

[Martin Escardo]

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?

Best wishes,
Martin

[Robert Lubarsky]

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.

 

Bob

 

 

-----Original Message-----
From: construc...@googlegroups.com [mailto:construc...@googlegroups.com] On Behalf Of Andrej Bauer
Sent: Thursday, June 02, 2011 9:07 AM
To: construc...@googlegroups.com
Subject: Re: A puzzle

 

In Russian constructivism/effective topos the proof is easy, since all

[Andrej Bauer]

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.

With kind regards,

Andrej

[Toby Bartels]

Andrej Bauer wrote in part:

>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.)

--Toby

[Andrej Bauer]

>
>> 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.

We are back to topology.

With kind regards,

Andrej

[Fred Richman]

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?

--Fred

[Thomas Streicher]

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.

Thomas

[Thomas Streicher]

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?

[Paul Taylor]

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.

Paul

[Kreinovich, Vladik]

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

[Andrej Bauer]

> 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.

With kind regards,

Andrej

[Paul Taylor]

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

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.

Paul

[Andrej Bauer]

Dear all,

here is a first attempt at demonstrating that there is a realizability
topos in which there is an injection from N^N to N:

http://math.andrej.com/2011/06/15/constructive-gem-an-injection-from-baire-space-to-natural-numbers/

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.

With kind regards,

Andrej

[Martin Escardo]

Andrej,

I am looking forward to studying the details, but it looks convincing.

Just one non-technical correction. You say

"At the Mathematical Foundations of Programming Semantics XVII,
which took place at Carnegie Mellon University in May 2011, Paulo
Oliva and Martín Escardó showed[...]"

This was shown by Paulo alone, in his tutorial talk (also presented a
few weeks earlier at the Wessex Seminar in Swansea).

Best wishes,
Martin

[lubarsk...@comcast.net]

I think Andre's solution is right. Nicely done.

 

Andre, in your write-up I suggest you bring out more clearly how the integer m = r(x) is built, to make clear that it depends on x extensionally. The machine is running through ordinal time, looking for an m that builds the same function as x. When one is found, which will certainly happen, this will likely be at a limit stage. So there could well be many such m's found at that point. The machine will then have to make a canonical decision, presumably picking the least.

 

Bob

 

----- Oorspronkelijk bericht -----
Van: "Andrej Bauer" <andrej...@andrej.com>
Aan: construc...@googlegroups.com
Verzonden: Woensdag 15 juni 2011 15:50:34
Onderwerp: Re: A puzzle

[Andrej Bauer]

Thanks for the comments, I will incorporate them.

By the way, is there a sheaf topos in which N^Nembeds into N?

[Thomas Streicher]

Dear Andrej,

I have had a look at your countermodel which I find very convincing.
I have tried similar things but based on hyperarithmetic computability
which however hasn't lead to an end. Is there any characterization of
Hamkin computability in terms of the analytic hierarchy? It must be
quite
beyond hyperarithmetic (i.e. \Delta_1^1). Is it known where or can it
not
be characterized in such terms?

Best, Thomas

[Andrej Bauer]

If I remember correctly, the power of infinit time Turing machines
reaches into Delta^1_2, but don't take my word for it. It's somewhere
in the paper: http://arxiv.org/abs/math/0212047

With kind regards,

Andrej

[lubarsk...@comcast.net]

This was characterized by Phil Welch. There are three kinds of ITTM reals: writable, eventually writable, and accidentally writable. All three are the reals in some initial segment of L, resp. L_\lambda, L_\zeta, and L_\Sigma. L_\zeta is the least initial segment which has a \Sigma_2-elementary extension; L_\Sigma is that extension; L_\lambda is the smallest \Sigma_1 substructure of L_\zeta.

Bob

[Thomas Streicher]

Ok, this answers the question what are the total infinite time
computable functions. My question rather was what are the partial
infinite time computable functions on N. Can they be captured in terms
of some
relative notion of computability.

Thomas

[lubarsk...@comcast.net]

I assume that by "an ITTM computation that {e}(x) = m" is meant a halting computation -- in this context there are other possibilities. In that case, a partial function would be something that halts on some, perhaps not all, inputs. Those functions are eventually writable, meaning that eventually they will be completely written down, although the machine might not know to halt. To see that, given e, start computing, dovetailing {e}(x) for all x; whenever you see an output, write it down; eventually all halting computations will be done with; you have no way of knowing that, so you'll keep on computing, even though in fact nothing new will ever be generated. So you're written the graph of {e}, never to change, hence it's eventually writable, but you don't know to stop, hence not writable.

 

Bob

----- Oorspronkelijk bericht -----
Van: "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de>
Aan: "constructivenews" <construc...@googlegroups.com>
Verzonden: Donderdag 16 juni 2011 18:58:00
Onderwerp: Re: A puzzle

[lubarsk...@comcast.net]

> By the way, is there a sheaf topos in which N^Nembeds into N?

No. Consider the sheaves over a topological space T. Suppose you had such an embedding, h. The sheaf topos contains every function in N^N from Set. Fix x in T. For each f in N^N in set there is a neighborhood of x determining the value h(f). These values are all distinct for different f's. So this would give an embedding of N^N into N in Set.

 

Bob

[Alex Simpson]

By "sheaf topos" I think Andrej meant "Grothendieck topos".
That is, he was asking if there exists a Grothendieck
topos in which N^N embeds in N. Bob's argument for the special
case of sheaves over a topological space apparently doesn't
generalise to the general case.

Alex

--
Alex Simpson, LFCS, School of Informatics, Univ. of Edinburgh, UK
Email: Alex.S...@ed.ac.uk Tel: +44 (0)131 650 5113
Web: http://homepages.inf.ed.ac.uk/als Fax: +44 (0)131 651 1426

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Thomas Streicher]

Bob,

if I understand you correctly the notion of termination is problematic
in the sense that there are various possibilities. But Andrej in his
note was using one of them. He gives a pca structure on N
and I wonder whether this is induced by some realtive notion of
computablity, i.e. can be captured by an oracle.

I am asking this because I doubt it. I think pca's induced by relative
computability do not induce models
where N^N embeds into N. At least I had this problem when
experimenting with hyperarithmetic computability.

Best, Thomas

[lubarsk...@comcast.net]

I was cautious in my evaluation of Andrej's suggestion, and naturally went just for the point everyone would expect to be the weak spot: partiality, and/or undecidability of totality, or undecidability of equality of functions, some such thing. I made the most reasonable guess of what he means by {e}(x) = n, and it all seems to check out.

I'm not clear what your problem is, Thomas. ITTM computability is not Turing computability relative to an oracle. It is its own thing. Given two indices of total functions, it is decidable whether those functions are equal, and there is a canonical choice of representative index for such functions. What more would one need?

Bob

----- Original Message -----
From: "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de>
To: "constructivenews" <construc...@googlegroups.com>
Sent: Friday, June 17, 2011 1:53:28 PM
Subject: Re: A puzzle

[Andrej Bauer]

>I made the most reasonable guess of what he means by {e}(x) = n, and it all seems to check out.

No need to guess. I meant: machine e on input x terminates (reaches
the halting state at some ordinal step) with output n written on the
output tape. What else could I have meant?

I think Thomas is asking for some kind of description of partial
computable maps N -> N. For example, is there a notion of dominance so
that the partial computable maps are precisely those of the form N ->
N_\bot?

With kind regard,

Andrej

[lubarsk...@comcast.net]

> No need to guess. I meant: machine e on input x terminates (reaches
the halting state at some ordinal step) with output n written on the
output tape.

So I guessed right.

> What else could I have meant?

e eventually writes n, without necessarily halting. Or n is the lim inf of what e writes, even if the output keeps on changing. All less reasonable, but possible.

> I think Thomas is asking for some kind of description of partial
computable maps N -> N. For example, is there a notion of dominance so
that the partial computable maps are precisely those of the form N ->
N_\bot?

Assuming N_\bot is the discrete set N with \bot underneath all the numbers, then wouldn't the partial maps from N to N necessarily be the maps from N to N_\bot? As for a description with more content, they would be those functions \Sigma_1 definable over L_\lambda, which is the least \Sigma_1 elementary substructure of L_\zeta, which is the least set with a \Sigma_2 elementary extension. Not the easiest description to understand, I expect, but it does have the advantages of being both precise and correct. If you think in terms of hierarchies of reflection properties, then having longer and longer chains of \Sigma_n reflection for bigger n's is how the hierarchy is built up. That can help orient you as to where the property above fits.

Bob

[lubarsk...@comcast.net]

On a related note, Fred Richman asked me whether it is possible for every discrete set to embed into N. ITTM realizability satisfies that too, for much the same reason.

Bob


----- Original Message -----
From: "Andrej Bauer" <andrej...@andrej.com>
To: construc...@googlegroups.com
Sent: Friday, June 17, 2011 5:28:53 PM
Subject: Re: A puzzle

[Thomas Streicher]

> I'm not clear what your problem is, Thomas. ITTM computability is not Turing computability relative to an oracle. It is its own thing. Given two indices of total functions, it is decidable whether those functions are equal, and there is a canonical choice of representative index for such functions. What more would one need?

Thanks, Bob, that's a very simple and easy argument which simply
wasn't aware of. Clearly, for all
notions of relative computability extensional equality of Goedel
numbers of total functions is not decidable whereas in ITTM it is. BTW
is totality decidable, i.e. can we solve the halting problem in ITTM?
That's related to the question whether there is a dominance \Sigma in
the pca originating from ITTM. Though I was not think in these terms
orginally. Andrej has just been so kind to excuse the naivity of my
question.

Thomas

[Andrej Bauer]

> On a related note, Fred Richman asked me whether it is possible for every
> discrete set to embed into N. ITTM realizability satisfies that too, for
> much the same reason.

I thought the effective topos already satisfied that. A discrete set
is one whose equality is decidable. Such a set necessarily embeds into
N in the effective topos, I am pretty sure.

Regarding the ITTM model: what goes wrong with Paulo Oliva's programs
if we try to "run them in the ITTM model"?

With kind regards,

Andrej

[Thomas Streicher]

> Regarding the ITTM model: what goes wrong with Paulo Oliva's programs

> if we try to "run them in the ITTM model.

I think that Fan or Bar Theorem fail in this model since there will be
something
like the Kleene tree. However, it is not clear to me how to construct
one since
there doesn't seem to be an analogue of Kleene's T-predicate.

Thomas

[lubarsk...@comcast.net]

Hi,

 

The set of ITTM indices which halt is eventually writable; it is an example of the domain or range of a partial ITTM function.

 

What is a dominance in a pca?

 

Bob

 

----- Oorspronkelijk bericht -----
Van: "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de>
Aan: "constructivenews" <construc...@googlegroups.com>

Verzonden: Vrijdag 17 juni 2011 18:27:19
Onderwerp: Re: A puzzle

[lubarsk...@comcast.net]

Bar Induction holds. Given an in-out labeling of the nodes N^(<N) of the countably branching tree, it is ITTM computable to assign ordinal labels to those nodes correspondingly. If \bot gets an ordinal, that proves that instance of bar induction. If not, you can ITTM computably take the left-most path through the subtree of unlabeled nodes.

 

What are Paulo's programs, that we may check what part(s) of them fail(s) in this model?

 

As for discrete sets embedding into N, that could well have been known to hold in the effective topos; I'm just unaware of that. Is that really true though? I don't see it. Membership in a set A must be given by an integer. If the set is discrete, the same integer cannot witness membership of two objects in A. So if e witness "x in A" then x could be sent to e. That automatically gives a one-many relation from A to N. If you want to embed A into N, you'd need a function. Since several integers could witness "x in A," how do we pick out one? Taking the smallest is problematic, as there may be no algorithm to decide whether an integer d witnesses membership in A for something.

 

Would ITTM realizability be the first example of embedding all discrete sets into N and N^N being discrete?

 

Bob

 

----- Oorspronkelijk bericht -----
Van: "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de>
Aan: "constructivenews" <construc...@googlegroups.com>

Verzonden: Zaterdag 18 juni 2011 12:22:43
Onderwerp: Re: A puzzle

[Thomas Streicher]

> The set of ITTM indices which halt is eventually writable; it is an example of the domain or range of a partial ITTM function.

so we have a notion of r.e., i.e. semicomputable in modern language; I
guess what's
missing is a Kleene T-predicate which would be absurd anyway since
computations are
not finite and thus can't be coded by natural numbers

> What is a dominance in a pca?

It's given in

http://homepages.inf.ed.ac.uk/als/Research/uniform.ps.gz

in Def.4.1.
A DIVERGENCE in a pca A is a subset D of A such that
i) D is nonempty if A is total
ii) if a in D and ab \downarrow then ab in D.

Since Andrej's pca arising from ITTM is partial one may take D =
\emptyset.

It is shown in loc.cit. (on p.11) how a divergence D gives rise to a
dominance \Sigma.
The intuition behind a dominance is that it classifies emicomputable
predicates.

Thomas

[Andrej Bauer]

> so we have a notion of r.e., i.e. semicomputable in modern language; I
> guess what's missing is a Kleene T-predicate which would be absurd anyway since
> computations are not finite and thus can't be coded by natural numbers

Well, wouldn't the natural genralization of T-predicate be something a
relation T(n,m,a) where n is the machine code, n is the input, and a
is whatever it takes to describe a computation? So what does describe
a computation? A map from a countable ordinal to the Cantor space
could do it. The important thing is to make T decidable in the topos,
and as long as the type of a is overt, we'll be able to do the usual
things with the T predicate, no?

With kind regards,

Andrej

[Thomas Streicher]

> What are Paulo's programs, that we may check what part(s) of them fail(s) in this model?

The program is in Th 2 of Paulo's paper

Understanding and using Spector's bar recursive interpretation of
classical analysis
Paulo Oliva
[pdf] Proceedings of CiE'2006, LNCS 3988:423-434, Springer, 2006

available from his homepage. The point is that one can prove in
classical higher order
arithmetic that there is no injection from N^N to N. This can be given
a Dialectica
interpretation using bar recursion as shown by Spector.

Therefore I still doubt that ITTM validates bar recursion.

> As for discrete sets embedding into N, that could well have been known to hold in the effective topos; I'm just unaware of that. Is that really true though?

In Prop.3.2.32 of his book Jaap constructs a decidable modest set
which is not a subobject of N. Thus in Eff not all ecidable sets are
subobjects of N.

> Would ITTM realizability be the first example of embedding all discrete sets into N and N^N being discrete?

Sure, otherwise it wouldn't have needed Andrej's effort.

Thomas

[Thomas Streicher]

> Well, wouldn't the natural genralization of T-predicate be something a
> relation T(n,m,a) where n is the machine code, n is the input, and a
> is whatever it takes to describe a computation? So what does describe
> a computation? A map from a countable ordinal to the Cantor space
> could do it. The important thing is to make T decidable in the topos,
> and as long as the type of a is overt, we'll be able to do the usual
> things with the T predicate, no?

Interesting idea but I think it is important that computations are
coded by natural numbers as well. At least in relative computability
that is still the case.

Thomas

[lubarsk...@comcast.net]

Forget about coding ITTM computations with natural numbers. Such a computation is an infinitary object. The intuition that this is somehow like relative (Turing finite) computability is also misplaced.

 

A computation can be coded into a real. Just as with finitary computations, a computation is a succession of snapshots, which includes the state of the computer, the placement of the head, and the contents of the tapes. (Did I forget something? What else is in a computation?) The difference here is, the number of states is transfinite, and since there's enough time to visit the whole tape, its contents cannot be summarized by a finite integer; rather, you need an infinite amount of space for this. Any halting computation halts at a countable stage, so this is in the end countably many bits, which can be stored in a real.

 

Now here comes what code be a meaningful difference. The computation "a" referred to below contains finitely much information from each of finitely many stages. So one can imagine building "a" up from the bottom. For instance, computably biject N with NxN, at stage n put the state of the computation onto the n^th slice, and you're done. With ITTMs, this is not possible. You cannot know in advance how long the computation will take place. Given that e converges, you can write another machine which will write down the ordinal length that e takes, and then you can use that to slice N and write down a computation. This can even be done canonically: for instance, you can compute the L-least coding of such a computation.

 

Is this the info you need?

 

Bob

----- Oorspronkelijk bericht -----
Van: "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de>
Aan: "constructivenews" <construc...@googlegroups.com>

Verzonden: Zondag 19 juni 2011 00:25:37
Onderwerp: Re: A puzzle

[lubarsk...@comcast.net]

>> Would ITTM realizability be the first example of embedding all discrete sets into N and N^N being discrete?

> Sure, otherwise it wouldn't have needed Andrej's effort.

Well, I sure feel dumb!  :-o

 

Bob

[lubarsk...@comcast.net]

>> What are Paulo's programs, that we may check what part(s) of them fail(s) in this model?

>  The point is that one can prove in classical higher order arithmetic that there is no injection from N^N to N. This can be given a Dialectica interpretation using bar recursion as shown by Spector.

I don't yet understand the constructive interpretation of Paulo's theorem to be on firm ground here. What I have noticed is that he takes a type 2 functional, what we have been calling h:(N->N) ->N; defines f(k) = some function g with h(g) = k; diagonalizes to get d_f(k) = f(k)(k) + 1; and then observes that d and f(h(d)) differ at h(d) but h returns the same value on both of them. What doesn't fly about this in our context is that f is not total, so h(f) might be undefined. I understand that the classical principles that make his argument work in his context supposedly get Dialectica interpreted to something constructively true, so maybe this isn't a problem after all. It's what makes me suspicious, though. The use of classical logic right at the beginning also needs to be interpreted away.

> Therefore I still doubt that ITTM validates bar recursion.

 

Do we need bar recursion for more than decidable predicates? That's all that I claim to hold here.

 

 

>> Would ITTM realizability be the first example of embedding all discrete sets into N and N^N being discrete?

> Sure, otherwise it wouldn't have needed Andrej's effort.

To rescue my question, is this the first known case of all discrete sets embedding into N?

 

Bob

[Thomas Streicher]

Thanks for the explanations. I understand now why it is hopeless to
code computations
in ITTM by natural numbers. That brings to the point quite well how
different it is to
realtive computability.

Thomas

[Thomas Streicher]

There is no reference whatsoever to partial functions in Paulo's (and
relatd) work.
Moreover, you see seem to confound bar recursion and bar induction.
Paulo uses bar recursion to Dialectica interpret the negative
translations of instances of the comprehension scheme. Classical logic
and comprehension allow one to prove very easily that for every F : (N-
>N)->N there exist f,g:N->N with Ff = Fg but f(n) \not= g(n) for
some n. The programs he gets are obtained by unwinding this classical
proof. He needs
bar recursion to interpret the single use of comprehension.
So the model of E-HA_\omega arising from ITTM realizability cannot
validate bar recursion. In a sense this is no surprise since there are
only countably many functions from N to N and those don't suffice for
testing well-foundedness of trees.

Thomas

[lubarsk...@comcast.net]

I neglected to mention, when Andrej asked what could be meant by ITTM realizability other than via a halting computation on an integer input with integer output, take as the pca the set of pairs <natural number, real number>, with {<e,r>}(<f,s>) meaning "machine e with oracle r applied to the input <f,s>"; the output, if this halts, is what is on the output tape, which is a real, which can be taken to code such a pair. So ITTM computations can be thought of as from reals to reals. Which is how it's normally viewed.

 

Bob

[Martin Escardo]

Meanwhile I've asked Paulo to put his MFPS slides online with his recent
version of the proof of non-injectivity of functions (N->N)->N and the
extracted program. He did this this morning.

On 19/06/11 16:20, lubarsk...@comcast.net wrote:
> >> What are Paulo's programs, that we may check what part(s) of them
> fail(s) in this model?

Here they are

http://www.eecs.qmul.ac.uk/~pbo/away.html

in a slightly different way as the article Thomas mentions.

Martin

[Robert Lubarsky]

Hi all,

Earlier in the summer there was considerable discussion about
ITTM-realizability providing a model of an injection from N^N to N. People
were then wondering why Paulo Oliva's program providing a counter-example to
such an injection did not work in this model. The culprit seemed to be bar

recursion. For instance, Thomas Streicher wrote:

> So the model of E-HA_\omega arising from ITTM realizability cannot
validate bar recursion.

I doubted this publicly, going so far as to say that bar recursion worked
under ITTM realizability. After extended discussion with Paulo about his
program and about bar recursion more generally, I am convinced that the
discrepancy between Thomas's and my assertions was based on my ignorance of
how terminology is used. I assumed "bar recursion" is like "bar induction."
Since bar induction is "given a bar, and an inductive property true at the
bar, the property holds at <>," I assumed bar recursion would be "given a
bar, and values at the bar, and an inductive procedure going from values at
the children of a node to a value at the node, there is a unique value at
<>." That is not the case. If you write down stopping conditions of a
program on nodes, and an inductive procedure (from the children of a node to
the node), that's a bar recursive program, even if the stopping nodes do not
form a bar. Then "bar recursion" as a statement (after all, for bar
recursion to be validated or not, it must be a statement) is that any such
program produces a value at <>. Of course you wouldn't expect that to be
true all the time. As opposed to bar induction. For instance, classical set
theory validates BI and not BR.

As for just why ITTM realizability falsifies BR, I still disagree with
Thomas's next assertion:

> In a sense this is no surprise since there are only countably many
functions from N to N and those don't suffice for testing well-foundedness
of trees.

Yes, there are only countably many functions from N to N, in the sense that
there is an injection from N^N to N. Testing w-f of trees is a different
matter. The latter would be "given a tree as input, test whether it's w-f."
The tree would be given as an input. In fact, there is easily an ITTM
realizer to test for well-foundedness. So rather than an inability to test
for w-f causing BR to fail, I would say it's exactly the ability to test for
w-f that causes BR to fail. Whatever construction you would have to do
classically to get Paulo's program (for instance) to fail, you don't need
any more than ITTM computability to do that construction. Although I have
not stepped through this procedure myself, not even the classical
construction, this seems clear to me. How many steps would you need to build
this counter-example? \omega^\omega^\omega^\omega^\omega? If that's all you
need, an ITTM can do that with its eyes closed.

Since I don't like loose ends, I very much wanted to clear this matter up,
at least for myself. Are we now in agreement?

Bob

[Thomas Streicher]

Dear Bob,

my reason for concluding that the ITTM realizability model does not
validate
bar recursion was Theorem 2 of Paolo's paper in CiE'2006. I am glad
that we agree now on this.

> Yes, there are only countably many functions from N to N, in the sense that
> there is an injection from N^N to N. Testing w-f of trees is a different
> matter. The latter would be "given a tree as input, test whether it's w-f."
> The tree would be given as an input. In fact, there is easily an ITTM
> realizer to test for well-foundedness.

I thought of the internal statement of well-foundedness which is
different
from its external meaning since there might not be enough paths to
test.

> So rather than an inability to test
> for w-f causing BR to fail, I would say it's exactly the ability to test for
> w-f that causes BR to fail. Whatever construction you would have to do
> classically to get Paulo's program (for instance) to fail, you don't need
> any more than ITTM computability to do that construction. Although I have
> not stepped through this procedure myself, not even the classical
> construction, this seems clear to me. How many steps would you need to build
> this counter-example? \omega^\omega^\omega^\omega^\omega? If that's all you
> need, an ITTM can do that with its eyes closed.

I don't agree but possibly because I don't understand what you say.
I agree that classically BR fails because because of lack of well-
foundedness.
But classically some instances of BR hold like the one used by Paolo
in his program. I mean his program works in the standard set
theoretical model of HA_\omega.
But apparently Paolo's program fails in the ITTM model.

Whatever construction you would have to do
> classically to get Paulo's program (for instance) to fail, you don't need
> any more than ITTM computability to do that construction.

That's cryptic to me. Classically, Paolo's program works.

Best, Thomas

[Robert Lubarsky]

Hi Thomas,

> I thought of the internal statement of well-foundedness which is different
from its external meaning since there might not be enough paths to test.

I am also thinking of the internal statement. Nothing else would make much
sense. ITTMs don't check for well-foundedness by testing paths. Rather,
inductively nodes in the w-f part are thrown out, one at a time, until only
the ill-founded part is left. At that point it's easy to find a path, if
that's what you want.

> But classically some instances of BR hold like the one used by Paolo
in his program. I mean his program works in the standard set theoretical
model of HA_\omega. But apparently Paolo's program fails in the ITTM model.

> That's cryptic to me. Classically, Paolo's program works.

Why do you believe that? Even Paolo says his program doesn't work
classically.

Bob

[Thomas Streicher]

Hi Bob,

ok, you have a program checking whether in a tree there are no
infinite paths
that can be programmed in the sense of ITTM. Have you described it
somewhere?

> Why do you believe that? Even Paolo says his program doesn't work
> classically.

You are right. He applies bar recursion to the hypothetical function
\Psi and
there is no reason that it terminates in Set.

Thus BI is a classical principle whereas BR is not. BR entails BI but
not
vice versa.

Still I don't understand why you say

"it's exactly the ability to test for w-f that causes BR to
fail"

Because well-foundedness of the trees as employed in BR is not
automatic?

Thomas

[Martin Escardo]

Bar induction is a funny way of formulating structural induction on well
founded trees, by considering bars (which I find a bit unnatural, by the
way, but this is not what I want to emphasize here).

For the sake of illustration, let's consider a particular kind of trees
that arise often in this situation. You either have a leaf with a label,
a natural number n, denoted by L(n), or else given countably many trees
t_n you form a new tree B(t) with a new root and the given trees t as
the branches. These are the only two ways of constructing trees. To
prove that a property P holds for all such trees, you prove that P(L(n))
holds for every natural number n, and that if P(t_i) holds for a family
of trees t_i, then P(B(t)) holds. This is structural induction on trees,
and bar induction is a convoluted way of formulating this. And there is
no trouble in formulating structural recursion on such trees: f is
defined by structural recursion as

f(L(n)) = l(n)
f(B(t)) = b(i |-> f(t_i))

for given l and b of suitable types.

However, bar recursion *is not* structural recursion on such trees. What
it is is structural recursion on such trees *indirectly presented* as
continuous functions (N->N)->N. You can see the details of this, in more
generality, in Section 5.4 of the paper I wrote with Paulo,

http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf

As an exercise, I invite you to formulate the usual induction principle
on natural numbers using bars: In this case, the trees are boring,
because they are one-or-zero branching, and a bar is just a natural
number. What you get is Fermat's formulation of induction as "infinite
descent".

Coming back to Bob's and Thomas' discussion, I think the confusion may
arise by trying to see bar induction and recursion as counter-parts of
each other, which strictly they are not. Bar recursion requires a
non-classical assumption on the functions (N->N)->N. For Spector bar
recursion, the assumption can be majorizability. For modified bar
recursion, the assumption can be continuity. And so on. But in all
instances of bar recursion a non-classical assumption is needed. So Bob
is right, I think.

Martin

[Robert Lubarsky]

Hi,

> ok, you have a program checking whether in a tree there are no
infinite paths that can be programmed in the sense of ITTM. Have you
described it somewhere?

It's in the original ITTM paper by Hamkins & Lewis (JSL 2000 p. 567). Simply
put, given a tree coded as a set of pairs of integers (so it can be given as
input), recursively throw out points with no successors, until there's
nothing left to do.

> Still I don't understand why you say

> "it's exactly the ability to test for w-f that causes BR to
fail"

> Because well-foundedness of the trees as employed in BR is not automatic?

Yes. And an ITTM can separate out the w-f from the ill-founded parts and
construct a counter-example to BR, pretty much as you could in Set.

Bob

[Thomas Streicher]

Hi Bob,

> It's in the original ITTM paper by Hamkins & Lewis (JSL 2000 p. 567). Simply
> put, given a tree coded as a set of pairs of integers (so it can be given as
> input), recursively throw out points with no successors, until there's
> nothing left to do.

thanks for the pointer

> > Because well-foundedness of the trees as employed in BR is not automatic?
>
> Yes. And an ITTM can separate out the w-f from the ill-founded parts and
> construct a counter-example to BR, pretty much as you could in Set.

ok, now I see what you meant
we do agree now; one can have BI without BR as pointed out by Martin
Escardo; the terminological situation is somewhat awkward because BR
is more than transfinite induction over well-founded trees

Thomas

[Robert Lubarsky]

> the terminological situation is somewhat awkward because BR
is more than transfinite induction over well-founded trees

I find "bar recursion" to be a horrible name for what is being named. The
recursion involved has very little to do with bars.

Bob

[Thomas Streicher]

> I find "bar recursion" to be a horrible name for what is being named. The
> recursion involved has very little to do with bars.

well, it is recursion over well founded trees + the requirement that
certain predicates always describe bars like in continuous functionals
or hereditary majorizable functionals

Thomas

[Robert Lubarsky]

> well, it is recursion over well founded trees + the requirement that
> certain predicates always describe bars like in continuous functionals
> or hereditary majorizable functionals

Not at all. If the trees were w-f then bar recursion would hold in Set. And
the majorizable functionals don't give bars. It's recursion over full trees
with a stopping condition, and the stopping condition might not be on a bar.

Bob

[Thomas Streicher]

> Not at all. If the trees were w-f then bar recursion would hold in Set. And
> the majorizable functionals don't give bars. It's recursion over full trees
> with a stopping condition, and the stopping condition might not be on a bar.

since the stopping condition is given by a majorizable functional it
does define a bar

thomas

[Thomas Streicher]

In Lemma 2.2 of the respective article of Bezem (on p. 655 of JSL 50)
you find a very simple proof that
the stopping condition gives rise to a bar. Later on heavy use of bar
induction is made in the argument.

The reason why bar recursion doesn't hold in the ITTM model is that
type 2 functional don't give rise to bars.

Thomas

PS BTW does it hold in the ITTM model that internally well-founded
trees are inductive, i.e. well-founded externally?

[Robert Lubarsky]

Since this discussion is getting technical, and since at this point nobody
but Thomas and I are participating in this, I think I will be doing everyone
a favor by taking this offline and talking with Thomas one-on-one. If I have
misread the situation, and there is great demand for us to hash this out in
public, or some individual(s) want to be kept in the loop, I will be happy
to do so, by request.

Bob