% (find-LATEX "2020gaina-kowalski.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020gaina-kowalski.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020gaina-kowalski.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020gaina-kowalski.pdf"))
% (defun e () (interactive) (find-LATEX "2020gaina-kowalski.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020gaina-kowalski"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020gaina-kowalski.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020gaina-kowalski.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020gaina-kowalski.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020gaina-kowalski.pdf
%               file:///tmp/2020gaina-kowalski.pdf
%           file:///tmp/pen/2020gaina-kowalski.pdf
% http://angg.twu.net/LATEX/2020gaina-kowalski.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb}                 % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
\begin{document}

% (find-books "__cats/__cats.el" "gaina-kowalski")
% (find-symbolspage 20)


Referee report on: 

``Fra\"isse-Hintikka Theorem in institutions'', by

Daniel G\u{a}in\u{a} and Tomasz Kowalski

\bigskip

Let me start by confessing that I am not a specialist in institutions.
When the editors asked me if I could be a referee for this paper I
accepted because 1) I had been planning to learn instituions since a
long time, and 2) because after a quick glance I got the impression
that this paper could be very interesting. I wouldn't be able to judge
how novel it is, but I decided to compensate that by reading it with a
lot of attention and checking all the details that I could.

I found this paper far more interesting that I expected ---
fascinating, even. It is extremely well-written and practically
self-contained; I knew some Categorical Semantics (mostly along the
lines of, e.g., Bart Jacobs's book ``Categorical Logic and Type
Theory'') and I was able to read the paper by just complementing that
with the first three chapters of Razvan Diaconescu's book
``Institution-Independent Model Theory''. After the two first sections
the paper go straight to some very non-trivial (to me, of course!)
uses of institutions, with a way of defining quantification that I had
never seen before, and then it defines certain games on top of that.
It's beautiful stuff; for many people this kind of beauty and elegance
is not enough, and the paper handles this by pointing in the
introduction to several places where important applications of these
games can be found.

I was only able to spot two typos in the paper: a trivial one in the
abstract, in which ``Fraïssé'' is written with ``Sc'' instead of
``ss'', and in page 5, in the grammar that defines sentences, I think
that the ``for all'' at the right should be an ``exists''.

There are two places in which I felt that the paper is not clear
enough and it should be possible to fix this with small changes. The
first one is in page 4: ``Note that, unlike the single-sorted case,
the reduct functor modifies the universes of models''... for me it is
obvious that every change of signature changes the domain of discourse
of the sentences in some way, but the text says that the ``universe''
of a model is a set of sets, one for each sort, and this didn't make
much sense to me; and this paragraph ends with ``Otherwise, the notion
of reduct is standard''... does this ``standard'' mean ``standard in
Model Theory'', because in (traditional?) Model Theory
single-sortedness is the default?

The second place in which I felt that the text could be clearer is in
section 3.2. I had to struggle too much to understand what the
signatures $\Sigma[X]$, $\Sigma_1[X]$, etc, and the pushouts ``mean'',
and I think that the next readers will find the text much easier to
read if the authors add a few sentences explaining that in the case we
are interested in we are just choosing a set of variables X and adding
the same set of variables (modulo some adjustments for technical
reasons) to the signatures $\Sigma$, $\Sigma_1$, and $\Sigma_2$; also,
it would be nice to point to places in the literature in which
quantification spaces are used in less trivial ways, and in which the
pushoutness of the squares in Figure 1 is really important. I guess
that the reference [9], i.e., Diaconescu's paper ``Quasi-varieties and
initial semantics for hybridized institutions'', has all this, but I
didn't occur to me to download it and look at it until today (and I
feel stupid in retrospect)...

My overall impression is that this is an excellent paper, and I really
hope that the other referees agree with me, and that it gets accepted
and published.









\end{document}




% Local Variables:
% coding: utf-8-unix
% ee-tla: "NONE"
% End: