König's Lemma

[Ryan Hayes]

Has anybody attempted to prove König's Lemma in UF?

As a refresh, König's Lemma states that if a binary tree T has countably infinite nodes (each of finite degree) then there exists an infinite-lengthed path in T. It's a classic "comprehension" -esque theorem in mathematical logic.

Vladimir has emphasized the classicalness (?) of UF and so while I realize this theorem isn't provable in typical MLTT; I think it (or a slightly weakened version) should be provable in UF. I believe it's simply an equivalence to Nat (the 'nerve' of the tree from root through said infinite path).

Just as a slight postscript, it's not that I can't figure out how to prove this theorem it's simply that I am interested in what people think about "whether it should be provable". I came across it while reading about the Löwenheim-Skolem-Tarski 'paradox' (which it's loosely related à la compactness) and so it is related to there being some (kinda weird prob no isomorphic to "normal" model(s)) finite model of UF. (I am aware Löwenheim-Skolem doesn't hold for constructive logics in general but obv UF isn't strictly; it has a richer semantics).

Thanks in advance for any general comments/insights,

Ryan

[Ryan Hayes]

And it's probably obvious but by path I mean "branch"; in current implemented type systems I think this would be somewhat difficult to prove without defining a sort of ur-infinite-binary-tree which; again, I am really interested in what people think. It just seems "morally" quite similar to path induction but it's a bit different since we might have to use an "unfolded" definition.

I guess ancillary question would be are type formers distinguished. If we definite a type family over an infinite structure (like Nat) to another (finite type former like succ for N but potentially infinite) *should* (double emphasis on *should*—deontological question! ... I know current answer is 'not really') that be allowed to "freely generate" a structure too? If not it makes me wonder why succ : Nat -> Nat is admissible. (If S is a function then proving an isomorphism to N means we are pattern matching/recursing on N (or an implicit infinite quantification/jump)... Is matching an open term extensional? succ : takes a simple form but what if we had a type former like: Q : (n : N) -> Prime n -> T for some type T obviously (as is the case with N and Z) we can treat the "open object" T without actually generating a bunch of primes. If we try to make the system excessively "operationally constructive" one can imagine "operational paradoxes" quantifying over known a known exponential time algorithm in a type former with some massive term that would cause some locality issues (surely there are giant terms whose type formers are tiny like the Ackerman function) ... Anyway that's very wishy washy and really just an arm chair musing.

In short if we can prove an isomorphism from Z to S1 with "open terms like loop : base == base" then could we do the same for \n > Vec Ackerman ( n+n , succ n * (Ackerman n + 5 n + 99) )?

Sorry for all the random musings. Just a lot of "which level?" thoughts.

[Ryan Hayes]

And sorry to post on my own post twice but the idea of quantifying over an open term ('freely generating' --- really freely denoting --- an infinite structure) is basically equivalent to König's lemma so it stands to reason that we should be able to prove it. :-) that was my point. stated rather tortuously I admit.

[Thomas Streicher]

In assemblies over the first Kleene algebra one may construct the
groupoid model which validates UA but number realizability refutes the
Fan principle of intuitionistic mathematics (the contrapositive of
Koenig's lemma).

Thomas

[Ryan Hayes]

That's a rather weak system, no? Weaker by far than CZF. I believe it's equivalent to LL parsers, basically. There have been claims that UF subsumes set theory. I am trying to reconcile this. Granted you mention just one model. What else isn't provable in such an interpretation? And that's without Universes right? So UA is rather useless in that setting...?

[Ryan Hayes]

Equivalent in strength to the decision problem over regulars expressions.* I can't imagine higher inductive types in such a setting. Or some facts about natural numbers (as you stated).

[Ryan Hayes]

For example I don't believe you could define the prime counting function in the model you state since (I believe) Kleene Algebra are equivalent to ELEMENTARY, a few ticks away from computable functions.

[Andrej Bauer]

There are Kleene algebras, Kleene algebras, the first Kleene algebra,
and the second Kleene algebra, and they are completely different
things:

http://en.wikipedia.org/wiki/Kleene_algebra
http://ncatlab.org/nlab/show/Kleene's+second+algebra
http://ncatlab.org/nlab/show/partial+combinatory+algebra (see
"Examples" section)

Thomas is talking about partial combinatory algebras, obviously, since
he is referring to realizability models. Let me bit more explicit than
Thomas:

König's Lemma is not provable in UF, unless we additionally assume
some form of excluded middle (which is not part of UF proper).

So please check the definitions. I do not know what you understand by
"Vladimir has emphasized the classicalness", maybe the fact that the
intended model has a strong classical component. In any case, UF is
*not* classical, it is *compatible* with classical mathematics. I'd
recommend reading the discussions about excluded middle in the HoTT
book.

With kind regards,

Andrej

[Michael Shulman]

Do we know a countermodel with infinitely many univalent universes?

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Andrej Bauer]

On Wed, Aug 13, 2014 at 4:57 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> Do we know a countermodel with infinitely many univalent universes?

No. You'd need to beef up Thomas's suggestion to higher dimensions,
i.e., we need "higher-dimensional" realizability over Kleene's first
algebra.

[Ryan Hayes]

Andrej, I thought I made it pretty clear this wasn't a dumb claim. People have literally claimed UF subsumed set theory. I suppose that's what I meant. I was echoing this rather sketchy claim rather facetiously. Vladimir has said that LEM shouldn't really be considered "bad" as such (per normal constructive wont). Will elaborate more when I am not up for 27 hours. :-)

See : http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

[Bas Spitters]

It should be easy to make a sheaf counter model for Koning's Lemma, as
it is very non-constructive.

For the counter model to the fan theorem, the constructive
contrapositive, we'd like to use a realizability model along the lines
that Thomas suggested, this should be like the work by Wouter
Steckelenburg.
http://arxiv.org/abs/1406.6579
(I see he put up a new version recently).

On Wed, Aug 13, 2014 at 4:57 PM, Michael Shulman <shu...@sandiego.edu> wrote:

[Michael Shulman]

On Wed, Aug 13, 2014 at 8:14 AM, Ryan Hayes <rygui...@gmail.com> wrote:
> See : http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

Andrej wrote there that

> In Univalent foundations we *may* assume excluded middle for (−1)-types and we *may* assume the axiom of choice for 0-types.

If you're talking about UF *with* such assumptions (which are
perfectly *compatible* with it, but which we don't usually include by
default when saying "UF"), then of course you can prove Konig's lemma
in the usual way.

[Michael Shulman]

On Wed, Aug 13, 2014 at 8:17 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> It should be easy to make a sheaf counter model for Koning's Lemma, as
> it is very non-constructive.

Yes -- but what about if we want a model with true univalent universes
(not just weakly Tarski ones)? Does Konig's lemma fail in any of
those models that we know so far (which I think are still limited to
elegant Reedy presheaves)?

> For the counter model to the fan theorem, the constructive
> contrapositive, we'd like to use a realizability model along the lines
> that Thomas suggested,

Are you saying that the fan theorem holds in all sheaf models?

> this should be like the work by Wouter
> Steckelenburg.
> http://arxiv.org/abs/1406.6579
> (I see he put up a new version recently).

Has anyone looked at the new version yet?

[Andrej Bauer]

On Wed, Aug 13, 2014 at 5:14 PM, Ryan Hayes <rygui...@gmail.com> wrote:
> Andrej, I thought I made it pretty clear this wasn't a dumb claim.

I never thought it was a dumb claim, I just wanted to make it clear
that (a) you misunderstood what Thomas wrote because there are many
things called "Kleene algebra" and (b) it seems pretty clear that
König's lemma is not provable in UF.

> People have literally claimed UF subsumed set theory.

When you say "Univalent foundations" the vast majority of people will
take it to mean "The HoTT book". If you are referring to something
other than that you have to say so. If you are referring to something
someone might have said, please provide a reference and be precise
about the mathematical content.

> See : http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

This is a reference, of course. I wrote it. I was careful not to say
anywhere that UF validates excluded middle. I said things like "we may
assume excluded middle for (−1)-types" and "Any mathematics that is
formalized using Univalent foundations is compatible with classical
mathematics". I responded to you in the same way, by relativizing with
respect to excluded middle:

"König's Lemma is not provable in UF, unless we additionally assume
some form of excluded middle (which is not part of UF proper)."

So I think it's pretty clear that "UF" does not include "excluded
middle" in any shape of form. If you assume it, you have to say so
explicitly. And if you do, then obviously König's lemma becomes
provable. If you don't, then Thomas's remark shows that it's not
provable with one univalent universe. I very very much doubt anything
could change if you got more univalent universes, since König's lemma
happens entirely in h-sets.

Good night :-)

Andrej

[Michael Shulman]

On Wed, Aug 13, 2014 at 8:25 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> I very very much doubt anything
> could change if you got more univalent universes, since König's lemma
> happens entirely in h-sets.

I agree, of course.

I wonder whether there could be any metatheorem of this sort? Is it
possible that more univalent universes could allow us to prove
*anything* new about h-sets?

[Thomas Streicher]

> I wonder whether there could be any metatheorem of this sort? Is it
> possible that more univalent universes could allow us to prove
> *anything* new about h-sets?

In type theory with n+1 universes you can prove consistency of type
theory with n universes, i.e. a new \Pi^0_1 sentence.

Thomas

[Michael Shulman]

But how about just the assumption that the extra universes are
univalent? The groupoid model does have plenty of universes, it's
just that they aren't univalent after the first one.

[Thomas Streicher]

> But how about just the assumption that the extra universes are
> univalent? The groupoid model does have plenty of universes, it's
> just that they aren't univalent after the first one.

That's indeed a problem unless Stekelenburg succeeds with his
construction of models in categories of assemblies.

But you are asking whether the assumption of univalence for universes
(already assumed to exist) is conservative. Good question but I have
no idea how one could show it.

Thomas

[Bas Spitters]

Konig's lemma is equivalent to LLPO.
http://onlinelibrary.wiley.com/doi/10.1002/malq.19900360307/abstract

I am not sure whether there is a Kripke/presheaf counter model to this.

> Are you saying that the fan theorem holds in all sheaf models?

I was just saying that the usual counterexample uses realizability.

There is an example in Fourman and Hyland - sheaf models for analysis Thm 4.4.
Sheaves over the K( I x I ) |= ~ fan
K(X) is the collection of coperfect opens and I the unit interval.

[François Dorais]

On Thu, Aug 14, 2014 at 2:46 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:

Konig's lemma is equivalent to LLPO.
http://onlinelibrary.wiley.com/doi/10.1002/malq.19900360307/abstract

Not quite. Following Bishop, Ishihara assumes countable choice which has several side effects. Without any nontrivial choice assumptions, LLPO is much weaker than (both the weak and strong) König Lemma. However, it is true WKL is equivalent to countably many instances of LLPO. (Basically, you need one instance of LLPO to decide each bit of the branch through an infinite decidable subtree of the full binary tree.)

[Bas Spitters]

Thanks, yes of course.
In fact, König Lemma implies DC in suitable frameworks.

[Vladimir Voevodsky]

If I am not mistaken, one can construct in the theory with n+1 universe a term t of type nat -> bool and then proof, in the meta-theory, that if t is equal (propositionally) to a term which can be defined in the theory with n universes than the theory with n universes is inconsistent.

V.

[Thomas Streicher]

> If I am not mistaken, one can construct in the theory with n+1 universe a term t of type nat -> bool and then proof, in the meta-theory, that if t is equal (propositionally) to a term which can be defined in the theory with n universes than the theory with n universes is inconsistent.

I don't think so because the point is that there is a primitive
recursive function definition f for which type theory with n+1
universes proves (\Pi n:N) Id_N(f(n),0) but type theory with n
universes doesn't. Of course f is the function with f(k) = 0 if the
k-th derivation (in type theory with n universes) does prove False and
f(k) = 1 otherwise. In type theory with n+1 universes one easily
proves that f(k) = 0 for all k since one can show that no derivation
in type theory with n universes proves False.

However, if type theory with n+1 universes proves strong normalisation
for type theory with n universes then the interpreter for function of
type N->N can be programmed in the type theory with n+1 universes. By
the usual recursion theoretic argument this interpreter cannot be
formulated in type theory with n universes.

But if we have a type theory where not all closed terms of type N
reduce to a numeral we cannot use this style of argument. Alas, HoTT
could be of this kind since we don't know whether every closed term of
type N reduces to a numeral.

Thomas

[Vladimir Voevodsky]

Thomas, I did not understand from your message whether you agree or disagree with my comment.

V.

[Vladimir Voevodsky]

Here is a sketch of the proof of this claim. It does not depend on the strength of the theory (once it is high enough) or on normalization or on canonicity. It is directly based on Goedel's proof of the first incompleteness theorem.

1. One constructs a function enum : nat− > ( nat− > bool ) in the theory with n+1-universe such that for any term X of type nat− > bool in the theory with n-universes, or more precisely, for any valid judgement of the form (⊢ X : nat− > bool) in this theory, one can, using the concrete syntax of X, find a natural number n(X) such that enum(n(X)) is definitionally equal to X.

Actually building such an enumeration function may be difficult but should be possible. After all there are only countably many term of type nat -> bool in the empty context in the theory with n-universes.

2. Consider the term (fun n : nat => not (enum n n)) where "not" is the Boolean "not". It is of type nat −> bool. Let us assume that it can be defined in the theory with n universes. Then there exists m : nat such that enum(m) ≡ (fun n : nat => not (enum n n)). Then

enum m m ≡ (fun n : nat => not (enum n n ) ) m ≡ not (enum m m )

and we conclude that the theory with n universes is inconsistent.

Vladimir.











On Aug 16, 2014, at 9:40 AM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:

> On Sat, Aug 16, 2014 at 09:27:51AM +0800, Vladimir Voevodsky wrote:
>> Thomas, I did not understand from your message whether you agree or disagree with my comment.
>

> I disagrre with your comment in case there is no normalization reult
> for the type theory which allows one to show that all closed terms of
> type N reduce to a numeral.
>
> More generally, stronger theories need not allow one to define more
> more number theoetic functions. Let T be PA and T' = T + Con_T. Then T
> and T' have the same provably recursive functions. Actually, if you
> add to PA and set of true \Pi^0_1 sentences this stronger theory
> doesn't allow one to define more number theoretic functions (as can be
> seen by modified realizability).
>
> The reason is that \Pi^0_1 sentences have no computational
> significance.
>
> Thomas

[Thomas Streicher]

I fully agree with you when having an enum (that's what I called an
"interpreter" for number theoretic functions). But I don't see from
where you get such an enum in the first place without proving
that every term is provably equivalent to a unique numeral.

Thomas

On Sat, Aug 16, 2014 at 10:08:09AM +0800, Vladimir Voevodsky wrote:
> Here is a sketch of the proof of this claim. It does not depend on the strength of the theory (once it is high enough) or on normalization or on canonicity. It is directly based on Goedel's proof of the first incompleteness theorem.
>

> 1. One constructs a function enum : nat??? > ( nat??? > bool ) in the theory with n+1-universe such that for any term X of type nat??? > bool in the theory with n-universes, or more precisely, for any valid judgement of the form (??? X : nat??? > bool) in this theory, one can, using the concrete syntax of X, find a natural number n(X) such that enum(n(X)) is definitionally equal to X.

>
> Actually building such an enumeration function may be difficult but should be possible. After all there are only countably many term of type nat -> bool in the empty context in the theory with n-universes.
>

> 2. Consider the term (fun n : nat => not (enum n n)) where "not" is the Boolean "not". It is of type nat ???> bool. Let us assume that it can be defined in the theory with n universes. Then there exists m : nat such that enum(m) ??? (fun n : nat => not (enum n n)). Then
>
> enum m m ??? (fun n : nat => not (enum n n ) ) m ??? not (enum m m )

[Vladimir Voevodsky]

I am not even sure what it has to do with values of type nat being numerals. The enum enumerates terms of type (nat -> bool).

V.

[Thomas Streicher]

> >> Here is a sketch of the proof of this claim. It does not depend on the strength of the theory (once it is high enough) or on normalization or on canonicity. It is directly based on Goedel's proof of the first incompleteness theorem.
> >>
> >> 1. One constructs a function enum : nat??? > ( nat??? > bool ) in the theory with n+1-universe such that for any term X of type nat??? > bool in the theory with n-universes, or more precisely, for any valid judgement of the form (??? X : nat??? > bool) in this theory, one can, using the concrete syntax of X, find a natural number n(X) such that enum(n(X)) is definitionally equal to X.
> >>
> >> Actually building such an enumeration function may be difficult but should be possible. After all there are only countably many term of type nat -> bool in the empty context in the theory with n-universes.

One can always find a primitive recursive function

enum : nat -> Tm_n(nat -> bool)

enumerating the closed terms of type nat -> bool in the system with n
universes

but I don't see how to get an interpreter

int : Tm(nat -> bool) -> nat -> bool

Thomas

PS Do you agree that stronger systems need not be able to define more
functions? My argument is that PA and PA + Con_PA have teh same set of
provably recursive functions.

[maxim....@googlemail.com]

//...there are only countably many term of type nat -> bool in the empty context in the theory with n-universes. 

Why the terms of types nat -> bool  may be enumerated? 

 Function enum looks like surjection: nat->2^nat...

Thanks.

Max.

[andré hirschowitz]

Hello,

2014-08-17 16:10 GMT+02:00 <maxim....@googlemail.com>:

//...there are only countably many term of type nat -> bool in the empty context in the theory with n-universes. 

Why the terms of types nat -> bool  may be enumerated? 

 Function enum looks like surjection: nat->2^nat...

(Since noone answered, I tried to, and I hope it helps).

This is a well-known (apparent) paradox.

As you know  it can be proven that no function f: nat->(nat -> bool) is  surjective. Nevertheless, the set of terms of type nat-> bool is countable (think for instance that they are represented by some kind of strings, or trees).

If I understand correctly the previous message, it could (probably) be possible to define a type Tm( nat-> bool) representing the set of terms of type nat-> bool, and a surjective (in some sense)

enum : nat -> Tm(nat-> bool)

but it seems more difficult to define

interp : Tm(nat-> bool) ->(nat ->bool).

Anyway, this one  could not be proven surjective (hopefully).

ah

[Vladimir Voevodsky]

There has been and is a lot of discussion of this issue - how to build an interpreter internally. Since we do not require univalence the usual induction-recursion in the ambient (with n+1 universes) theory may be sufficient.

V.

[Vladimir Voevodsky]

On Aug 18, 2014, at 6:43 AM, andré hirschowitz <a...@unice.fr> wrote:

interp : Tm(nat-> bool) ->(nat ->bool).

Anyway, this one  could not be proven surjective (hopefully).

One should be able to prove, in meta-theory, that this function is surjective on objects. (E.g. a function empty -> T is surjective on objects if T is not inhabited). 

V.

[Vladimir Voevodsky]

On Aug 18, 2014, at 6:43 AM, andré hirschowitz <a...@unice.fr> wrote:

interp : Tm(nat-> bool) ->(nat ->bool).

Anyway, this one  could not be proven surjective (hopefully).

[maxim....@googlemail.com]

Then appears question about consistency of this meta-theory.

 In "weak" form it is notenum.

 I.e. There are proofs of notenum in the meta-theory?

Thanks  

Max

[Thomas Streicher]

> There has been and is a lot of discussion of this issue - how to build an interpreter internally. Since we do not require univalence the usual induction-recursion in the ambient (with n+1 universes) theory may be sufficient.

If we dont have univalence I agree because then every closed term of
type Nat reduces to a numeral and we can build in the theory with n+1
universes an interpreter for closed terms of type Nat of the theory
with n universes.

Thomas

[Vladimir Voevodsky]

I do not understand. We are talking about terms of type nat -> bool . What does it have to do with terms of type nat ?

V.

[Thomas Streicher]

I agree with Andre since there is a surjection from nat to Tm(nat -> bool)
wghich would give rise to a surjection from nat to nat -> bool. But
this cannot exist due to Cantor's diagonal argument which holds
constructively and predicatively.

Thomas

[Thomas Streicher]

On Mon, Aug 18, 2014 at 05:20:44PM +0800, Vladimir Voevodsky wrote:
> I do not understand. We are talking about terms of type nat -> bool . What does it have to do with terms of type nat ?

the question is whether we can program in the theory with n+1 universes
an interpreter for the closed terms of type nat -> bool in the theory
with n universes
for this purpose the natural thing to do is the following: given a
term t of type nat -> bool and a natural number n normalize t num(n)
which gives a closed normal form of type bool which can be translated
to a boolean value iff there is no chunk, i.e. evert=y closed normal
form of type bool is either true or false

in case n=1 and the presence of the uninterpreted constant ua of type UA
this is not possible anymore

Thomas

[maxim....@googlemail.com]

//...cannot exist due to Cantor's diagonal argument which holds 
constructively and predicatively. 

 Allow me to disagree. 

I think opposite: Cantor's diagonal arguments are impredicative and non-constructive because they are based on existence of the actual infinity. Actual infinity impredicative by origin and thus is an application of the diagonal arguments-"diagonal axiom".

[Thomas Streicher]

> //...cannot exist due to Cantor's diagonal argument which holds
> constructively and predicatively.
>
> Allow me to disagree.

Suppose there is a surjective map e : N -> N^N. Let f : N -> N with
f(n) = e(n)(n) + 1. If there were an n with e(n) = f then e(n)(n) =
f(n) = e(n)(n) + 1. Contradiction!

Well, I have used extensionality for functions from N to N. But
otherwise it's constructive and in any case it is predicative.

If we have powerset available as in topos logic we can show that
there is no surjective e : X -> P(X). Let S = { x:X | \neg x \in e(x) }.
Let x in X with e(x) = S. Then x \in e(x) iff x \in S iff \neg x \in e(x).
Contradiction!

Thomas

PS A nice paper on this is http://arxiv.org/abs/math/0305282

[andré hirschowitz]

2014-08-18 20:47 GMT+02:00 Thomas Streicher <stre...@mathematik.tu-darmstadt.de>:

> //...cannot exist due to Cantor's diagonal argument which holds
> constructively and predicatively.
>
>  Allow me to disagree.

Suppose there is a surjective map  e : N -> N^N. Let f : N -> N with
f(n) = e(n)(n) + 1. If there were an n with e(n) = f then e(n)(n) =
f(n) = e(n)(n) + 1. Contradiction!

 

 I do not see where this invokes extensionality...

ah

[maxim....@googlemail.com]

Thanks for link.

//  Suppose there is a surjective map  e : N -> N^N. Let f : N -> N with 

f(n) = e(n)(n) + 1. If there were an n with e(n) = f then e(n)(n) = 
f(n) = e(n)(n) + 1. Contradiction! 

Well, I have used extensionality for functions from N to N. But 

otherwise it's constructive and in any case it is predicative....//

Impredicativity appear at extensionality:

 //...Let f : N -> N with 

f(n) = e(n)(n) + 1.

when

f(m)=f(m)+1; m:e(m)=f

this is unbounded recursion(in order to define function value).. 

possible resolution: f(m)=oo.

Diagonal arguments based on assumption about actual infinity i.e. impredicativity(diagonal arguments)

Max

[Andrej Bauer]

On Tue, Aug 19, 2014 at 5:26 AM, <maxim....@googlemail.com> wrote:
> Diagonal arguments based on assumption about actual infinity i.e.
> impredicativity(diagonal arguments)

It is false that diagonal arguments have anything to do with infinity
or impredicativity. The basic form of the diagonal argument was
identified by Lawvere with his fixed point theorem. It works in any
cartesian-closed category. It can be formulated in predicative set
theory as well. It assumes almost nothing, and certainly not any kind
of infinity.

However, to get interesting *applications* of Lawvere's theorem we
typically need to assume the existence of N or some such. But this is
irrelevant: the basic argument of Lawvere's works without any such
assumptions.

For a concise proof of Lawvere's theorem see e.g.
http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/ but
do not take that as a proper reference.

Furthermore, I would suggest that HoTT list is not the proper forum to
clear up basic misconceptions about Cantor's diagonal argument.

With kind regards,

Andrej

[Thomas Streicher]

> > Suppose there is a surjective map e : N -> N^N. Let f : N -> N with
> > f(n) = e(n)(n) + 1. If there were an n with e(n) = f then e(n)(n) =
> > f(n) = e(n)(n) + 1. Contradiction!
> >
> >
> >
> I do not see where this invokes extensionality...

You are right I was "overly cautious".

If we don't have extensionality then the argument even shosws that
there cannot be a function e : N -> N^N such that for every f \in N^N
theer exists a n \in N with e(n)(m) = f(m) for all m \in N.

Thomas

[Vladimir Voevodsky]

I do not understand the question then. There *is* a construction of enum in the meta-theory.

Also, there *is* a construction of enum for the type theory with n universes in the type theory with n+1-universes if the type theory with n+1-universes is sophisticated enough. But this, unlike the case of classical meta-theory, is hard to do and probably have never been properly done in the case when the theory with n-universes is the Martin-Lof Type theory.

Vladimir.

PS I mean enum: nat -> ( bool -> nat ) such that for any closed term of type nat -> bool there exists a numeral n such that enum(n) is definitionally equal to this term.



On Aug 21, 2014, at 12:24 AM, Максим Будаев <maxim....@googlemail.com> wrote:

> 2014-08-18 15:09 GMT+06:00, Vladimir Voevodsky <vlad...@ias.edu>:
>> What is notenum?
>>
>> V.
>>
>
> I read just now. Sorry
>
> notenum is a negation of enum,
> proposition : there is no function enum : nat− > ( nat− > bool )...
>
> Max

[maxim....@googlemail.com]

//...There *is* a construction of enum in the meta-theory

Then  in the meta-theory  there is value for any enum n m including enum n n such that enum n n = not (enum n n ) In syntax point of view, this is impredicative definition for enum n n and thus unbounded recursion. For complete construction the meta-theory must resolve any impredicative definitions in the theory by means of infinity type, 

  but why this is consistent?

  Are there proofs of noenum(There is no enum; better than notenum) in the meta-theory?

   Sophisticated proofs, based on infinity types existence ... 

Max

[Bas Spitters]

Douglas Bridges points out that the Kripke model on p138 of Varieties
of constructive mathematics is a counter model for LPO, and in fact
for LLPO. The model is:
0
/ \
P1 1
/ \
P2 2
etc.
This is a direct poset and hence fits Mike's strict model.

On Thu, Aug 14, 2014 at 8:46 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> Konig's lemma is equivalent to LLPO.
> http://onlinelibrary.wiley.com/doi/10.1002/malq.19900360307/abstract
>
> I am not sure whether there is a Kripke/presheaf counter model to this.
>
>> Are you saying that the fan theorem holds in all sheaf models?
> I was just saying that the usual counterexample uses realizability.
>
> There is an example in Fourman and Hyland - sheaf models for analysis Thm 4.4.
> Sheaves over the K( I x I ) |= ~ fan
> K(X) is the collection of coperfect opens and I the unit interval.
>
> On Wed, Aug 13, 2014 at 5:23 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>> On Wed, Aug 13, 2014 at 8:17 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
>>> It should be easy to make a sheaf counter model for Koning's Lemma, as
>>> it is very non-constructive.
>>
>> Yes -- but what about if we want a model with true univalent universes
>> (not just weakly Tarski ones)? Does Konig's lemma fail in any of
>> those models that we know so far (which I think are still limited to
>> elegant Reedy presheaves)?
>>
>>> For the counter model to the fan theorem, the constructive
>>> contrapositive, we'd like to use a realizability model along the lines
>>> that Thomas suggested,
>>
>> Are you saying that the fan theorem holds in all sheaf models?
>>
>>> this should be like the work by Wouter
>>> Steckelenburg.
>>> http://arxiv.org/abs/1406.6579
>>> (I see he put up a new version recently).
>>
>> Has anyone looked at the new version yet?

[Michael Shulman]

On Fri, Aug 22, 2014 at 8:52 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> Douglas Bridges points out that the Kripke model on p138 of Varieties
> of constructive mathematics is a counter model for LPO, and in fact
> for LLPO. The model is:
> 0
> / \
> P1 1
> / \
> P2 2
> etc.
> This is a direct poset and hence fits Mike's strict model.

Just had a chance to look this up. I wasn't sure from your
description whether their Kripke models were covariant or
contravariant functors and what direction the arrows go in the
displayed graph, but now that I read it looks like they are covariant
and the arrows go down. That makes it (as you say) a direct poset,
whereas my strict models are for inverse posets, the opposites of
direct ones. Am I misunderstanding?

Mike

[Bas Spitters]

I am afraid you are right indeed.

The inequalities point up, hence the arrows down.
Bridges and Richman indeed use covariant Kripke models.
Hence, this is a diagram over a direct poset, but a presheaf over an
inverse poset.

So, the question whether there is a strict model seems still open.

[Andrew Swan]

It might be possible to show LLPO fails using the cubical set model. If "internal" LLPO in the cubical set model implies "external" LLPO, then one can just construct the cubical set model in a background universe where LLPO fails to get a countermodel.

[Michael Shulman]

On Thu, Aug 28, 2014 at 6:02 AM, Andrew Swan <wakeli...@gmail.com> wrote:
> It might be possible to show LLPO fails using the cubical set model. If
> "internal" LLPO in the cubical set model implies "external" LLPO, then one
> can just construct the cubical set model in a background universe where LLPO
> fails to get a countermodel.

Hmm, so if we construct the cubical set model internally to a topos,
then how are the hsets in the cubical model related to the original
topos? It seems offhand like they should be some kind of ex/lex
completion of it. Of course, N and 2 and 2^N in the cubical model
will be "the same" as those of the original topos (i.e. they will be
discrete cubical sets), but it seems like the image factorization will
be different; so the internal and external versions are probably not
identical. One of them might still imply the other, though...

[Andrew Swan]

I'm not sure if I follow where image factorization comes in. What formulation of LLPO are you using? Is it formulated using disjoint sum or mere disjunction?

[Michael Shulman]

Any formulation of LLPO involves existential quantification and
disjunction, both of which involve image factorization if you use
their hprop versions. I was assuming we wanted the hprop versions,
although admit I haven't thought deeply about it; now that I look, I
see that the book mentions the untruncated version of LPO. Which
version of LLPO is related to Konig's Lemma? Are there corresponding
multiple versions of Konig's lemma? I think of Konig's lemma as a
choice-like property, which suggests that it should be truncated.

[Bas Spitters]

The hprop version should be the most natural interpretation.
And we should expect to obtain both (truncated) LLPO and a version of
(truncated) DC.

[Martin Escardo]

I can answer these questions, and in fact I have already answered them
both in this list and in the constructivenews list:

* The truncated versions of LPO and WLPO agree with their
non-truncated versions.

* The non-truncated version of LLPO (using Sigma rather than exists)
is actually equivalent to WLPO.

* A model by Michael Rathjen (he told me that after I posted the
above), separates WLPO from LLPO.

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Michael Shulman]

On Thu, Aug 28, 2014 at 1:56 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> * The truncated versions of LPO and WLPO agree with their
> non-truncated versions.

Ah, this perhaps has to do with Exercise 3.19 in the book?

[Martin Escardo]

Yes, it does. I will forward two messages to you (I can't find links on
the web)@ one question by Andrej and an answer by me. Then you (Mike),
made this in to portions of the book, which then were eventually demoted
to exercises.

Martin

[Martin Escardo]

On 28/08/14 21:56, Martin Escardo wrote:
>
> I can answer these questions, and in fact I have already answered them
> both in this list and in the constructivenews list:
>
> * The truncated versions of LPO and WLPO agree with their
> non-truncated versions.

I addressed this already.

> * The non-truncated version of LLPO (using Sigma rather than exists)
> is actually equivalent to WLPO.

This was only announced in the constructivenews list (in connection
with the discussion that if all functions (N->N)->N are continuous
with the Sigma formulation of continuity, then 0=1), but I can provide
a proof on request.

Nevertheless, this is an interesting exercise. Moreover, it is one of
the nice examples where Sigma and exists make a huge difference.

> * A model by Michael Rathjen (he told me that after I posted the
> above), separates WLPO from LLPO.

This is here:

http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf

Martin

[Andrew Swan]

Okay, that makes things clearer.

Looking at Ishihara's paper that Bas Spitters linked to ( http://onlinelibrary.wiley.com/doi/10.1002/malq.19900360307/abstract ), König's lemma implies the following form of LLPO:

for all binary sequences f : N -> 2, if f(i) = 1 for at most one i then either f(2i) = 0 for every i, or f(2i + 1) = 0 for every i

This also follows from the form of LLPO formulated with hProp and assuming (a weak form of) countable choice the converse also holds. It's fairly easy to find models of intuitionist set theory where this form of LLPO fails (using realizability, for example).

I claim that if this form of LLPO holds internally in the cubical set model, then it also holds externally. I think a proof along the following lines should work. Let f : N -> 2 be a binary sequence such that f(i) = 1 for at most one i. Then we can also view f as a section of 2^N in the cubical set model in the obvious way. By working internally in cubical set model, it should be possible to show that there exists a section of the cubical set inh((forall i, f(2i)=0) + (forall i, f(2i + 1) = 0)). Hence, there also exists a section of the cubical set ((forall i, f(2i)=0) + (forall i, f(2i + 1)=0)). Hence (externally) either for all i f(2i) = 0 or for all i f(2i + 1) = 0.

> email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Michael Shulman]

That makes sense. More generally, I guess that "there merely exists" in a setoidy/exact-completion model is a *stronger* statement than "there merely exists" externally, in fact it seems about the same as "there purely exists" externally.

Of course, although the cubical model has true univalent universes, it's not-quite-strict in a different way, right?

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Martin Escardo]

On 28/08/14 21:56, Martin Escardo wrote:

> * The truncated versions of LPO and WLPO agree with their
> non-truncated versions.
>
> * The non-truncated version of LLPO (using Sigma rather than exists)
> is actually equivalent to WLPO.
>
> * A model by Michael Rathjen (he told me that after I posted the
> above), separates WLPO from LLPO.

Here is what is going on with WLPO versus LLPO, from the point of view
of continuity.

First let's consider WLPO. It says that every binary sequence is
constantly 0 or not.

Theorem. WLPO is equivalent to the existence of a non-continuous
function N_\infty->N.

This is perhaps not obvious.
(http://www.cs.bham.ac.uk/~mhe/papers/wlpo-and-continuity-revised.pdf)

What is N_\infty? Intuitively, it is N (the natural numbers) with an
added limit point at infinity. Abstractly, N_\infty is the final
coalgebra of the functor 1+(-). Concretely, there are a number of
options. Two favourite ones are (1) the set of decreasing binary
sequences, (2) the set of binary sequences that have at most one 1.
They are isomorphic sets (and hence equivalence types).

Theorem. It is decidable whether a function N_infty->N is
not-continuous.

(That is, every such function is not-continuous or
not-not-continuous. If you have MP (Markov principle), every such
function is continuous or not, but I will not assume MP.)

Theorem. If not-WLPO, then all functions N_\infty->N are
not-not-continuous. If additionally MP holds, then all such functions
are continuous.

Thus, WLPO (possibly interacting with MP) is the boundary of
(non-)continuity in mathematics.

That's why WLPO is an interesting (undecided) proposition. It is the
negation of continuity (expressed positively).

Question. Is there a nice univalent model of MLTT that falsifies WLPO?
(And hence validates the not-not-continuity of all functions
N_\infty->N.) More ambitiously, is there a univalent model of MLTT
that validates the continuity of all functions N_\infty->N?

Now LLPO's turn.

LLPO says that for every binary sequence that has at most one 1,
either the even terms are all 0, or the odd terms are all 0.

Now it does matter what we mean by "A or B" : the truncated version
||A+B|| or the non-truncated version A+B.

Let's assume that we take the concrete implementation (2) of N_infty
described above (the binary sequences with at most one 1).

Then infinity, written \infty, is the constantly zero sequence.

The number n is coded by the sequence that is 1 at position n and 0
everywhere else.

Now consider the functions evens,odds:N_\infty->N_\infty that take even
and odd terms. What do they do?

evens(2n)=n
evens(2n+1)=\infty
evens(\infty)=\infty

odds(2n)=\infty
odds(2n+1)=n
odds(\infty)=\infty

Both of them are (of course) continuous.

Then LLPO says, with this language,

For every x:N_\infty, evens(x)=\infty or odds(x)=\infty.

We can't infer that || evens(x)=\infty + odds(x)=\infty || ->
evens(x)=\infty + odds(x)=\infty.

The reason is that the propositions evens(x)=\infty and odds(x)=\infty
are not mutually incompatible. In fact, for x=\infty, both hold.

Hence there is no apparent way of getting WLPO from this.

Now consider LLPO':

For every x:N_\infty, evens(x)=\infty + odds(x)=\infty.

I claim that what I explain above gives you a way to derive WLPO from
LLPO'. In fact, because of the use of non-truncated _+_, we get a
non-continuous function N_\infty->2, and hence WLPO.

(There are short-cut ways of obtaining the same conclusion. I wanted
to emphasize the connection with (non-)continuity.)

Martin

> On Thu, Aug 28, 2014 at 2:55 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>>
>>
>> On 28/08/14 21:56, Martin Escardo wrote:
>>>

>>> I can answer these questions, and in fact I have already answered them
>>> both in this list and in the constructivenews list:
>>>
>>> * The truncated versions of LPO and WLPO agree with their
>>> non-truncated versions.
>>

>> I addressed this already.

>>
>>> * The non-truncated version of LLPO (using Sigma rather than exists)
>>> is actually equivalent to WLPO.
>>

>> This was only announced in the constructivenews list (in connection
>> with the discussion that if all functions (N->N)->N are continuous
>> with the Sigma formulation of continuity, then 0=1), but I can provide
>> a proof on request.
>>
>> Nevertheless, this is an interesting exercise. Moreover, it is one of
>> the nice examples where Sigma and exists make a huge difference.
>>

>>> * A model by Michael Rathjen (he told me that after I posted the
>>> above), separates WLPO from LLPO.
>>

>> This is here:
>>
>> http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf
>>
>> Martin
>>
>>