co-taboos

[Martin Escardo]

Peter Aczel introduced the terminology "taboo" to explain a certain
practice in constructive mathematics, corresponding to Brouwerian
counter-examples.

I argue that co-taboos also occur (but they deserve a better name).

Immerse yourself in a form of constructive mathematics that is
compatible with classical mathematics and also with any other known
form of constructive mathematics.

For example, Bishop mathematics, if we had a precise definition of
what that is, would probably fit the bill.

We could call this "minimal mathematics", "absolute mathematics",
"neutral mathematics" or fill-in your terminology. I prefer "neutral",
although this is problematic, as there isn't a unique neutral
mathematics. I haven't found a perfect terminology.

In such a neutral mathematics, used as a veihicle for constructive
mathematics, we tend to say things such as "LPO doesn't hold". Of
course, what we really mean is that LPO is undecided, but prevented by
constructive interpretations of the neutral theory, whatever
"constructive interpretation" may mean.

A good terminology was introduced by Peter Aczel: LPO is a
[constructive] taboo, rather than false. And there are many other
taboos, with their relationships widely investigated within (different
forms of) neutral mathematics.

So, for example, rather than saying that the existence of a
non-continuous function N^N->N is false (as Brouwer would say), in
neutral mathematics, we say that it is a taboo, reducing it to some
canonical taboo such as WLPO.

What we do is to replace implications "A -> false" by implications

"A -> some-canonical-taboo".

But also, when using neutral mathematics as a vehicle for constructive
mathematics, we sometimes replace A by "true -> A" without noticing,
and then "true" by what I would like to call a co-taboo, to get


"some-canonical-co-taboo -> A".

Such co-taboos include "all functions of a certain kind are
continuous" and "all functions of a certain kind are computable",
among others.

So, sometimes,

"A [potentially] fails" may mean "A -> some-taboo"

and

"A [potentially] holds" may mean "some-co-taboo -> A".

If something potentially holds in neutral mathematics, we can't expect
to prove it false.

If something potentially fails in neutral mathematics, we can't expect
to prove it true.

I think I would prefer to see principles such as "all functions of a
certain kind are continuous" not as things I would like to postulate
as axioms, but rather as things that I would like to take as co-taboos
when using neutral mathematics as a vehicle for constructive
mathematics.

But then, of course, the distinction of neutral and contructive
mathematics is blurred. (This is why I said "neutral mathematics as a
vehicle for constructive mathematics".)

For instance, Martin-Loef Type Theory (of its various forms) is both
neutral and constructive. However, one thing is clear: excluded middle
is not false - it is merely a taboo. Contravariantly, the uniform
continuity of all functions 2^N->N is not true, but it is a co-taboo.

There must be a better word than co-taboo to convey this idea.

Martin

[Andrej Bauer]

On Sat, Feb 6, 2016 at 2:46 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> I argue that co-taboos also occur (but they deserve a better name).

A constructive fetish.

[Erik Palmgren]

Why not just say "A is constructively consistent" with neutral/Bishop
mathematics if there is a constructive model of A. The model need
not be a Tarski model of course. It is known that
neutral mathematics has a greater "axiomatic freedom" (not sure who
coined that term) than classical mathematics.

Erik

[Erik Palmgren]

Constructive (or constructivist) principle is good,
and is used in the Troelstra & van Dalen volumes from 1988.


Den 2016-02-06 kl. 15:41, skrev Thorsten Altenkirch:
> But taboos are also consistent?
>
> Why not constructive principle which makes it clear that it is not just minimalist. Many constructive principles are anti classical but this is not necessarily so.
>
> Thorsten
>
> Sent from my iPhone

>> --
>> 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.
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment. Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>

[bhup....@gmail.com]

On 06 February 2016 02:46, Martin Escardo wrote in construc...@googlegroups.com:

"Immerse yourself in a form of constructive mathematics that is compatible with classical mathematics and also with any other known form of constructive mathematics. ... In such a neutral mathematics, used as a veihicle for constructive mathematics, we tend to say things such as "LPO doesn't hold". Of course, what we really mean is that LPO is undecided, but prevented by constructive interpretations of the neutral theory, whatever "constructive interpretation" may mean. ... If something potentially holds in neutral mathematics, we can't expect to prove it false. If something potentially fails in neutral mathematics, we can't expect to prove it true. ... There must be a better word than co-taboo to convey this idea."

A possible candidate (see link below): A form of constructive mathematics that distinguishes between the concept of `algorithmically verifiable truth' in the non-finitary---hence essentially subjective---reasoning that circumscribes human intelligences (which, by the Anthropic principle, can be taken to reflect the 'truths' of natural laws), and the concept of 'algorithmically computable truth' in the finitary---hence essentially objective---reasoning that circumscribes mechanical intelligences.

http://alixcomsi.com/11_Three_Perspectives_of_FOL_Outline.pdf

Regards,

Bhup

[Martin Escardo]

On 06/02/16 14:56, Erik Palmgren wrote:
> Constructive (or constructivist) principle is good,
> and is used in the Troelstra & van Dalen volumes from 1988.

But there are examples of propositions A and B, each of which can be
given a constructive interpretation in certain neutral systems such as
HA^omega, but which contradict each other in the same systems.

For example, take A = (continuity and extensionality) and B=choice, or
A=continuity and B=(extensionality and choice).

I wouldn't like to regard such A and B as intrinsically constructive
principles if they can't hold together, even though each of them
separately does have a constructive interpretation.

Even more, there are examples of propositions A and B such that each of
them can be given a constructive interpretation, but we don't know at
present if they are together consistent.

For example, take A=continuity and B=univalence in intensional MLTT.

Maybe only the principles of neutral mathematics can be considered to be
intrinsically constructive, by the very definition of neutral
mathematics (has to be compatible with classical mathematics and any
form of constructive mathematics).

Of course, tabooness has to be qualified. Although continuity is not a
constructive taboo (I regard it as a constructive co-taboo), it is of
course a taboo of neutral mathematics, in that as soon we prove that
A->continuity, we learn that A cannot be a neutral/absolute truth.

Martin

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

[Martin Escardo]

On 07/02/16 12:27, Thorsten Altenkirch wrote:
> Different constructive principles may contradict each other. Why is this a
> problem?

If you are talking about "accepted" constructive principles (co-taboos),
I don't see a problem.

But consider the following.

In intensional MLTT, if you postulate not-A for any closed type
expression A such that not-A is consistent, then you remain strongly
normalizing to canonical forms, and hence not-A has a computational
interpretation in this sense.

In particular, not-not-excluded-middle has a computational
interpretation (where you can take excluded middle in its strong form
Pi(X:U).X+(X->0)).

However, although this shows that doubly-negated excluded middle does
have a computational interpretation in MLTT style, I don't regard it as
a constructive principle. Using the same method, for any type A such
that not-not-A is "accidentally" consistent, we can have the
"constructive" axiom not-not-A with a vacuous computational
interpretation. But do we really wish to think of not-not-A as a
constructive principle?

My only point is this (I think): if you want to use neutral mathematics
as a vehicle for constructive mathematics (as Bishop tried to do, and as
Martin-Loef type theory does), and neutral mathematics is not your
objective, then you need to look at taboos (things that are regarded as
non-constructive) and co-taboos (things that are regarded as pertaining
to constructivity, even though they can't be proved in neutral mathematics).

But I would like to emphasize that what is a "constructive taboo" is not
intrinsically clear. For instance, you may regard LPO as clearly a
constructive taboo. But why? For instance, if you replace the set N of
natural numbers by the set N_infty of natural numbers with a point at
infinity, we move from something that was regarded as a taboo to
something that is just true.

We may have thought that LPO is dubious because it is a decision that
involves an infinite quantification. But then such a decision is
possible for an infinite quantification over an even larger set.

What makes LPO to be an intrinsic constructive taboo (other than the
fact that there is a (computational) model of neutral mathematics in
which it fails)?

How can we look at LPO and doubt it, when we look at the similarly looking

forall p:N_\infty->2, either p(x)=0 for some x:N_\infty, or else
p(x)=1 for all x,

and conclude that it just holds in neutral mathematics, and hence in
constructive mathematics of any kind?


Martin


>
> There are also extensions of ZF which contradict each other. Hence the
> situation isn¹t really so unusual and isn¹t even restricted to
> constructive mathematics.
>
> Thorsten

[Martin Escardo]

On 08/02/16 09:50, Thorsten Altenkirch wrote:
> I am confused since non-non-excluded middle is a minimalist tautology.


not-not(p or not p) always holds.

But not-not(forall p. p or not p) doesn't need to hold. This is
not-not-excluded middle. It contradicts continuity principles.

Martin