Advert & question

[Martin Escardo]

A while ago, I advertised a proof that a certain infinite set, larger
than N, satisfies the principle of omniscience in Bishop mathematics.
I want to advertise a blog post about that:

http://math.andrej.com/2014/05/08/seemingly-impossible-proofs/

In order to both check that I was right and be able to run the proofs
in the computer (after all, they are constructive), I have formalized
them in Martin-Loef type theory (MLTT), in Agda notation, where Agda
is a constructive-proof computer system based on MLTT.

But also I want to remark on hurdles I have had when trying to
translate Bishop statements to MLTT statements. Does the Curry-Howard
correspondence really give the interpretation of the
quantifiers/logical connectives that Bishop mathematicians have in
mind?

I am not sure. In a relatively recent message, I discussed a
counter-example, namely that if all functions N^N->N are continuous
then 0=1, when continuity is interpreted via Curry-Howard (aka BHK).

Anyway, I think that, after some work, I did overcome the hurdles in
what I discuss in the above blog post (you may disagree, please tell
me if so - this is a question of whether my formalization really does
formalize what is said informally and presumably rigorously).

But here I want to report another counter-example I came across in the
last few days.

Claim. Suppose LLPO is interpreted via CHBHK. Then WLPO<->LLPO.

I don't care much about WLPO and LLPO per se, but they serve as
precise demarcations of the boundaries of the classical and
constructive provinces of mathematics, as the work on reverse
constructive mathematics shows.

Now, I believe I've seen a description of a model of (some
formalization of) Bishop in which WLPO fails but LLPO holds.

LLPO = for every binary sequence with at most one 1, either
all even terms are 0, or all odd terms are 0.

If we interpret "or" as "+" via CHBHK, we get a non-continuous
function of the binary sequences with at most one 1 into the two-point
set 2, by analysing which branch of "+" we land in using the LLPO
oracle, which is necessarily non-continuous, and hence we get WLPO (by
Ishihara's work (and also by my overlapping recent work)).

The trouble is, when one reads "exists" and "or" in Bishop, often the
CHBHK interpretation is meant (namely Sigma and "+" in MLTT), but not
always (as in LLPO, and in the definition of continuity for functions
N^N->N, but also in many other cases, such as the definition of the
Dedekind reals).

What are "exists" and "or" meant to mean, when the CHBHK
interpretation is not meant, as in the examples of LLPO and continuity
of functions N^N->N?

One possible answer is provided by HoTT, but I would like see your
independent answers before proposing that.

Martin

[bhup....@gmail.com]

How would the argument reconcile with the following finitary
number-theoretic argument that no interpretation of the first order Peano
Arithmetic PA can admit an infinite set larger than N?

(i) Define a number-theoretic function f(x) as algorithmically verifiable
iff, for any given natural number n, there is a deterministic algorithm that
determines the value of each of {f(1), f(2), ..., f(n)}.

(ii) Let r(n) denote the n'th digit in the unique decimal expansion that
defines a putatively given real number R in the interval 0 < R < 1.

(iii) By the definition of a real number as the limit of a Cauchy sequence
of rationals, it follows that r(n) is an algorithmically verifiable
number-theoretic function.

(iv) By Goedel's primitive recursive Beta-function, every algorithmically
verifiable number-theoretic function is uniquely representable by an
arithmetical formula in PA.

(v) Since PA is first order, the reals are denumerable.

The detailed argument is accessible at:

http://alixcomsi.com/47_Continuum_Hypothesis_Update.pdf

Bhup

======================

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

On 14/05/14 14:33, bhup....@gmail.com wrote:
> How would the argument reconcile with the following finitary
> number-theoretic argument that no interpretation of the first order Peano
> Arithmetic PA can admit an infinite set larger than N?

I am working in a system richer than PA, in which sets other than N are
available. In particular, given two sets X and Y, you can form the set
of functions X->Y. When X=Y=N this is the set of sequences of natural
numbers. By Cantor's diagonal argument, this set is uncountable
(constructively, in the sense that given any enumeration of sequences,
we can build a sequence not listed in the enumeration).

Of course, this is within the theory - you may well have a model in
which (according to your meta-theory), N->N is interpreted as a
countable set. Cf. Skolem's paradox. In the advertised theorems, we
don't talk about models. We reason within the theory (formally
Martin-Loef type theory, but, as said in the post, the claimed results
are meant to be valid in Bishop mathematics too, although this is open
to interpretation, as Bishop mathematics is (deliberately, for bad or
for good) not a formal system).

M.

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

[Bhupinder Singh Anand]

In what sense would you see the argument as an instance of Skolem's paradox
(since the arithmetical argument I outlined for the denumerability of the
reals does not appeal to any axiomatic properties of any particular formal
system of arithmetic such as PA), and in what sense can one define an
infinite set in any formal or informal system of arithmetic (whether PA, or
a system richer than PA, or Bishop's constructive mathematics) that can be
termed arithmetically as 'larger' than N?

After all, for any formal (or informal) system of arithmetic to be
mathematically meaningful, shouldn't it admit the possibility of an
interpretation that includes the natural numbers and preserves those of
their arithmetical properties that are, minimally and unarguably, accepted
by conventional wisdom under the standard interpretation of arithmetic?

The argument I outlined (essentially an unusual arithmetical perspective of
CH which apparently dissolves Skolem's paradox) simply suggests there may be
constructive limitations on the possibility of defining an infinite set in
any formal system of arithmetic (whether PA, or a system richer than PA, or
Bishop's constructive mathematics) that can be interpreted in any model of
the theory as arithmetically 'larger' than N, by highlighting a putative 1-1
correspondence between:

(a) any putative real number R in the interval 0 < R < 1;

(b) its associated unique decimal expansion that---viewed as a Cauchy
sequence---must then correspond, uniquely and constructively, to an
algorithmically verifiable number-theoretic sequence {r(n)};

(c) a well-defined arithmetical formula that must then correspond, uniquely
and constructively, by Goedel's primitive recursive Beta function to the
sequence {r(n)}.

That the arithmetical formula is also accepted as a PA formula by the
standard representation theorem (Theorem VII of Goedel's seminal 1931 paper
on formally undecidable arithmetical propositions) merely implies that the
set of such formulas is, by definition, first order (whence denumerable).

Regards,

[Andrej Bauer]

Dear Bhup,

your arguments contain flaws and misconceptions. For example, you
claim that your argument works in constructive logic, but:

>(b) its associated unique decimal expansion that---viewed as a Cauchy
>sequence---must then correspond, uniquely and constructively, to an
>algorithmically verifiable number-theoretic sequence {r(n)};

To say that every real has a unique decimal expansion requires
non-constructive logic.

The functions you speak of are normally called "computable", not
"algorithmically verifiable".

(c) a well-defined arithmetical formula that must then correspond, uniquely
and constructively, by Goedel's primitive recursive Beta function to the
sequence {r(n)}.

You are probably mixing up primitive recursion and general recursion
here, but it is hard to tell as your terminology is not standard.

The general idea of your argument is well known. To make it
technically sound we can use Kleene's number realizability from 1943.
In Kleene's realizability model every computable real number is
associated with the set of (codes of) those Turing machines that
compute its decimal expansion. This shows that the set of computable
reals is a quotient of a subset of the natural numbers. This of course
means that there are at most countably many computable reals.

However, there is a distinction between "enumerable" and "enumerable
in a model". Martin hinted at that when he mentioned Skolem's paradox.
*Inside* the realizability model you can still validate the usual
Cantor's diagonal argument to show that there is onto map from natural
numbers to reals.

With kind regards,

Andrej

[Giovanni Sambin]

Dear Martin,

thank you for your post. I believe your results and resulting questions are very interesting. It will take me more time to go through the details of your proofs and try to properly understand their meaning. Here I begin to give an answer to two question of yours of a more general nature.

>Does the Curry-Howard correspondence really give the interpretation of the

>quantifiers/logical connectives that Bishop mathematicians have in mind?

Also at the light of the content of your post, I believe the answer is: no. As often underlined by Douglas Bridges, Bishop mathematics is just mathematics done using intuitionistic logic, where -as I understand- intuitionistic logic is meant to be logic, as distinct from set theory (interpreted as logic via Curry-Howard). We have the privilege of now having Douglas here as a guest. He confirms.

Anyway, there are also historical and logical arguments supporting this view. Historically, Bishop published his book in 1967, definitely before Howard's paper (if I remember well, this circulated as a preprint beginning in 1969). Martin-Löf's formalization of Curry-Howard isomorphism, namely his propositions-as-sets interpretation, came even later. In other words, Bishop did not have the rules for Sigma and the interpretation of Exists as Sigma.

The same conclusion is reached also by a technical argument. Bishop meant to do standard mathematics. There is no doubt that he had extensionality (sets, now sometimes called setoids,  have extensional equality, two functions are equal when they give the same values). We know (for instance, by  Martin-Löf's paper "100 hundred years of Zermelo's axiom of choice") that AC is not valid in an extensional theory, like that of setoids used by Bishop. So the assumption that Exists=Sigma is ruled out, since we know that it would give AC.

>What are "exists" and "or" meant to mean, when the CHBHK interpretation

>is not meant, as in the examples of LLPO and continuity of functions

N^N->N?

The easy part of my answer is: "exists" and "or" are exactly as in intuitionistic logic (without proof-terms and Curry-Howard). This has always been clear to me since the beginning of my involvement with formal topology in the 80s (it is explicitly said on page 2 of my first paper). In fact, one needs standard intuitionistic logic in order to obtain a reasonable theory of subsets. Actually, I still wonder how some authors claim using Martin-Löf type theory as a foundation, and then play with subsets with no problems. What is a subset? When are two subsets equal? What is the union of a family of subsets? All these questions have crystal clear answers if you have access to standard intuitionistic logic, including the judgement A true. I don't see similar simple answers otherwise. My treatment of subsets is similar to Bishop's one, except that for me a subset is a propositional function over a set, and hence it is never a set.

In other words, we should not identify the informal BHK interpretation, followed by Bishop, with its formal expression as in Martin-Löf type theory, through propositions-as-sets.

Less easy is to explain how one can put the use of intuitionistic logic together with a computational interpretation of set theory, as in Martin-Löf type theory. This is a problem I faced since the 80s and which, after 20 years, I  believe is totally solved by our (we = Milly Maietti and me) Minimalist Foundation proposed in 2005.  If you are interested, I can explain in a next post the ideas of MF. This post is already sufficiently long...

All the best

Giovanni

Martin

[Martin Escardo]

Dear Giovanni,

Thanks for your answer.

On 15/05/14 11:06, Giovanni Sambin wrote:
> >Does the Curry-Howard correspondence really give the interpretation of the
> >quantifiers/logical connectives that Bishop mathematicians have in mind?
>
> Also at the light of the content of your post, I believe the answer is:
> no. As often underlined by Douglas Bridges, Bishop mathematics is just

> mathematics done using intuitionistic logic.

This is what Bishop followers claim, but it is not what Bishop himself
seems to say and do in his two books (one with Douglas). He even
speculates that "choice holds by the very meaning of existence". Also,
in practice, when he proves a forall-exists theorem, he goes on to
define (explicitly or implicitly) a procedure to construct the
exists-output from the forall-input.

> The easy part of my answer is: "exists" and "or" are exactly as in
> intuitionistic logic (without proof-terms and Curry-Howard).

The case of "or" (for me) is harder to analyse empirically by reading
the books, because there are hardly any theorems with "or" in the
conclusion.

In connection with the subject matter of the post (but at that time
not in connection with the discussion of this message), a few years
ago Douglas Bridges mentioned Bishop’s 1967 proof of Lemma 7 of
Foundations, page 177, which I mention in the JSL paper.

In this example, there is "or" in the conclusion, and with the proof
Bishop gives, the "+" interpretation of "or" works, as he gives an
explicit procedure to decide the branch and produce the corresponding
or-output data from the forall-input data.

Some such or-in-the-conclusion examples, in the same spirit, occur in
Ishihara's work.

The example I gave was that if or=+ is taken in LLPO and WLPO, then
they are equivalent, but there is a model of intuitionistic set theory
(where?) that validates LLPO but not WLPO (and we always have
WLPO->LLPO).

What I don't have at the moment is an example or a "real" statement
where it would make a difference to take intuitionistic or or +.

But with "exists" such examples occur: if all functions N^N->N are
continuous then 0=1 if you take exists=Sigma, but with the
intuitionistic exists there are models of that. Now it seems strange
to name the BHK interpretation after Brouwer, because for him all
functions N^N->N were continuous, but this is inconsistent with the
BHK interpretation of continuity.

The above situations, however, don't describe the problems I
face. They occur in two situation: (1) when making definitions (should
we take one exists or the other)? (2) Similarly, in hypotheses of
therems with an existential deeply inside the premise (which one is
meant?).

In homotopy type theory, one has both the intuitionistic exists and
Sigma (and or and +), and one can choose which one is appropriate for
whatever one is doing, if we are formulating our own theorems and
proofs. But if we look at somebody else's theorems, it is less simple
to figure out which one is meant (and I assure you, sometimes it is
one and sometimes is the other, and sometimes is not clear at all).

> Less easy is to explain how one can put the use of intuitionistic logic
> together with a computational interpretation of set theory, as in
> Martin-Löf type theory. This is a problem I faced since the 80s and
> which, after 20 years, I believe is totally solved by our (we = Milly
> Maietti and me) Minimalist Foundation proposed in 2005. If you are
> interested, I can explain in a next post the ideas of MF. This post is
> already sufficiently long...

Ok, thanks.

Best,
Martin

[Maria Emilia Maietti]

Dear Martin
many thanks for your questions.


I can not show what is the best foundation for Bishop's mathematics
(and to answer your points in Bishop's proofs)

but I think it should model

-effective quotients (to represent Bishop's reals)

- proof-irrelevance of propositions (to work informally as most
constructive mathematicians do) at least validating intuitionistic logic

- power-collections (power-sets if not predicative) with usual
extensional equality of subsets.

and as claimed by most followers

- be compatible with classical mathematics.


Now by Diaconescu's argument (put in type theoretic terms in many places
including my PhD thesis) we know that all these features
are not constructively compatible
with full axiom of choice and hence with "exists=Sigma".


Then one could argue that you can get all the above features

(*) if you work
within the setoid model (a' la Bishop) of Martin-Loef's type theory(MLTT)
where the right kind of axiom of choice holds (Aczel's presentation
axiom if you prefer).

We can think of Bishop's pre-sets as Martin-Loef's intensional sets
and Bishop's sets as Martin-Loef's total setoids.


But working in this model, think of dependent setoids, is difficult,
it needs a proof-assistant to deal with proof-terms in order to exploit
the brutal force
of "exists=Sigma". But then the informal reasoning of usual mathematical
practice is far away.

Here I have questions:

1.
how can we make proofs in the setoid model over MLTT compatible with
classical mathematics in a ZFC set theory?

2. how can we make proofs in MLTT compatible with classical mathematics
in a ZFC set theory by sending propositions to propositions (=preserving
the meaning of quantifiers)?
Indeed, I only know the interpretation of MLTT in classical set theory
where you interpret sets as sets and propositions are again sets but
this is not useful for compatibility, just shows relative consistency.


In fact a major advantage of Bishop's constructive development contrary
to Brouwer's is often said to be its ***compatibility with classical
mathematics*** but for MLTT or all the theorems valid in its setoid
model this is not clear to me.

This is to me a main motivation for looking for another foundation as
Aczel's CZF or even better (for me and Giovanni) our (extensional level)
Minimalist Foundation with additional principles, (for example countable
choices) when really needed.


Many thanks for your attention
Milly

[Fred Richman]

Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>> As often underlined by Douglas Bridges, Bishop mathematics is just
>> mathematics done using intuitionistic logic.

> This is what Bishop followers claim, but it is not what Bishop himself
> seems to say and do in his two books (one with Douglas). He even
> speculates that "choice holds by the very meaning of existence".

I should probably refrain from commenting on this thread, but here goes anyway.

First of all, Bishop's statement that "choice holds by the very meaning of existence" is difficult to reconcile with the fact that he introduced different names for functions that are onto and functions that have right inverses.

Worrying about exactly what Bishop meant reminds me of Andre Scedrov's comment about regarding Brouwer the way people used to regard Lenin.

I see little reason to believe that Bishop considered constructive mathematics as just mathematics done using intuitionistic logic. If that were the case, he might have dropped some hints so it wouldn't have taken me so long to come to that conclusion, a conclusion which was pretty much empirical: it looked to me like a paper would be considered a piece of constructive mathematics exactly when it was written in the context of intuitionistic logic.

To my mind, the biggest reason against believing that Bishop thought that way is the central role he assigned to his notion of an operation, which has no analogue in classical mathematics or in Brouwer's thought. Of course you can see it in Russian constructivism, or in what used to be called recursive function theory, where an operation is a specific kind of algorithm. Most of the time you can rephrase statements in Bishop-style constructive mathematics that refer to operations to eliminate that reference. The only instance I know of where that did not seem possible was the treatment of Noetherian rings by Jonathan Tennenbaum, a student of Bishop's. In any event, talk about operations seems to have pretty much disappeared from Bishop-style constructive mathematics.

--Fred

[Martin Escardo]

On 15/05/14 19:22, Fred Richman wrote:
> Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
>>> As often underlined by Douglas Bridges, Bishop mathematics is just
>>> mathematics done using intuitionistic logic.
>
>> This is what Bishop followers claim, but it is not what Bishop himself
>> seems to say and do in his two books (one with Douglas). He even
>> speculates that "choice holds by the very meaning of existence".
>
> I should probably refrain from commenting on this thread, but here goes anyway.
>
> First of all, Bishop's statement that "choice holds by the very meaning of existence" is difficult to reconcile with the fact that he introduced different names for functions that are onto and functions that have right inverses.

Exactly! If you define "onto" using Sigma, you actually get "has a right
inverse". If you want to define "onto", you must not use Sigma, but
instead the intuitionistic existential.

Such a distinction is possible in so-called HoTT.

> Worrying about exactly what Bishop meant reminds me of Andre Scedrov's comment about regarding Brouwer the way people used to regard Lenin.

Probably. But one does has to worry IF one is translating pieces of
Bishop mathematics to Martin-Loef type theory, or perhaps to HoTT, in
the computer, as people do using Coq and Agda and similar.

Your example precisely illustrates that. I don't want you to read 10
lines of Agda, but these 10 lines

http://www.cs.bham.ac.uk/~mhe/agda/Retraction.html

define retraction with a definition that looks like that of surjection.

So I run in the very issue you mention above.

I don't think you can define surjection in MLTT. But in its extension
HoTT, you can, because in addition to Sigma you have the intuitionistic
exists.

In any case, this is a good example of the general issue Sigma vs exists
when one tries to translate from Bishop to MLTT (via BHK).

This is precisely the kind of issue I had in mind in my original question.

How do we figure out which one to use when reading Bishop and writing in
MLTT? In the case of surjection vs retraction, this is clear, and so it
is in many other cases.

Martin

> I see little reason to believe that Bishop considered constructive mathematics as just mathematics done using intuitionistic logic. If that were the case, he might have dropped some hints so it wouldn't have taken me so long to come to that conclusion, a conclusion which was pretty much empirical: it looked to me like a paper would be considered a piece of constructive mathematics exactly when it was written in the context of intuitionistic logic.
>
> To my mind, the biggest reason against believing that Bishop thought that way is the central role he assigned to his notion of an operation, which has no analogue in classical mathematics or in Brouwer's thought. Of course you can see it in Russian constructivism, or in what used to be called recursive function theory, where an operation is a specific kind of algorithm. Most of the time you can rephrase statements in Bishop-style constructive mathematics that refer to operations to eliminate that reference. The only instance I know of where that did not seem possible was the treatment of Noetherian rings by Jonathan Tennenbaum, a student of Bishop's. In any event, talk about operations seems to have pretty much disappeared from Bishop-style constructive mathematics.
>
> --Fred
>

[Maria Emilia Maietti]

Dear Fred and Martin

concerning

On 05/15/2014 08:22 PM, Fred Richman wrote:
> The only instance I know of where that did not seem possible was the
> treatment of Noetherian rings by Jonathan Tennenbaum, a student of
> Bishop's. In any event, talk about operations seems to have pretty
> much disappeared from Bishop-style constructive mathematics. --Fred

one of the main motivations to develop the Minimalist Foundation
by Giovanni Sambin and myself
is to keep the
distinction ''operation and function'' (as in Feferman's theories)

which is **not present in Aczel's CZF ***and it is lost with
''exist=Sigma'' in Martin-Loef's
type theory (MLTT).
Also this distinction is lost when axiom of unique choice is validated,
for example in the internal theory
of a Heyting pretopos or a topos (in MF the axiom of unique choice is
not derivable).

Hence the Minimalist Foundation (MF) (in the extensional level)
as finally formalized in
http://www.math.unipd.it/~maietti/papers/tt.pdf

is the best option to our knowledge ( for me and Giovanni Sambin)
to formalize Bishop's constructive mathematics, for the above reason
and because we have a clear
extensional theory (close to the language of usual mathematical
practice) and an intensional one (to be implemented in a
proof-assistant) and an interpretation via setoids between the two.

Finally MF is compatible with **classical predicative mathematics**
contrary to CZF and MLTT.

Our next research plan is to compare our MF with Feferman's constructive
and classical theories.

Best wishes
Milly

[Altenkirch Thorsten]

Hi Milly,

I remember discussions with you and Giovanni several years ago on this
topic - before HoTT became fashionable. At this time I already suggested
to define exists as squashed Sigma (squash types were known in NuPRL, aka
Bracket types Awodey/Bauer).

Also the notion of "propositions" was known in Type Theory before HoTT as
a type with at most one element and it is clear that there should be a
notion of existential which is closed under propositions. The distinction
between Sigma and Exists is very useful and historically wasn't available
to Bishop, but times have changed.

Now, I wonder wether this should lead you and Giovanni reconsider the need
for minimalist foundations as you have suggested? Having said this it is
interesting that a two level theory (intensional/extensional) is discussed
again in the HoTT community under the name of HTS (homotopy Type System)
proposed by Voevodsky. However, the motivation seems quite different and
(re-)introduces the notion of a strict, i.e. proof-irrelvant equality for
every type (which however isn't univalent).

Cheers,
Thorsten

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

Dear Andrej,

Thanks for your critical---and justifiably chastising---observations. I am indeed culpable.

1. I should have clarified in my post, itself, that my comments were from the perspective of a back-to-the-basics constructive logic that differs significantly from both classical (Hilbertian) logic and the usual non-classical logics, in that the perspective:

(i) accepts the formal classical first order logic FOL as finitarily consistent;

(ii) does not accept the Hilbertian, epsilon-calculus inspired, prescription that 'neg(Ax)F(x)' always implies 'neg F(a)' for some term 'a' of the logic (in other words, it does not accept that FOL can be assumed to be omega-consistent);

(iii) does not accept that accepting (ii) must imply that the Law of the Excluded Middle does not hold (and that FOL cannot therefore be treated as a constructive logic).

2. The proof that FOL is finitarily consistent follows immediately from the proof that the first order Peano Arithmetic PA is finitarily consistent; as detailed in the following paper on ‘Evidence-Based Interpretations of PA’ that I presented at AISB/IACAP 2012 at Birmingham:

http://events.cs.bham.ac.uk/turing12/proceedings/04.pdf

3. In this paper I showed that PA has two Tarskian interpretations (one finitary and one non-finitary) over the domain N of the natural numbers.

4. The non-finitary interpretation is the familiar 'standard' interpretation of PA; where I show that the truth of the atomic formulas of a formal language is defined in terms of algorithmic verifiability.

5. The finitary interpretation is a 'Kleenian' interpretation of PA; where the truth of the atomic formulas of a formal language is defined in terms of algorithmic computability (corresponding to Kleene's realizability).

6. The 'standard' interpretation is 'non-finitary' (as is well-known) since---although it can be shown (link below) that the PA axioms interpret as true with respect to algorithmic verifiability, and the rules of inference preserve such truth---the compound formulas of PA are not 'finitarily' decidable with respect to algorithmic verifiability.

7. The 'Kleenian' interpretation is 'finitary' since---whilst (as shown in the above paper) the PA axioms interpret as true with respect to algorithmic computability, and the rules of inference preserve such truth---the compound formulas of PA are also now 'finitarily' decidable with respect to algorithmic computability.

8. The consistency of the 'non-finitary' interpretation of PA is proven---and the arguments of the above paper revised and updated---in a current investigation (link below) of the consequences that the distinction between algorithmic verifiability and algorithmic computability may have for Cognition and Lucas’ Goedelian Thesis:

http://alixcomsi.com/28_Human%20Reasoning_v_Mechanistic%20Reasoning_2014_Update.pdf

As to the specific points raised by you:

(a) I don’t have a sense of whether or not my argument “works in constructive logic”; I only suggested that there may be constructive limitations on the possibility of consistently introducing through definition an infinite set into any formal system of arithmetic (whether PA, or a system richer than PA, or Bishop's constructive mathematics) that can be ‘interpreted’ in any model of the theory or constructive logic as arithmetically 'larger' than N.

(b) The ‘algorithmically verifiable’ argument I offered does not need to assume that every real number R must have a uniquely constructible decimal expansion. It should be sufficient to accept that R is the limit of some unique notional Cauchy sequence, and therefore its associated sequence has the property of being algorithmically verifiable.

What I have in mind is that, once we accept the mathematical existence of uncountable reals as necessary in order to complete the real number field, then Cantor’s diagonal argument can also be interpreted as illustrating that an uncountable real 'has' the property of being algorithmically verifiable but not algorithmically computable.

(c) The argument for the arithmetical denumerability of the reals applies only to the reals as defined classically in terms of Cauchy sequences. Moreover, it appeals only to the evidence-based distinction between the algorithmic computability and the algorithmic verifiability of number-theoretic functions over the domain N of the natural numbers. The argument does not claim to apply to reals defined otherwise, nor does it appeal to non-constructive Skolem-inspired enumerability in the domain of any putative non-standard model of arithmetic.

Thanks and regards,

Bhup

======================
-----Original Message-----
From: construc...@googlegroups.com [mailto:construc...@googlegroups.com] On Behalf Of Andrej Bauer
Sent: 15 May 2014 10:02
To: Bhupinder Singh Anand; construc...@googlegroups.com
Subject: Re: Advert & question

[Martin Escardo]

Dear Milly,

I am not saying that I don't like your foundations or that they don't do
the job. I am sure they do.

I was asking a question about Bishop vs BHK, and in particular the
Curry-Howard implementation of BHK carried out by Martin-Loef.

I am surprised to hear that MLTT is not compatible with classical
mathematics. You mean because you can't formulate choice? HoTT can
formulate choice because it has Exists in addition to Sigma. (The usual
choice with Sigma which is valid in MLTT of course has nothing to do
with choice, and is just true, as you know.) The HoTT book explains very
clearly how HoTT is compatible with classical logic, and has all the
desirable constructions you mention.

But also, I am not very familiar with NuPrl, which is based on
extensional MLTT, but it seems to me that it is both compatible with
classical logic and also has the constructions you want.

Anyway, this is just a digression prompted by what you say.

What I was discussing is that it seems essential to have both Sigma and
Exists in a constructive foundation, to make certain meaningful
distinctions.

I realize that many people in this list won't be interested in
foundations. But people who write constructive proofs that computers can
diggest need them (or, rather, let's say that at least the computers
definitely need them).

Martin

[Martin Escardo]

On 16/05/14 15:57, Martin Escardo wrote:
> I realize that many people in this list won't be interested in
> foundations. But people who write constructive proofs that computers can
> diggest need them (or, rather, let's say that at least the computers
> definitely need them).

Bishop was interested in this enterprise, and in fact he proposed it
himself (so we can blame him):

Bishop, Errett (1970) Mathematics as a numerical language. 1970
Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y., 1968)
pp. 53–71. North-Holland, Amsterdam.

Now, his mathematics was deliberately informal, and I sympathize with
that. And so do the HoTT crowd, who wrote the HoTT book
*deliberately* in an informal language, at the same time they were
implementing the book in Coq and Agda formally. Moreover, many
portions of the book are informalizations of proofs that were done
first formally in one of these two systems.

In this context, the question of whether/when Bishop means Sigma for
Exists is a practical, rather than merely philosophical or dogmatic
(Leninian) one. When you formalize a piece of mathematics in a
computer, you have to figure out and supply the (deliberate or
accidental) missing details.

In the next message I will briefly explain how the Sigma/Exists
distinction works in HoTT (already hinted by Thorsten Altenkirch in
this thread), which is an extension of Martin-Loef Type Theory.

Martin

[Martin Escardo]

So much for speculation. As a preamble to explain Exists from Sigma,
let's consider Fred's example (thanks for bringing it up):

We have sets X and Y and a function f:X->Y and we want to say that f
is onto, but doesn't necessarily have a right inverse.

Clearly, what we should say, then, is:

(1) forall y:Y. exists x:X. f(x)=y.

Attempt in type theory: We say (via Curry-Howard) that the set

(2) Pi y:Y. Sigma x:X. f(x)=y

is inhabited. What is Pi? Just the cartesian product. What is Sigma?
Just the disjoint union. What is the set "f(x)=y". In bishop
mathematics, it would be

{z in 1 | f(x) = y}.

What is an inhabitant of the above type (2)? Just a function that
given y:Y finds x:X such that f(x)=y.

But then, bingo, this function gives a right inverse Y->X.

And, clearly, there are surjections that don't have right
inverses. So, how do we define surjection in the Curry-Howard world?

On 16/05/14 21:58, Martin Escardo wrote:
> In the next message I will briefly explain how the Sigma/Exists
> distinction works in HoTT (already hinted by Thorsten Altenkirch in
> this thread), which is an extension of Martin-Loef Type Theory.

In MLTT, there is no distinction between propositions and types/sets,
and this comes from the BHK interpretation of logic, which I will not
rehearse, but is illustrated above.

In the HoTT view, a proposition is a particular kind of type: one that
has at most one element. (Sometimes called an hproposition.)

There is an operation that converts any type X into a proposition
||X||. Intuitively, ||X|| is the claim that X is inhabited without
revealing *in principle* any element of X.

In Bishop mathematics, this can be defined as

||X|| = { z in 1 | X is inhabited }.

(In type theory, this is necessarily defined in a subtler way.)

The set ||X|| is positively defined, but knowing an element of ||X||
doesn't reveal any element of X (actually *sometimes* it does).

In HoTT, which is a type theory in the realm of BHK/Curry-Howard, so
that the logic is encoded in the mathematics, we define the type

Exists x:X. A(x) = || Sigma x:X. A(x) ||.

While the axiom of choice is obviously true with Sigma, it is "clearly
false" with Exists (or clearly a taboo or Browerian counter-example).

So let me close with Fred's example. We express the fact that f:X->Y
is onto, in such a type theory, by the proposition

Pi y:Y. || Sigma x:X. f(x)=y ||.

This is how mathematics is done in the HoTT Book: sometimes we put
||-|| around Sigmas, and sometimes we don't.

When translating Bishop to type theory, it is not always clear when
||-|| is needed/intended/desirable.

(Technical remark: when interpreting constructive mathematics in a
topos, it is a *fact* that Exists is characterized from Sigma in this
way. Sigma is present in a topos via its "local cartesian
closedness". Hence the distinction Exists/Sigma, as well as its
relationship, could have been emphasized independently of constructive
mathematics needs.)

(Historical remark. People in NuPrl pioneered the idea of something
like ||-||, but there are two differences: (1) they work in
extensional type theory, for which there are important subtle
differences, and (2), their correponding "bracket types" don't have
good elimination rules when applied to the intensional version of the
theory, which is the one (that has to be) used in in HoTT.)

Martin

[Maria Emilia Maietti]

Dear Martin
many thanks for your interest.
Very quickly

>
> I am surprised to hear that MLTT is not compatible with classical
> mathematics.

I do not know a proof that MLTT is compatible with ZFC classical set theory.

> You mean because you can't formulate choice?

yes,
I do not know how to interpret Martin-Lof's Exists=Sigma in ZFC by
interpreting Martin-Loef's
propositions into ZFC-propositions, so that Martin-Loef's axiom of choice
gets interpreted in a choice axiom for example

>
> I realize that many people in this list won't be interested in
> foundations. But people who write constructive proofs that computers
> can diggest need them (or, rather, let's say that at least the
> computers definitely need them).

This point you make is very important to Giovanni Sambin and myself.

Our notion of two-level system as explained in

http://www.math.unipd.it/~maietti/papers/MaiettiSambin-rev2.pdf

was born exactly to **formalize constructive proofs**
developed in a language **compatible with that of common mathematical
practice**
(at the extensional level)
**in a trustable intensional type theory*** (at the intensional level)
which can serve as a base for a proof-assistant and from which we can
extract
the desired computational contents (By the way also for us category
theory has been very useful to study the abstract link between the two
levels in joint work with Pino Rosolini).


Many thanks, indeed
Milly

[Martin Escardo]

Dear Milly,

I thought of replying to you privately so as not to polute this list
too much, but I think this, although tangential to this thread, is
important so that people don't have the impression that MLTT is not
compatible with classical mathematics - it definitely is, and so I
will indent it:

----------------------------------------------------------------
MLTT *is* compatible with classical mathematics, including
excluded middle and choice (in the classical meaning of choice).
----------------------------------------------------------------

On 16/05/14 22:59, Maria Emilia Maietti wrote:
>> I am surprised to hear that MLTT is not compatible with classical
>> mathematics.
> I do not know a proof that MLTT is compatible with ZFC classical set
> theory.
>
>> You mean because you can't formulate choice?
>
> yes,
> I do not know how to interpret Martin-Lof's Exists=Sigma in ZFC by
> interpreting Martin-Loef's
> propositions into ZFC-propositions, so that Martin-Loef's axiom of choice
> gets interpreted in a choice axiom for example

Ok, here is how this can be done, as explained in the HoTT book. The
book is about HoTT, of course, but this applies to (its sublanguage)
MLTT.

First, you need to define excluded middle carefully. Let's do it not
carefully first:

Pi X:Type. X + ¬X,

where ¬X = (X -> 0) and 0 is the empty type.

When MLTT is interpreted in ZFC (Pi = cartesian product, Sigma =
disjoint sum, etc.), this *does not* give excluded middle: it gives
*global choice*: it says that there is a (class) function that given
any set X, finds a point of X, or tells you that X is empty. While you
can consider this axiom in classical mathematics (Bourbaki does), it
is not part of ZFC.

The careful formulation is

Pi X:Type. proposition X -> X + ¬X,

where, as in the previous message, 'proposition X' means that the set
X has at most one point (it is a truth value).

This corresponds precisely to ZFC-excluded middle under the standard
interpretation of MLTT in ZFC, as you can easily check.

Now, once you postulate this, rendering yourself classical, you can
show

||X|| = ¬¬X,

where again ||X|| was defined in the previous message (positively, but
under excluded middle the negative formulation works).

Now, it is a fact that in MLTT that the following is (provably) true:

(Pi x:X. Sigma y:Y. A(x,y)) -> (Sigma f:X->Y. Pi x:X. A(x,f(x))).

This is also true in ZF minus excluded middle (in fact, this function
is an isomorphism of sets, with an easily defined inverse).

Now, the axiom of choice is

(Pi x:X. ||Sigma y:Y. A(x,y)||)->||Sigma f:X->Y. Pi x:X. A(x,f(x))||.

While ||-|| cannot be formulated in MLTT (it is a HoTT extension),
under excluded middle as above you can show that ¬¬(-) has the
defining property of ||-||, as discussed above. In any case, even
without this observation, what corresponds to the axiom of choice ZFC
is the existence of a function

(Pi x:X. ¬¬(Sigma y:Y. A(x,y)))->¬¬Sigma f:X->Y. Pi x:X. A(x,f(x)).

So, MLTT *is* compatible with ZFC, and moreover with ZFC+global
choice. As also discussed in the HoTT book, HoTT is compatible with
ZFC too, but *not* with global choice (it violates the univalence
axiom).

>> I realize that many people in this list won't be interested in
>> foundations. But people who write constructive proofs that computers
>> can diggest need them (or, rather, let's say that at least the
>> computers definitely need them).
>
> This point you make is very important to Giovanni Sambin and myself.
>
> Our notion of two-level system as explained in
>
> http://www.math.unipd.it/~maietti/papers/MaiettiSambin-rev2.pdf
>
> was born exactly to **formalize constructive proofs**
> developed in a language **compatible with that of common mathematical
> practice**
> (at the extensional level)
> **in a trustable intensional type theory*** (at the intensional level)
> which can serve as a base for a proof-assistant and from which we can
> extract
> the desired computational contents (By the way also for us category
> theory has been very useful to study the abstract link between the two
> levels in joint work with Pino Rosolini).

The HoTT people have the same aims, and I can see that there are lots
of common ideas and techniques with what you say, as Thorsten already
hinted.

Martin

[Martin Escardo]

This remark is so that I don't sound silly:

On 16/05/14 23:58, Martin Escardo wrote:
> So, MLTT *is* compatible with ZFC, and moreover with ZFC+global
> choice. As also discussed in the HoTT book, HoTT is compatible with
> ZFC too, but *not* with global choice (it violates the univalence
> axiom).

HoTT is compatible with excluded middle and choice, is what I should
have said. Of course, the ZFC model of MLTT is not a model of HoTT.

Martin

[Martin Escardo]

On 16/05/14 23:58, Martin Escardo wrote:

> what corresponds to the axiom of choice ZFC
> is the existence of a function
>
> (Pi x:X. ¬¬(Sigma y:Y. A(x,y)))->¬¬Sigma f:X->Y. Pi x:X. A(x,f(x)).

There is a perhaps more appealing way of seeing this directly: the
axiom of choice in ZFC is equivalent to saying that a product of
non-empty sets is non-empty, which has an immediate expression in
MLTT:

(Pi x:X. ¬¬B(x)) -> ¬¬(Pi x:X. B(x)).

Martin

[Thomas Streicher]

Can't one interpret Minimal Foundations in Extensional Type Theory and
the latter in ZFC (possiby with some Grothendieck universes). Of
course, such a translation validates more than minimal foundations
require. But we are just asking about consistency.

Thomas

[Maria Emilia Maietti]

Dear Martin

many thanks for this discussion which helped me to clarify my issues.
Your discussions on this list are always very fruitful to me.


I certainly agree on what you said below about MLTT (Martin-Loef's
type theory)
if **compatibility= relative consistency**

However in my question (in previous emails) I used the word **compatibility** with a stronger meaning
(to express that intended by Bishop's followers)
namely I say that MLTT satisfies compatibility with classical set theory ZFC if we can show
an interpretation of MLTT into ZFC ***preserving the meaning of propositions and sets.***.

The interpretation of MLTT you described below does not satify this
stronger notion of compatibility
since it translates
Martin-Lof's axiom of choice in a sort of distributivity property between
dependent products and disjoint unions which is not what meant as
''axiom of choice'' in classical mathematics. In fact it can be done in
any Locally cartesian closed category (including those base on ZF or Aczel's CZF)
when MLTT is only the first order fragment.

An interpretation compatible in my sense above with classical ZFC is easier to be achieved

if we drop exists=Sigma and we work in a language where we can represent

''exists x in A B(x)= trivial quotient of Sigma_{x in A} B(x)''

as you also said below.

I just add that this kind of ''exists'' is present also not only in a topos but
also in the **internal type theory of
a locally cartesian pretopos** (where
it entails the axiom of unique choice)

as shown at least in 2005 paper
http://www.math.unipd.it/~maietti/papers/tumscs.pdf
and taken from my 1998 PhD thesis.

Many thanks for your attention

Best wishes
Milly

[Martin Escardo]

Dear Milly,

Thanks for the discussion.

On 18/05/14 20:52, Maria Emilia Maietti wrote:
> many thanks for this discussion which helped me to clarify my issues.
> Your discussions on this list are always very fruitful to me.
>
>
> I certainly agree on what you said below about MLTT (Martin-Loef's
> type theory)
> if **compatibility= relative consistency**

May I venture to say that I had in mind more than just that?

> However in my question (in previous emails) I used the word
> **compatibility** with a stronger meaning
> (to express that intended by Bishop's followers)
> namely I say that MLTT satisfies compatibility with classical set theory
> ZFC if we can show
> an interpretation of MLTT into ZFC ***preserving the meaning of
> propositions and sets.***.

In ZFC, we have propositions (it is a first order theory) and sets.

Define a "truth set" to be a set with at most one element = set
isomorphic to a subsingleton.

Given any proposition P, you get the truth set <P> = {z in 1|P}.
Given a truth set T, you get the proposition [T] that T is inhabited.
This gives a correspondence between propositions and truth sets, such
that two propositions are logically equivalent iff their truth sets
are isomorphic.

(If I wanted to avoid isomorphisms, I would say that a truth set is a
subset of 1. But I prefer not to.)

For any set X, define ||X|| to be the (truth) set ||X|| = {z in 1|X is
inhabited}. (Or the quotient of X by the chaotic equivalence relation
that identifies any two points.)

Then we have, for any truth sets X=<P> and Y=<Q>, where P and Q are
propositions, that the following hold:

[<X> x <Y>] <-> (P and Q).

That is, the cartesian product of <X> and <Y> is inhabited iff P and Q
hold. Similarly,

[|| <X> + <Y> ||] <-> (P or Q).

[sets of functions <X> -> <Y>] <-> (P -> Q)

(That is, there is a function <X> -> <Y> iff P -> Q.)

[set of functions <X> -> 0] <-> ¬P.

(There is a function into the empty set iff P is false.)

If Y(x)=<P(x)> is a family of truth-sets indexed by a set X, then

[product of Y(x)] <-> for all x in X, P(x).
[||disjoint union of Y(x)||] <-> for some x in X, P(x).

The above are theorems in ZFC, not definitions. But they justify the
definitions in MLTT, for "truth types" (types with at most one
element):

P and Q = P x Q
P or Q = ||P + Q||
P -> Q = P -> Q
¬P = P -> 0
forall x:X. P x = Pi x. P x
exists x:X. P x = ||Sigma x:X. P x||

Except that there is no such thing as ||-|| in MLTT. There is in NuPrl
and in HoTT, as discussed previously, but I am not qualified to discuss
NuPrl.

You can, however, define truth-type in MLTT (and hence in HoTT):

truth-type X = Pi x,y:X. x = y.

(Called a proposition or hproposition in HoTT.)

Moreover, under these definitions,

truth-type X -> X + ¬X

corresponds precisely to excluded middle in ZFC, and

Pi X:X. ||Sigma y:Y. A(x,y)|| -> ||Sigma f:X->Y.Pi x:X.A(x,f(x))||

corresponds precisely to the axiom of choice in ZFC.

This is what I had in mind.

Martin

[Martin Escardo]

And I can;t resist making two comments about that, the first of which
is a clarification of why COUNTABLE CHOICE IS PROBLEMATIC in a
constructive setting:

(1) Pi x:X. ||Sigma y:Y. A(x,y)|| -> ||Sigma f:X->Y.Pi x:X.A(x,f(x))||

Now drop the "C" from ZFC, and drop excluded middle too.

When X=N (countable choice), this formulation of choice as a function
(rather than as a logical statement) shows clearly why countable
choice is problematic, just as problematic as general choice. How
would you get a function as described in (1), in general?


(2) Although MLTT doesn't have ||-|| and hence can't say (1), as
remarked in a previous message, it can say

(Pi x:X. ¬¬ B(x)) -> ¬¬ Pi x:X. B(x),

which is equivalent to classical choice in the ZFC interpretation, so
you don't need to extend MLTT with ||-|| to faithfully capture excluded
middle and choice (if you wanted to).

Martin

[Erik Palmgren]

I think your comment "just as problematic as general choice" below (1) may appear a bit misleading.
Yes, there are many models in which countable choice fails just as bad as general choice.
We do have constructive models in which countable choice holds, but we do not have
constructive (and generalized predicative) models in which general choice holds.

Erik

________________________________________
Från: construc...@googlegroups.com [construc...@googlegroups.com] f&#246;r Martin Escardo [m.es...@cs.bham.ac.uk]
Skickat: den 19 maj 2014 00:06
Till: Maria Emilia Maietti; construc...@googlegroups.com
Ämne: Re: Advert & question- on compatibility+ reference on exists

Martin

--

[Martin Escardo]

On 18/05/14 23:30, Erik Palmgren wrote:
>
> I think your comment "just as problematic as general choice" below (1) may appear a bit misleading.
> Yes, there are many models in which countable choice fails just as bad as general choice.
> We do have constructive models in which countable choice holds, but we do not have
> constructive (and generalized predicative) models in which general choice holds.

(I wasn't thinking of models: how do you construct the function (1)
below? If I tell you that X=N, you are not in a better position. Of
course, in the models the situation may be different, as you say.)

Martin

[Peter LeFanu Lumsdaine]

On Sun, May 18, 2014 at 8:52 PM, Maria Emilia Maietti <mai...@math.unipd.it> wrote:

[...] in my question (in previous emails) I used the word **compatibility** with a stronger meaning 

(to express that intended by Bishop's followers)
namely I say that MLTT satisfies compatibility with classical set theory ZFC if we can show
an interpretation of MLTT into ZFC ***preserving the meaning of propositions and sets.***.

The interpretation of MLTT you described below does not satify this stronger notion of compatibility
since it translates Martin-Lof's axiom of choice in a sort of distributivity property between
dependent products and disjoint unions which is not what meant as
''axiom of choice''  in classical mathematics.

 

[...]

 

An interpretation compatible in my sense above with classical ZFC is easier to be achieved if we drop exists=Sigma and we work in a language where we can represent 

  

''exists x in A B(x)= trivial quotient of Sigma_{x in A} B(x)''

 

I think most of the HoTT crowd would absolutely agree with you on this distinction between the two forms of choice!  As you say, the pi-sigma form, which has been called the axiom of choice in the M-L type theory tradition, does not correspond in the set model to the classical axiom of choice.  However, one can also represent in M-L type theory the "exists = triv. quotient of sigma" that you discuss; and the axiom of choice, formulated this way, *does* correspond in the set model (also in the simplicial set model) precisely to the classical axiom of choice.  So (at least on my reading), Martin's assertion:

----------------------------------------------------------------
    MLTT *is* compatible with classical mathematics, including
    excluded middle and choice (in the classical meaning of choice).
----------------------------------------------------------------

 really does hold with the sense of "compatibilty" that you set out.  Indeed, since as I mentioned above all this holds not only in the sets model but also the simplicial sets model, one can strengthen it to:

----------------------------------------------------------------
    HoTT (including univalence and HITs) is compatible

    with classical mathematics, including excluded middle

    and choice (in the classical meaning of choice).
----------------------------------------------------------------

To be careful again: the forms of EM and choice meant here are *not* the + and Sigma forms that are perhaps more often associated with type theory (which do not correspond, in these interpretations, to classical EM and AC) but the "propositional" forms, which correspond precisely in these models to their classical counterparts.

This difference between these and the more traditional type-theoretic forms of EM/AC is discussed and analysed at more length in the HoTT book.

-Peter.

[Martin Escardo]

Just to clarify:

On 19/05/14 00:32, Peter LeFanu Lumsdaine wrote:
> This difference between these and the more traditional type-theoretic
> forms of EM/AC is discussed and analysed at more length in the HoTT book.

I already referred to the HoTT book in previous discussions in this
list in this respect. I take no credit for this.

Martin

[Thomas Streicher]

I misread the problem as interpreting MLTT in Set but you guys speak
of interpreting in ZF as a theory. Let's speak about MLTT without
universes. Then clearly MLTT proves much less \Pi^0_1 sentences than ZFC.
I had such Goedelian thing is mind.

Thomas

[Altenkirch Thorsten]

I agree that countable choice is problematic, however, unlike full choice
it doesn't imply excluded middle (a taboo).

And indeed countable choice can be justified by the setoid interpretation.
Actually we can go further and replace N by any set (in the sense of HoTT)
that can be defined in pure type theory without quotients or HITs.

Thorsten

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

[Altenkirch Thorsten]

From: Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>
Date: Mon, 19 May 2014 00:32:40 +0100
To: Maria Emilia Maietti <mai...@math.unipd.it>
Cc: Martin Escardo <m.es...@cs.bham.ac.uk>, "construc...@googlegroups.com" <construc...@googlegroups.com>
Subject: Re: Advert & question- on compatibility+ reference on exists

To be careful again: the forms of EM and choice meant here are *not* the + and Sigma forms that are perhaps more often associated with type theory (which do not correspond, in these interpretations, to classical EM and AC) but the "propositional" forms, which correspond precisely in these models to their classical counterparts.

I thought in the case of EM it doesn't matter wether you say P \/ not P or P + not P, since the latter is a proposition anyway (assuming that P is)?

T.

[Altenkirch Thorsten]

Even if we assume EM?

Note that this gives us classical powersets since A -> Bool is equivalent
to A -> Prop.

T.

On 19/05/2014 07:41, "Thomas Streicher"

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

[Steve Awodey]

On May 19, 2014, at 12:44 PM, Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk> wrote:

> From: Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>
>> To be careful again: the forms of EM and choice meant here are *not* the + and Sigma forms that are perhaps more often associated with type theory (which do not correspond, in these interpretations, to classical EM and AC) but the "propositional" forms, which correspond precisely in these models to their classical counterparts.
>
> I thought in the case of EM it doesn't matter wether you say P \/ not P or P + not P, since the latter is a proposition anyway (assuming that P is)?
>
> T.

I can’t resist throwing into the mix the odd fact that if EM is formulated as P + not P for *all* types P (not just propositions) then, under the interpretation in sets, it is the (usual) axiom of choice.

Steve

[Martin Escardo]

It is stronger than choice: it is global choice.

Martin

[Altenkirch Thorsten]

I guess by global choice you mean that |X| -> X (knowing that a type is
inhabited gives you an element), while (local ?) choice is equivalent to
(Pi x:A.|B x|) -> |Pi x : A. B x|? Is it clear that these two principles
are different (for provable propositions)?

Thorsten

[Martin Escardo]

On 19/05/14 15:31, Altenkirch Thorsten wrote:
> I guess by global choice you mean that |X| -> X (knowing that a type is
> inhabited gives you an element), while (local ?) choice is equivalent to
> (Pi x:A.|B x|) -> |Pi x : A. B x|? Is it clear that these two principles
> are different (for provable propositions)?

https://en.wikipedia.org/wiki/Axiom_of_global_choice

"In mathematics, specifically in class theories, the axiom of global
choice is a stronger variant of the axiom of choice that applies to
proper classes of sets as well as sets of sets. Informally it states
that one can simultaneously choose an element from every non-empty set."

In the HoTT book, it is shown that global choice (and hence "excluded
middle" in the form forall X:Type.X + 柔, which is equivalent) is
inconsistent with univalance, but that choice is consistent with univalance.

Notice that once you postulate "forall X:Type.X + 柔", we have the ||X||
is equivalent (isomorphic) to the set 洵X.

Martin

[Altenkirch Thorsten]

Just to make the relation between Bool = Prop and Em more precise: It
seems that saying that isTrue : Bool -> Prop is an equivalence is
equivalent to EM : Pi X:Prop. P \/ ~P (Thanks to Paolo Capriotti for
discussing this).

On 19/05/2014 11:47, "Altenkirch Thorsten"

[Thierry Coquand]

Dear all,

Thanks for an interesting discussion.
About

> >What are "exists" and "or" meant to mean, when the CHBHK interpretation
> >is not meant, as in the examples of LLPO and continuity of functions
> N^N->N?
>
> The easy part of my answer is: "exists" and "or" are exactly as in intuitionistic logic (without proof-terms and Curry-Howard). This has always been clear to me since the beginning of my involvement with formal topology in the 80s (it is explicitly said on page 2 of my first paper).

one crucial difference with the approach suggested by the univalent foundation is that this approach introduces
"exists" and "or" that behave like in intuitionistic logic while satisfying the axiom of unique choice. In particular

A or B -> A + B if A and B are incompatible propositions
(exists x:A)P(x) -> (Sigma x:A)P(x) if P(x) is a proposition and P(x)/\P(u) -> Id_A(x,u)

A priori, this seems to fit with mathematical practice where one can give a name to an object if this
object is uniquely determined (but one needs to test this approach on more examples to see if indeed
it gives a better formal representation of mathematical proofs).

Best regards,
Thierry

[Martin Escardo]

On 20/05/14 13:32, Thierry Coquand wrote:
> one crucial difference with the approach suggested by the univalent foundation is that this approach introduces
> "exists" and "or" that behave like in intuitionistic logic while satisfying the axiom of unique choice. In particular
>
> A or B -> A + B if A and B are incompatible propositions
> (exists x:A)P(x) -> (Sigma x:A)P(x) if P(x) is a proposition and P(x)/\P(u) -> Id_A(x,u)
>
> A priori, this seems to fit with mathematical practice where one can give a name to an object if this
> object is uniquely determined (but one needs to test this approach on more examples to see if indeed
> it gives a better formal representation of mathematical proofs).

Good culmination of the discussion.

We discussed the issues of compatibility with classical mathematics,
which is not what I intended originally, but I enjoyed the discussions
and (seemingly opposing) points of view.

Although also not originally intended for this discussion, the
compatibility of Bishop mathematics with Brouwerian hypotheses, if we
adopt the BHK interpretation of logic, is equally problematic, as
discussed in the earlier thread "Brouwer's continuity axioms",

https://groups.google.com/forum/#!topic/constructivenews/x5VqwBX3mRA

Luckily, the same resolution via ||-|| applies. But I see this as more
than just luck (as I am sure others here also do).

Informally, what Thierry expresses above is that the operation ||-||
performs a form of constructive information hiding (better than
e.g. double negation) so that when there is only one answer it gets
disclosed, somewhat like in Sherlock Holmes:

"When you have eliminated the impossible, whatever remains, however
improbable, must be the truth",

although an improvement of this quotation is needed to better
characterize ||-|| verbally in a positive way.

Under classical hypotheses, ||-|| trivializes to double negation. But,
in general, it gives a positive way of "constructively" hiding
information (to the extent that any secret can be kept private), which
is crucial to meaningfully distinguishing Exists from Sigma and Or
from +.

Martin

[Maria Emilia Maietti]

Dear all

in http://www.math.unipd.it/it/news/?id=2142

you find the application form for a one year fellowship in Padova

to work on "Homotopy type theoretic aspects within the Minimalist
Foundation".

Deadline of applications: 8th January 2018

For any kind of information please do not hesitate to contact me.

Best wishes

Maria Emilia Maietti