¬¬WLPO

[Martin Escardo]

What is known about ¬¬WLPO compared to the other constructive taboos or
Brouwerian counter-examples?

WLPO says that every binary sequence is constantly 1 or it isn't.

(So ¬¬WLPO is the double negation of a universally quantified formula.)

I am not assuming countable choice (or negating it).

I don't think WLPO follows from ¬¬WLPO, but I don't have an argument.

But in most, if not all, varieties of constrictive mathematics we have
that ¬WLPO is consistent, and hence ¬¬WLPO is not provable.

How does ¬¬WLPO compare to the known, canonical taboos?

Thanks,
Martin

[frank waaldijk]

dear Martin,

to be frank i don't much understand why the relative logical strength of all sorts of non-constructive principles seems to get more attention than the underlying constructive mathematical world.

There is one overriding principle in uncountable constructive math: continuity.

WLPO asserts the possibility of making a discontinuous choice on Cantor space, and is therefore obviously false. Provably false in intuitionistic mathematics, making ¬WLPO true in INT.

Therefore, in INT, WLPO follows from ¬¬WLPO (if you're looking for an argument).

In general, it is not possible to go from ¬¬(A V ¬A) to A V ¬A (even if A = ¬B) and I would be very surprised if you will find another argument than the one I just gave for INT.

Hopefully this helps,
cheers Frank

[frank waaldijk]

oh sorry, these double negation questions always confuse me!

you asked somewhat the opposite of what I answered :-)

anyway, to give you a better answer, perhaps it might be possible to construct some model of INT and some subspace of Cantor space, where notnotWLPO holds but where WLPO is still daring.

[frank waaldijk]

my first idea would be to construct subspaces M(alpha) indexed by alpha in Cantor space.

depending on the infinite behavior of alpha, sometimes we might see notnotWLPO hold for M(alpha), sometimes not, mostly unclear, but we might derive an intuitionistic continuity contradiction from the statement that for all alpha: in M(alpha) notnot WLPO implies WLPO.

so again (if the question would enthuse me, which to be frank it doesn't) I would turn to topology to see if I could find an answer there.

perhaps already one M(alpha) might suffice, to give a Brouwerian counterexample.

sorry again for misreading your question,
cheers Frank

[Thomas Streicher]

In both number and function realizability WLPO is not realizable and
for this reason the negation of WLPO is realizable.
Generally in such models A is realizable iff its double negation is
realizable.

But Bob Lubarsky might have constructed some sophisticated topological
countermodels...

Thomas

[Andrew Swan]

To separate \neg \neg WLPO from WLPO, use the realizability with truth model like in Rathjen, The disjunction and other properties for Constructive Zermelo-Fraenkel Set theory, but (unlike in that paper) assume classical logic in the background theory. Then since negated formulas are absolute, the double negation of any classically true statement (including WLPO) holds in the model. However, WLPO itself fails for the usual reasons. If I recall correctly, the topos theory way to do this is to glue along the inclusion from Set into the effective topos.

\neg \neg WLPO seems pretty weak to me and I can't think of any use for it offhand. I suppose if anyone knows of any consequences of WLPO that are stable under double negation, then they would be an example of a nontrivial consequence of \neg\neg WLPO.

Best,

Andrew

[Thomas Streicher]

> If I recall correctly, the topos theory way to do
> this is to glue along the inclusion from Set into the effective topos.

Yes, that's it!

Very cute argument BTW!

Thomas

[Robert Lubarsky]

In the JSL paper I referenced in my earlier reply, there is such a topological model. To make it easy on you all: Let U be a nonprincipal ultrafilter on the natural numbers. Let X be the union of the natural numbers omega and {∗, infinity}. Topologize X by letting the basic open sets be ∅, {k} (k ∈ omega), {infinity}, and sets of the form {∗, infinity} ∪ u for u ∈ U.

Regarding Frank's suggestion, the topological model over Cantor space satisfies WLPO but not LPO. So it does do something of interest around the principles in question, just not what Martin was looking for.

Bob

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

[Martin Escardo]

Thanks for all the answers and discussion.

In 2012, I constructed an example of a set X with two points x0 and x1
such that if there is a function p:X->2 with p(x0)=0 and p(x1)=1 then
WLPO holds. This is was in response to a colleague's conjecture that in
MLTT, any two different points could be separated by a function into the
booleans, 2.

Recently I've have been led to consider totally separated sets, that is,
sets Y such that, for any two given points x and y, if p(x)=p(y) for all
functions p:Y->2, then x=y.

A quick calculation shows that if the the above 2012 set X is totally
separated, then ¬¬WLPO holds.

As discussed in this thread, this is a bit weak. In particular, in
dependent type theory, which is the framework I am considering, we can
postulate ¬¬WLPO without loss of computational content, because any
consistent negative axiom can be postulated without loss of canonicity.
So ¬¬WLPO is one of these principles like Markov principle, which have
computational interpretations but perhaps are not very compelling
constructively. In particular, ¬¬WLPO, as emphasized by others
contradicts continuity principles. (And ¬WLPO is equivalent to a
continuity principle.)

Best,
Martin

[frank waaldijk]

dear Bob, you write

Regarding Frank's suggestion, the topological model over Cantor space satisfies WLPO but not LPO. So it does do  something of interest around the principles in question, just not what Martin  was looking for.

I could be wrong but I offer the following simple argument (following the suggestion I  gave earlier):

For alpha in Cantor space let M(alpha) be the model based on the one-point set {alpha}. We see that notnotWLPO holds for M(alpha)...(check for yourself). So if notnotWLPO would imply WLPO, then WLPO would hold for M(alpha). Since alpha is the only element, that implies that alpha either equals the zero sequence 0, or does not equal 0. So we obtain WLPO for Cantor space, which contradicts intuitionistic mathematics, which is equiconsistent with classical mathematics. So unless classical mathematics is inconsistent, notnotWLPO does not imply WLPO.

Cheers, Frank

 

 

[Andrej Bauer]

> So unless classical mathematics is inconsistent, notnotWLPO does not imply WLPO.

If classical mathematics is inconsistent, then also ¬¬WLPO does not
imply WLPO (in addition to many other theorems holding).

Thus, since classical mathematics is either is consistent or
inconsistent (it's classical after all), ¬¬WLPO does not imply WLPO.

With kind regards,

Andrej

[frank waaldijk]

That makes me laugh, good to have some humor in these things :-) thanx Andrej!

[Robert Lubarsky]

I do not know what “the model based on the one-point set {alpha}” means. I am not suggesting that it is meaningless, far from it, just that I have absolutely no clue what Frank is talking about. It is certainly not the topological model (= Grothendieck topos = forcing), as that is built with open sets and not with individual points.

 

Bob

--

[frank waaldijk]

Thanks for your interest Bob,

and you are right that I was rather sketchy. I will explain in more detail below. (And it is conceivable that my argument is incorrect, since I did not ckeck and check again, which is why I said "I could be wrong".)

.

What I meant was a first-order model, in the language of equality. The most direct approach is to use the language of FIM (Kleene&Vesley1965), which is a two-sorted language with variables for natural numbers and variables for elements of Baire space.  

In FIM-language we can express things like 'forall beta [ forall n [beta(n)=0] V NOT forall n [beta(n)=0]]' which is WLPO.

Now for alpha in Cantor space, take M(alpha) to be the model formed by the one-point set {alpha} and the language of FIM. We see that notnotWLPO holds in M(alpha), and the rest is like I stated earlier (hopefully). 

(If it works at all,) I think the argument also works in the simpler first-order language of just equality, using intuitionistic model theory (see e.g. Some elementary results in intuitionistic model theory [JSL, Veldman&Waaldijk1996].). Then it is better to use the sets {0, alpha} as models M(alpha). We need to see that for Cantor space WLPO implies WLPO+ : forall beta forall gamma [beta = gamma V beta /= gamma], which we can obtain considering that for any beta in Cantor space, there is a homeomorphism sending 0 to beta. Then in M(alpha) we see that notnotWLPO+ holds, and if notnotWLPO+ would imply WLPO+ then we get a contradiction with intuitionistic continuity.

I hope that is enough elucidation. You wrote:

I do not know what “the model based on the one-point set {alpha}” means. I am not suggesting that it is meaningless, far from it, just that I have absolutely no clue what Frank is talking about. It is certainly not the topological model (= Grothendieck topos = forcing), as that is built with open sets and not with individual points.

Now, to be a bit pesky which comes naturally to me (sorry...), let me say that I also have absolutely no clue what you were talking about earlier...! When you wrote:

In the JSL paper I referenced in my earlier reply, there is such a topological model. To make it easy on you all: Let U be a nonprincipal ultrafilter on the natural numbers. Let X be the union of the natural numbers omega and {∗, infinity}. Topologize X by letting the basic open sets be ∅, {k} (k ∈ omega), {infinity}, and sets of the form {∗, infinity} ∪ u for u ∈ U. 

Regarding Frank's suggestion, the topological model over Cantor space satisfies WLPO but not LPO. So it does do  something of interest around the principles in question, just not what Martin  was looking for. 

I mean that I really have no idea what a non-principal ultrafilter on the natural numbers looks like. And what is 'the topological model over Cantor space' in say intuitionistic mathematics? I know a perfectly fine intuitionistic topological model of Cantor space (Cantor space itself) in which like I said notWLPO is a theorem, so you must mean a different topological model. But is this model predicatively built, and does it function in accordance with intuitionistic logic? If you know of a readable account in which is it shown that these constructions are truly acceptable intuitionistically (by which I mean predicatively built and not essentially relying on classical assumptions somewhere in the fine print), please let me know. 

So I repeat my position once again (to the exasperation of some, I fear): constructive mathematics needs a solid, unified platform which is built predicatively and using only intuitionistic logic, much more than it needs the investigation of the relative strength of various non-constructive principles.

Friendly greetings,

Frank

[Berger U.]

Dear Frank,

How can there be a model with one real (= element of Baire space) only? Aren't constant 0 and constant 1 different reals which exist in every model?
Maybe I'm missing something.

Thanks!

Ulrich
________________________________________
From: construc...@googlegroups.com [construc...@googlegroups.com] on behalf of frank waaldijk [fwaa...@gmail.com]
Sent: 02 February 2018 09:59
To: constructivenews
Subject: Re: ¬¬WLPO

Thanks for your interest Bob,

and you are right that I was rather sketchy. I will explain in more detail below. (And it is conceivable that my argument is incorrect, since I did not ckeck and check again, which is why I said "I could be wrong".)
.
What I meant was a first-order model, in the language of equality. The most direct approach is to use the language of FIM (Kleene&Vesley1965), which is a two-sorted language with variables for natural numbers and variables for elements of Baire space.

In FIM-language we can express things like 'forall beta [ forall n [beta(n)=0] V NOT forall n [beta(n)=0]]' which is WLPO.

Now for alpha in Cantor space, take M(alpha) to be the model formed by the one-point set {alpha} and the language of FIM. We see that notnotWLPO holds in M(alpha), and the rest is like I stated earlier (hopefully).

(If it works at all,) I think the argument also works in the simpler first-order language of just equality, using intuitionistic model theory (see e.g. Some elementary results in intuitionistic model theory<https://www.fwaaldijk.nl/intuitionistic-model-theory.pdf> [JSL, Veldman&Waaldijk1996].). Then it is better to use the sets {0, alpha} as models M(alpha). We need to see that for Cantor space WLPO implies WLPO+ : forall beta forall gamma [beta = gamma V beta /= gamma], which we can obtain considering that for any beta in Cantor space, there is a homeomorphism sending 0 to beta. Then in M(alpha) we see that notnotWLPO+ holds, and if notnotWLPO+ would imply WLPO+ then we get a contradiction with intuitionistic continuity.

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com<mailto:constructivene...@googlegroups.com>.

[Robert Lubarsky]

Hi all,

 

> What I meant was a first-order model, in the language of equality. The most direct approach is to use the language of FIM (Kleene&Vesley1965), which is a two-sorted language with variables for natural numbers and variables for elements of Baire space.  Now for alpha in Cantor space, take M(alpha) to be the model formed by the one-point set {alpha} and the language of FIM. We see that notnotWLPO holds in M(alpha), and the rest is like I stated earlier (hopefully). 

 

I gather that M(alpha) is to contain for the first-order part the natural numbers and the second-order part contains alpha and everything that can be proven in FIM to exist. As to what is true in this model, that depends on the meta-theory. In a classical meta-theory, classical logic is true. No doubt if WLPO is true in the meta-theory, it was also still hold in this model. I do not see that this approach does anything.

 

> Now, to be a bit pesky which comes naturally to me (sorry...), let me say that I also have absolutely no clue what you were talking about earlier...!

 

Just to be clear, I don’t find this pesky at all. Questions are always welcome.

 

> I mean that I really have no idea what a non-principal ultrafilter on the natural numbers looks like. And what is 'the topological model over Cantor space' in say intuitionistic mathematics? I know a perfectly fine intuitionistic topological model of Cantor space (Cantor space itself) in which like I said notWLPO is a theorem, so you must mean a different topological model. But is this model predicatively built, and does it function in accordance with intuitionistic logic? If you know of a readable account in which is it shown that these constructions are truly acceptable intuitionistically (by which I mean predicatively built and not essentially relying on classical assumptions somewhere in the fine print), please let me know. 

 

Just to make life easy for me, I work in ZFC. I’m not smart enough to do constructive mathematics. For a constructive, predicative formulation, I would recommend Gambino’s “Heyting-valued interpretations for CST”, APAL v. 137 (2006), p. 164-188. I do not claim that the existence of an ultrafilter as above is provable constructively and predicatively.

 

Bob

 

[Giovanni Sambin]

2018-02-02 10:59 GMT+01:00 frank waaldijk <fwaa...@gmail.com>:

So I repeat my position once again (to the exasperation of some, I fear): constructive mathematics needs a solid, unified platform which is built predicatively and using only intuitionistic logic, much more than it needs the investigation of the relative strength of various non-constructive principles.

Dear Frank, 

perhaps to your exasperation I repeat my answer: the Minimalist Foundation (by Milly Maietti and myself) is what you look for! It is surely predicative and intuitionistic. Moreover, it can also keep control of AC and AC!. It is unified, in the sense that all other common foundations can be seen as extensions. What we still miss is (only???) a proper expository introduction. Chapter 2 of the book I am writing contains an introduction to the extensional level. Milly is writing many technical papers. Both of us plan to write something about it together next summer.

All the best

Giovanni

[Martin Escardo]

On 02/02/18 09:59, frank waaldijk wrote:
> So I repeat my position once again (to the exasperation of some, I
> fear): constructive mathematics needs a solid, unified platform which is
> built predicatively and using only intuitionistic logic, much more than
> it needs the investigation of the relative strength of various
> non-constructive principles.

I feel that since you have affirmed this twice, perhaps you are
demanding (1) an apology or (2) an explanation. (I will refrain from
writing (a) smilies or (b) frownies, which you will have to
reconstruct.)

Perhaps it is better to give both. (I mean (1) and (2), to clarify.)

I choose to start with (2), so that then (1) can be taken as an
apology for both starting this thread with such an outrageous question
about ¬¬WLPO and then for defending it with (2), too. Here we go.

(2): I think I understand ¬WLPO: it says precisely that every function
ℕ∞→ℕ is continuous in a weak sense (the ε-δ sense, but with doubly
negated existential quantifiers), where ℕ∞ is the set of decreasing
binary sequences.

So ¬WLPO is a weak Brouwerian continuity axiom.

It is remarkable that (without Brouwerian, Markovian or
countable-choice principles), not only the equivalence of ¬WLPO with a
continuity axiom holds, but also for any given function ℕ∞→ℕ you can
decide its weak continuity in this sense. Any such function is
continuous or it isn't.

The set ℕ∞ itself satisfies the principle of omniscience: for every
function p:ℕ∞→𝟚 into the two-point set 𝟚={0,1}, the statement
∃(x:X),p(x)=0 is decidable - the function p either has a root or it
doesn't. Again this is the case in a spartan constructive setting,
which could be called "agnostic mathematics".

I am interested in agnostic mathematics. In particular, I want to know
which sets, in addition to ℕ∞, satisfy the principle of omniscience in
agnostic mathematics. Or how much of excluded middle "just holds".

Moreover, I want to understand exactly how the (weak) omniscience of ℕ
fails. Or its double negation. In particular, I want to dispel the
naive thought that ℕ fails to be (weakly) omniscient just because it
is infinite. The set ℕ∞ is even larger, and so "more infinite", but it
it satisfies the principle of omniscience. And this has *nothing* to
do with continuity (continuity axioms are not asserted or denied in
order to prove this). The failure of the omniscience of ℕ must
therefore be rather subtle, going beyond the mere fact that ℕ is
infinite. Omniscience problems may start with infinite sets, but it is
not infinity alone that gives them.

So I really want to *understand* the connections between the so-called
"taboos", LPO, WLPO, LLPO, ¬¬WLPO, and *cotaboos* such as continuity
axiom, Fan theorem, and Bar induction. The last taboo, ¬¬WLPO, is the
"worst" in a sense, because it is in the boundary of constructive and
classical mathematics: it holds classically, it doesn't hold in
agnostic mathematics, but it does have a computational interpretation,
and it does contradict Brouwerian continuity axioms.

(1): My sincere apologies! :-) And I lied about the smilies. Please go
back to (1) for a further apology.

Best,
Martin

[Martin Escardo]

On 02/02/18 21:29, Martin Escardo wrote:
> The last taboo, ¬¬WLPO, is the
> "worst" in a sense, because it is in the boundary of constructive and
> classical mathematics: it holds classically, it doesn't hold in
> agnostic mathematics, but it does have a computational interpretation,
> and it does contradict Brouwerian continuity axioms.

It is clearly a rogue axiom, if we are in need of terminology for such
things.

M.

[frank waaldijk]

That is a wonderful answer, Martín.

It really helps me understand your question much much better, thank you for taking the time to explain this to me.

It is of course I who should apologize, but it is nice of you to suggest otherwise. Still: my apologies for overemphasizing a point that was not the most salient one to make.

I do hope that my suggestions regarding the models M(alpha) are helpful to you, in your endeavor to understand notnotWLPO in realtion to agnostic mathematics. They were certainly meant to be helpful, in the sense that as far as I can tell, these are very basic, stripped models which yet exhibit all the necessary elements to distinguish notnotWLPO from WLPO.

Maybe I will respond to Ulrich's question in private, somewhere this weekend, and maybe on rereading your answer I will have something more to say, but for now I'm done (it being late on a Friday night and all...).

Thanks again, Martín,

best wishes, Frank

[Martin Escardo]

Thanks for the discussion, Frank. Good night! Martin

> --
> You received this message because you are subscribed to the Google
> Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to constructivene...@googlegroups.com

> <mailto:constructivene...@googlegroups.com>.

[Andrew Swan]

On Fri, 6 Apr 2018 at 23:14 Martín Hötzel Escardó <m.es...@cs.bham.ac.uk> wrote:

One use of ¬¬WLPO is to show that the function space (Noo->N) is not
countable, where Noo is the set of decreasing binary sequences.

But it is (always) discrete (as already discussed in the other thread).

Because ¬¬WLPO has a constructive interpretation, there is a variety of
constructive mathematics with an uncountable discrete set/

We can see ¬WLPO as a (very weak) continuity axiom. So ¬¬WLPO negates
continuity, which makes (Noo->N) uncountable.

Nice!

 

Regarding the "Non-separable normed spaces" thread, the arxiv paper by
Andrej and Andrew seems to say something about "neutral mathematics"
(mathematics with classical principles removed, but no anticlassical,
potentially-constructive principles added).

Or is it saying more than that?

 

Our result is for anything that holds in the function realizabiltiy topos. This includes typical intuitionist axioms such as continuous choice, LCN, fan theorem, bar induction etc. So the principle "all functions are continuous" is an anticlassical axiom that holds there.

Of course, since the result is that a certain statement is not provable, it also applies to any weaker theory.

By the way, for Russian constructivism, Church's thesis implies that the complement of the halting set is an example of an uncountable discrete set.

Best,

Andrew

[Martin Escardo]

On 07/04/18 00:46, Andrew Swan wrote:
> By the way, for Russian constructivism, Church's thesis implies that the
> complement of the halting set is an example of an uncountable discrete set.

Ah, yes, interesting, too.

Martin

[Martin Escardo]

In connection with the new thread "Non-separable normed spaces", and in
particular Andrej and Andrew's message of 3rd April, and this:

On 27/01/18 19:33, Andrew Swan wrote:
> \neg \neg WLPO seems pretty weak to me and I can't think of any use
for it offhand. I suppose if anyone knows of any consequences of WLPO
that are stable under double negation, then they would be an example of
a nontrivial consequence of \neg\neg WLPO.

One use of ¬¬WLPO is to show that the function space (Noo->N) is not
countable, where Noo is the set of decreasing binary sequences.

But it is (always) discrete (as already discussed in the other thread).

Because ¬¬WLPO has a constructive interpretation, there is a variety of

constructive mathematics with an uncountable discrete set, among other
places.

We can see ¬WLPO as a (very weak) continuity axiom. So ¬¬WLPO negates
continuity, which makes (Noo->N) uncountable.

Regarding the "Non-separable normed spaces" thread, the arxiv paper by
Andrej and Andrew seems to say something about "neutral mathematics"
(mathematics with classical principles removed, but no anticlassical,

potentially-constructive principles added, or semi-constructive,
classically compatible axioms, added, such as ¬¬WLPO).

Or is it saying more than that?

Martin