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