Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and is 28 pages long. The other is entitled "How to compile mathematics into Algol", deals with implementation of his constructive type theory, and is 29 pages long. Both pdfs can be found here.

Numerous intriguing questions arise in connection with these articles, such as the following:

Question 1. What is the precise date of composition of the articles?

Question 2. Why weren't the articles published?

Question 3. What led Bishop to develop a constructive type theory, given what is often considered to be his lack of interest in formal logic and formalisation of constructive mathematics? (see Note 1 below).

Question 4. Should our perceived views of Bishop's foundational stance be reconsidered in light of these manuscripts?

Question 5. Since the manuscript "A general language" and Bishop's 1970 published article "Mathematics as a numerical language" are very different, could somebody summarize the similarities and differences between the two?

Note 1. For example, one finds the following comment by a selfdeclared constructivist:

the constructive mathematician dismisses classical mathematics as an exercise in formal logic (see Richman, Fred. Interview with a constructive mathematician. Modern Logic 6 (1996), no. 3, 247-271).

This is not an indication of great esteem for formal logic on the part of this particular constructivist.

Note 2. It must be said that Bishop himself was not averse to making statements of this sort:

It is not surprising that some of Brouwer's precepts were then formalized, giving rise to so-called intuitionistic number theory, and that the formal system so obtained turned out not to be of any constructive value. In fairness to Brouwer it should be said that he did not associate himself with these efforts to formalize reality; it is the fault of the logicians that many mathematicians who think they know something of the constructive point of view have in mind a dinky formal system or, just as bad, confuse constructivism with recursive function theory. (page 4 in "A constructivist manifesto", chapter 1 in Bishop, Errett. Foundations of constructive analysis. McGraw-Hill Book Co., New York-Toronto, Ont.-London 1967)

  • $\begingroup$ I like questions 1,2,5. For question 3, I would just say “What led Bishop to develop a constructive type theory?”, without referring to what is often considered. For question 4, I wouldn’t assume that “our” views of Bishop are all the same, so if you think some particular view may be in need of reconsideration, it would help to link to it. $\endgroup$ – Matt F. May 7 '18 at 16:57
  • $\begingroup$ OK, I added a comment to source this. @MattF. $\endgroup$ – Mikhail Katz May 8 '18 at 9:30
  • $\begingroup$ The “Interview With a Constructive Mathematician” is Richman’s explanation of his own view, explicitly not Bishop’s view, and frequently pointing out disagreements with Bishop. I don’t think it helps with the texts here, so I will give up on nudging this towards a better historical question. $\endgroup$ – Matt F. May 8 '18 at 12:39
  • $\begingroup$ This was precisely my point, as I think I made clear in the question: Bishop's views of constructivism are not necessarily those that have been pursued by his students, e.g., in the context of attitude toward type theory. Feel free to refrain from nudging, though. @MattF. $\endgroup$ – Mikhail Katz May 8 '18 at 12:54

Re (1): in this presentation by Iosif Petrakis the manuscripts are dated 1969(?). There is a 1970 published article from a 1968 conference with a similar topic as the unpublished "Compiling Mathematics into Algol". Erik Palmgren (arXiv:1201.6272) refers to this latter work as "Unpublished text for a seminar – 1970."

Re (2): from this comment by Bas Spitters I understand that it was Bishop's decision not to publish these manuscripts.

Re (3): Petrakis explains that it was Bishops intention to implement his framework for constructive mathematics into some computer language. For that purpose it was unavoidable that he could describe the algorithms with enough precision to be intelligible to machines, hence his interest in the formalisation of constructive mathematics. A quote from Bishop's Algol paper: "Formal constructive mathematics is concerned with the communication of algorithms with enough precision to be intelligible to machines".

  • $\begingroup$ The 1970 published article is entitled "Mathematics as a Numerical Language" but I don't think it deals with type theory. $\endgroup$ – Mikhail Katz May 7 '18 at 12:41
  • 1
    $\begingroup$ I cannot read that conference paper (paywall), but I understand it does address how to program constructive mathematics in Algol, and so it must address the formalisation of constructive mathematics. $\endgroup$ – Carlo Beenakker May 7 '18 at 12:43
  • $\begingroup$ @Carlo it does make some comments about programming languages, but not extensively. $\endgroup$ – David Roberts May 7 '18 at 23:33

Regarding Question (2), I have heard the following story from (non-constructivist) people who knew E. Bishop well:

Bishop had submitted (some of) these papers for publication, but they were not accepted in their then form. The reasons (as pointed out by either the editor or referees) was that other people had been working on similar topics with better/similar results. Bishop then set about improving his own papers/results, trying to formulate (what we now call) explicit type constructors everywhere. Unfortunately, Bishop died before he could finish this endeavour.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.