Report on third version of the submitted thesis

Report on third version of the submitted thesis

“Analysis and Construction of Logical Systems: A Category-Theoretic Approach”, by Micha l

Przyby lek

Jaap van Oosten

Department of Mathematics, Utrecht University June 17, 2016

A very peculiar history is developing around this thesis. When I received the first version, October 2014, I was not well informed about the possible actions a reviewer can take or demand (this is, I admit, also my own fault: I should have inquired). In my country, a reading committee essentially says

‘yes’ or ‘no’ to a thesis (members may, strictly informally and individually, send suggestions to the candidate for improvement of the final version, but this can not influence the decision); rejection is considered to be a serious embarrassment for the supervisor, who therefore makes doubly sure the thesis has an acceptable form before it is sent to the reading committee.

From this point of view, rejection of the thesis would be a serious matter, and I did not wish to spoil the graduation on my own. I therefore wrote a very benevolent, but rather superficial, assessment. When I saw the review by Zawadowski, I understood that the rules in Poland are different; and that by requesting a revision of the thesis, which then is reviewed again, the reading committee acts as an extension of the supervisor.

Therefore, when the revision appeared on May 20, 2015, I decided to give it a more critical look, which resulted in a 5-page review full of detailed comments, which I stressed was ‘far from complete’ (August 24, 2015). I urged a second revision. But now, I had again misunderstood the unwritten rules: I was made to understand that a second revision was very uncommon.

Further developments came to surprise me. The PhD committee decided

to have another expert look at the manuscript, and Professor Bartek Klin

wrote a report (December 29, 2015). I was a bit perplexed at this: of course,

the committee need not uncritically follow the advice of the reviewers, but

if it deems the reviewers incompetent, why doesn’t it dismiss them before seeking advice elsewhere?

Anyway, a discussion went on in Warsaw, in which I could not partici- pate. From Przyby lek’s Report on changes to the dissertation (May 6, 2015) which accompanied the second version, it was apparent how reluctant he was to make any changes, and Klin’s report (which seems heavily influenced by discussions with the candidate) seemed to me to lean toward Przyby lek’s side. I also sensed a certain pressure that the thesis would not be rejected.

I responded to Klin’s report in an e-mail message of January 12, 2016, in which I retracted my recommendation for a second revision, not only be- cause that was such an uncommon thing to do, but also because I expected less and less of a possible rewriting. My comments on the thesis, given in my response to Klin, don’t seem to have been forwarded to the candidate.

The committee decided (January 21, 2016) to have the candidate write a third version.

Well, then. The third version (which I received May 4, 2016) comes accompanied with a “Reply to the comments of the reviewers”, hereafter to be called the Reply. The Reply has a polemical tone and at places sermonizes and patronizes, as if it were my work which stands under scrutiny. It seems the candidate has put more energy into compiling the Reply, than into a thorough revision of the thesis. But let’s start with what we have now.

I begin with the Bibliography, which I had called a ‘disaster’. The Reply says: I have not found any name misspelled (there were some problems with non-ascii letters though). This remark is disingenuous (since he has tacitly corrected B´ eanabou into B´ enabou and Dosen into Doˇ sen), incomprehensible (what are the problems with non-ascii letters?) and incredible (since the bibliography still has entries by ‘Escard’ and ‘Freyd and edrov’). Misspelling however, is not the only thing that is wrong about the bibliography:

Although the effort to alphabetise must be appreciated, we still have Betti preceding B´ enabou, and the anti-alphabetical sequence Burali- Forti, Borceux, Barr. Doˇ sen stands between Day and Day, John- stone between Jacobs and Jacobs, Leinster precedes Lambek, Shulman comes before Sannella, and Streicher is between Street and Street.

Reference [B´ en67]: this appeared in Reports of the Midwest Category Seminar, Lecture Notes in Mathematics 47 (1967), pp. 1-77.

Reference [B´ en00] lacks enough information. I would add: Lecture

Notes of a Course given at TU Darmstadt (2000), electronically avail-

able at: [url ]

Reference [Dub70] gives Lecture notes in mathematics without num- ber, as if it were a book title.

Reference [Ehr63]: there is no publication by Ehresmann with the given title. There are several papers and also a book with the title Cat´ egories et structures but the publication which is meant here is entitled Cat´ egories Structur´ ees.

Reference [ELS04]: Escard should be Escard´ o .

Reference [Fe90]: Freyd and edrov: Freyd and Scedrov. There are no non-ascii symbols needed for Scedrov! Moreover, the title description is idiotic.

Reference [JH06]: has ‘UK’ twice.

Reference [Joh02]: does not mention that this is a two-volume title.

And has the moronic ‘autre tirage’

Reference [Rey83]: this is totally inadequate. I would write In: R.E.A.

Mason (ed), Information Processing 83, North-Holland 1984, pp. 513–

523

Reference [Str99] has ´ ala

Reference [Str10] does not tell us what kind of publication this is, nor where it is available.

References [Woo82] and [Woo85] both have Gomtrie Diffrentielle Cat- goriques.

One wonders: can we trust the mathematics of someone this sloppy?

Let’s then start on the thesis. The front page already has a fresh surprise for us: April 2013 (revised: February 2016). If it was already finished in April 2013, a date the two preceding versions don’t mention, why wait nearly two years before sending it to the reading committee? And if the revision was done February 2016 (which is credible, although only a month after the decision of the PhD committee to request a second revision), why did I not receive it before May 4?

We should answer the question: was the second rewriting a success? Has the text improved to such a degree that we can recommend it to be defended, with a clear conscience? My answer is no; and I am not sure what to say.

Clearly, the thesis has some content, which might warrant a PhD degree

(but due to the writing, to which I come back later, it is next to impossible to state clearly what this content is). Also, it must be appreciated that the author, within his linguistic limitations, has done an effort to expand in some places. But as a piece of mathematical communication, it still falls so short of normal requirements (requirements I demand even for a bachelor thesis in my department) that it is hard to recommend that it proceeds to the defence.

What are the main shortcomings? I see three types:

1) Lack of scientific context and scope of the presented research. A scien- tific text normally makes clear in what field the research takes place.

It will (at least in the case of a PhD thesis) provide an introduction to the field and highlight those results (by others) which are relevant to the author’s work. There is nothing of the sort in this thesis.

2) A style which is so opaque that at places the text is next to incom- prehensible; let me summarise the problems in the triad eerie formu- lations, spooky definitions and ghost theorems. I have given examples before; I will give examples below.

3) Lack of appropriate attribution of results. Look at Example 1.32: the

“discrete reflection” in the category of assemblies is worked out in detail, but it is nowhere indicated that this is not a piece of original research (the result it well-known from Hyland-Robinson-Rosolini and is worked out concretely in my book (Proposition 3.2.19)). This should be mentioned.

Example 1.47 on p. 44 mentions my book but the sentence Let us show that ωSet does not have even countable coproducts on the terminal object again suggests that this is new, although it is in my book:

proposition 3.2.3 does it for the Effective topos, but the reasoning for ωSet is analogous.

Another example is the introduction of Yoneda triangles in Chapter 2, where mention of the work of Weber and Street/Walters is only made as an afterthought.

I shall give a number of examples to illustrate point 2). These are mainly from the first part of the thesis; I hope the Warsaw PhD committee can appreciate, from these examples, the considerable effort it takes to get even this far.

The Abstract starts by stating the aim of the thesis: to develop categor-

ical foundations for studying lambda calculi [. . . ]. The naive reader wonders

here, why the study of finite things such as lambda calculi needs a founda- tion. Further in the Abstract there is still the formulation of Peter Freyd’s theorem that there are no sufficiently (co)complete non-posetal categories.

Despite the reasoning in the Reply, I think this confounds the reader (es- pecially if he is acquainted with that theorem). We also find the word

“analogical” there, but that might be a pun.

The Introduction is a good example of how one can obfuscate even simple things. Basically this is about the fact that a logic has a semantics as well as a proof system. In Example 0.1, a signature Σ

is introduced, and now we have a Boolean algebra over Σ

. I commented on this in my second review; this was ignored.

Just after Example 0.2 we read In the above example logical connectives were defined internally to the logic – i.e. were defined inductively over the syntax. . . The logical connectives (i.e., ∧, ∨, ⇒) defined inductively?? By induction on what?

Example 0.3 talks about the smallest (posetal) category having as ob- jects elements from the carrier of the syntactic algebra Prop [. . . ] and arrows generated by the following rules:. The second version had here, in paren- thesis, “deductive system” instead of “posetal”. Since it is unclear both in what sense “smallest” has to be taken, and in what way the given “rules”

“generate”, this led to a confused comment from me. But if you mean: the Lindenbaum algebra of propositional logic, why don’t you say so? Again, just after this Example, we read that the connectives in the above example were defined by the generating rules of deductions; well this is impossible to interpret because each rule refers to connectives, so the connectives precede the rules.

In Example 0.4 we have Sen, but just after, we have |Sen|, without explanation. A paragraph later we have a posetal category Sen satisfying compatibility condition. I don’t have any idea how to read this.

Chapter 1. Here we find a spooky definition: Definition 1.4.

Definition 1.4 (Discreteness). Let W

C

F

oo

be an adjunction between categories W and C with F left adjoint to U . This adjunction gives a notion of discreteness on category W if the unit of the adjunction is an isomor- phism.

So, after reading this definition, do you know what a “notion of discrete- ness” is?

The first sentence of p. 13 should have full coreflective subcategory.

Generally, the Examples in this chapter have spooky captions, which

might be called “anti-descriptive”: the systematically put the reader on the

wrong foot. Example 1.15 has the caption Failure of naive cartesian closed- ness, but is actually an example where naive cartesian closedness holds.

Definition 1.16 has the caption Internally cartesian closed connectives, but no connectives are mentioned.

The misprint adopt it, just above Definition 1.16, is quite annoying; it should be adapt it, I suppose.

Example 1.23 has the underlying locale of its open subsets is continuous.

I had commented on this, suggesting is a continuous lattice instead; but this was ignored.

On p. 28, l. -13, we still find “indexes”; my comment went ignored.

The same with the caption Ad hoc polymorphism for Definition 1.31.

On p. 33, after the rules for second-order λ-calculus, he has, on my recommendation, expanded the comment the usual conversions of lambda calculus apply by giving some rules. However, the notation suggests that instead of conversion rules we have a symmetric relation. Was this intended?

On p. 41, ll. 15–16 we read On the other hand, the result of Freyd carries to any cocomplete topos as we show below in Theorem 1.41 (also see: Corollary 1.45). He has chosen to disregard my comment that “carries”

should be “carries over”, but this is, in my view, a good example of a ghost theorem: when I look up Theorem 1.41, I don’t see the formulation of Freyd’s result or the stated generalization (I do see, however, an additional requirement: locally small), nor is it immediately apparent from Corollary 1.45. If this is a major result of the thesis, mentioned both in the abstract and in the Reply, why not work it out beyond all possible doubt?

I stop here with my examples. There is, moreover, an abundance of typos and linguistic errors in the text. There is such a haughty disdain for clarity and accuracy here that it comes to utter disrespect for the reader. It is a mystery to me how a paper based on this thesis got accepted by JPAA; I can only declare that I was not the referee.

I am fully aware that my comments will be regarded as trivial nit-picking by both the candidate and his supervisor. The supervisor, Prof. Andrzej Tarlecki, wrote in an assessment to the PhD committee: Neither the author nor me wanted a mathematically fully precise but dry presentation in the purely ”definition-theorem-proof” style. Which means he has supported his student in his bad habits, thereby doing him a great disservice.

Moreover Prof. Tarlecki wrote: I believe though that in all the indicated

cases this is a matter that can be easily rectified, albeit sometimes at a

considerable expense of space and effort if a fully precise statement was to

be given. “This” being sloppiness as remarked on in my second review.

Well, to judge from the present version the rectification wasn’t that “easy”.

Moreover, stating complicated things precisely, and if necessary spending lots of time to think about formulations which ease the burden on the reader (instead of confusing him) – that is the job of mathematicians.

When I worked on my PhD, my supervisor Prof. Troelstra systematically

returned everything I gave him to read, with elaborate comments on style,

punctuation, and the like; things I thought “trivial” at the time. But in the

end, I profited a great deal from this.