Let $f : (X',\sigma') \rightarrow (X,\sigma)$ a ramified Real cover, unramified over $X \setminus B$. Suppose that its ramification profile $\bm{\lambda}_i$ around $b_i^\pm$ is even for all $i$. Then
\begin{equation}
\varepsilon \rho_f(a) = \varepsilon \rho_{f_0}(a_0) \ldots \varepsilon \rho_{f_g}(a_g)
\end{equation}
where $a,a_0,\ldots,a_g$ are any admissible classes and $f_i$ is the degeneration of $f$ over $(X_i,\sigma_i,B_i)$.

Denote also by $f_D$ the degeneration of $f$ over the doublet $(D,\sigma_D,C_D)$. The diagram
\begin{equation}
\begin{tikzcd}
H_1(Y_\sigma^o) \ar[rr,"i_*"] \ar[dr] & & H_1(X_\sigma^o) \ar[dl] \\
& \{ \pm 1 \} &
\end{tikzcd}
\end{equation}
commutes, where the diagonal arrows are $\varepsilon \rho_{f_D}\varepsilon \rho_{f_0} \ldots \varepsilon \rho_{f_g}$ and $\varepsilon \rho_f$. Choosing admissible classes as in the statement and denoting by $a'$ the puncture class of $(Y',\sigma,C')$, we can use Lemma <ref> to obtain
\begin{equation}
\varepsilon \rho_f(a) = \varepsilon \rho_{f_D}(a')\varepsilon \rho_{f_0}(a_0) \ldots \varepsilon \rho_{f_g}(a_g).
\end{equation}
Indeed, the degenerations involved are of type (a),(b) and the left-hand side does not depend on the admissible class $a$.

We claim that the ramification profiles of $f_D$ are all even. For those that correspond to the points in $B$, it is part of the assumptions of the corollary. The others correspond to collapsed circles. The monodromy around them is the same as the monodromy around the only pair of marked points of one of the $(X_i,\sigma_i,B_i)$. Those have been classified in Example <ref>, and they are all even.

As a consequence, the function $\varepsilon \rho_{f_D}$ is constant equal to $1$. This proves the statement.

Let $(X,\sigma,B)$ be a marked connected Real Riemann surface and $f : (X',\sigma') \rightarrow (X,\sigma)$ a ramified Real cover, unramified over $X \setminus B$. Suppose that the ramification $\bm{\lambda}_i$ around $b_i^\pm$ is even for all $i$. Then the sign associated to $f$ in <cit.> is $\varepsilon \rho_f (a)$ for any admissible class $a$.

Through the degeneration of Corollary <ref>, the signs of <cit.> enjoy the same product formula, see <cit.>. Therefore, it is enough to compare them over the connected Real Riemann surface $(\mathbb{P}^1_\mathbb{C},\sigma,B)$ of Example <ref>. Both signs transform disjoint unions of covers into product of signs, so that it is enough to check that the signs match if the source is either a doublet or a connected Real Riemann surface. Those are classified in Example <ref>. With the signs of <cit.>, the cover by a doublet (corresponding to the partition $(d,d)$ of $2d$) is counted negatively while the cover by a $(\mathbb{P}^1_\mathbb{C},\sigma)$ (corresponding to the partition $(d)$ of $d$ with odd $d$) is counted positively. This is exactly what we have computed in Example <ref>.

§ EXTENSION TO NON-EMPTY FIXED LOCUS

In <cit.>, the signed Real Hurwitz numbers are defined from Real Gromov-Witten theory using a target which may have a non-empty fixed locus. It turns out that the signed count of ramified Real covers of a connected Real Riemann surface does not depend on the structure of its fixed locus. In Subsection <ref>, we have provided a topological definition of the sign when the fixed locus of the target is empty. The purpose of the present section is to define signs when the fixed locus of the target is not empty, with the constraint that the signed weighted sum over ramified Real covers is still the signed Real Hurwitz numbers of Section <ref>. As in <cit.>, we restrict to the case of covers unramified over the fixed locus, which means that we consider marked connected Real Riemann surfaces $(X,\sigma,B)$ with $X^\sigma \cap B = \emptyset$. A case with Real branch points is studied in <cit.>.

§.§ $\mathbb{P}^1_\mathbb{C}$ with a pair of conjugate points

In this subsection, we focus on the target $\mathbb{P}^1_\mathbb{C}$ with the involution
\begin{equation}
\tilde{\theta} : [x:y] \mapsto [\overline{y}: \overline{x} ]
\end{equation}
and the marked points $B_{\mathbb{P}^1_\mathbb{C}} = \{[0:1],[1:0]\}$. The fixed locus is the circle
\begin{equation}
\{ [x:y ] \ | \ |x| = |y | \}.
\end{equation}
Classification of ramified Real covers $f : (X',\sigma') \rightarrow (\mathbb{P}^{1}_\mathbb{C},\tilde{\theta})$ unramified over $\mathbb{P}^1_\mathbb{C} \setminus B_{\mathbb{P}^1_\mathbb{C}}$, with $(X',\sigma')$ either a connected Real Riemann surface or a doublet, is described in Example <ref>.

* The cover obtained by doubling $[x:y] \mapsto [x^d:y^d]$ accounts for the partition $\lambda = (d,d)$ of $2d$. Its automorphism group has cardinality $2d$. It is counted with a sign $-1$ in <cit.>.

* The cover
\begin{equation}
f : \left\{ \begin{array}{lll}
(\mathbb{P}^1_\mathbb{C},\tilde{\theta}) & \rightarrow & (\mathbb{P}^1_\mathbb{C},\tilde{\theta})\\ \relax
[x:y] & \mapsto & [x^d:y^d]
\end{array} \right.
\end{equation}
accounts for the partition $(d)$ of $d$. Its automorphism group has cardinality $d$. It is counted with a sign $+1$ in <cit.>.

* The cover
\begin{equation}
f : \left\{ \begin{array}{lll}
(\mathbb{P}^1_\mathbb{C},{\theta}) & \rightarrow & (\mathbb{P}^1_\mathbb{C},\tilde{\theta})\\ \relax
[x:y] & \mapsto & [x^d:y^d]
\end{array} \right.
\end{equation}
for $d$ even accounts for the partition $(d)$ of $d$, where the involution $\theta$ is as in Example <ref>. Its automorphism group has cardinality $d$. It is counted with a sign $-1$ in <cit.>.
With this choice of signs, we do recover that
\begin{equation}
\mathbb{R}H_{0,d}(\lambda) = \left\{ \begin{array}{ll}
1 / d & \text{ if } \lambda =  (d) \text{ with } d \text{ odd,} \\
-1/2d' & \text{ if } \lambda =  (d',d') \text{ with } d = 2d',\\
0 & \text{ otherwise.}
\end{array} \right.
\end{equation}

[scale = 0.7]
(6) at (-0.5, 0) ;
(7) at (0.5, 0) ;
(8) at (0, 1) $\bullet$;
(9) at (0, -1) $\bullet$;
(10) at (2, 0) ;
(11) at (3, 0) ;
(12) at (2.5, 1) $\bullet$;
(13) at (2.5, -1) $\bullet$;
(14) at (2, 4) ;
(15) at (3, 4) ;
(16) at (2.5, 5) ;
(17) at (2.5, 3) ;
(18) at (-5, 4) ;
(19) at (-4, 4) ;
(20) at (-4.5, 5) ;
(21) at (-4.5, 3) ;
(22) at (-3, 4) ;
(23) at (-2, 4) ;
(24) at (-2.5, 5) ;
(25) at (-2.5, 3) ;
(26) at (-4, 0) ;
(27) at (-3, 0) ;
(28) at (-3.5, 1) $\bullet$;
(29) at (-3.5, -1) $\bullet$;
(30) at (-0.5, 4) ;
(31) at (0.5, 4) ;
(32) at (0, 5) ;
(33) at (0, 3) ;
(34) at (-0.5, 0) ;
(35) at (0.5, 0) ;
(36) at (-0.25, 0.25) ;
(37) at (0.25, 0.25) ;
(38) at (-0.25, -0.25) ;
(39) at (0.25, -0.25) ;
(40) at (2, 0) ;
(41) at (3, 0) ;
(42) at (2.25, 0.25) ;
(43) at (2.75, 0.25) ;
(44) at (2.25, -0.25) ;
(45) at (2.75, -0.25) ;
(46) at (-4, 0) ;
(47) at (-3, 0) ;
(48) at (-3.75, 0.25) ;
(49) at (-3.25, 0.25) ;
(50) at (-3.75, -0.25) ;
(51) at (-3.25, -0.25) ;
(52) at (-0.5, 4) ;
(53) at (0.5, 4) ;
(54) at (-0.25, 4.25) ;
(55) at (0.25, 4.25) ;
(56) at (-0.25, 3.75) ;
(57) at (0.25, 3.75) ;
(58) at (2, 4) ;
(59) at (3, 4) ;
(60) at (2.25, 4.25) ;
(61) at (2.75, 4.25) ;
(62) at (2.25, 3.75) ;
(63) at (2.75, 3.75) ;
(64) at (-3.5, 2.25) ;
(65) at (-3.5, 1.75) ;
(66) at (2.5, 2.25) ;
(67) at (2.5, 1.75) ;
(68) at (0, 2.25) ;
(69) at (0, 1.75) ;
(70) at (-4.5, 5) $\bullet$;
(71) at (-4.5, 3) $\bullet$;
(72) at (-2.5, 5) $\bullet$;
(73) at (-2.5, 3) $\bullet$;
(74) at (0, 5) $\bullet$;
(75) at (0, 3) $\bullet$;
(76) at (2.5, 5) $\bullet$;
(77) at (2.5, 3) $\bullet$;
(78) at (-3.5, 1) ;
(79) at (-3.5, -1) ;
(80) at (0, 1) ;
(81) at (0, -1) ;
(82) at (2.5, 1) ;
(83) at (2.5, -1) ;
[in=180, out=90] (6.center) to (8.center);
[in=90, out=0] (8.center) to (7.center);
[in=0, out=-90] (7.center) to (9.center);
[in=180, out=-90] (6.center) to (9.center);
[in=180, out=90] (10.center) to (12.center);
[in=90, out=0] (12.center) to (11.center);
[in=0, out=-90] (11.center) to (13.center);
[in=180, out=-90] (10.center) to (13.center);
[in=180, out=90] (14.center) to (16.center);
[in=90, out=0] (16.center) to (15.center);
[in=0, out=-90] (15.center) to (17.center);
[in=180, out=-90] (14.center) to (17.center);
[in=180, out=90] (18.center) to (20.center);
[in=90, out=0] (20.center) to (19.center);
[in=0, out=-90] (19.center) to (21.center);
[in=180, out=-90] (18.center) to (21.center);
[in=180, out=90] (22.center) to (24.center);
[in=90, out=0] (24.center) to (23.center);
[in=0, out=-90] (23.center) to (25.center);
[in=180, out=-90] (22.center) to (25.center);
[in=180, out=90] (26.center) to (28.center);
[in=90, out=0] (28.center) to (27.center);
[in=0, out=-90] (27.center) to (29.center);
[in=180, out=-90] (26.center) to (29.center);
[in=180, out=90] (30.center) to (32.center);
[in=90, out=0] (32.center) to (31.center);
[in=0, out=-90] (31.center) to (33.center);
[in=180, out=-90] (30.center) to (33.center);
[bend left=15, looseness=1.25, dashed, very thick] (34.center) to (36.center);
[bend left=15, looseness=0.75, dashed, very thick] (36.center) to (37.center);
[bend left=15, looseness=1.25, dashed, very thick] (37.center) to (35.center);
[bend left=15, looseness=1.25, very thick] (35.center) to (39.center);
[bend left=15, looseness=0.75, very thick] (39.center) to (38.center);
[bend left=15, looseness=1.25, very thick] (38.center) to (34.center);
[bend left=15, looseness=1.25, dashed, very thick] (40.center) to (42.center);
[bend left=15, looseness=0.75, dashed, very thick] (42.center) to (43.center);
[bend left=15, looseness=1.25, dashed, very thick] (43.center) to (41.center);
[bend left=15, looseness=1.25, very thick] (41.center) to (45.center);
[bend left=15, looseness=0.75, very thick] (45.center) to (44.center);
[bend left=15, looseness=1.25, very thick] (44.center) to (40.center);
[bend left=15, looseness=1.25, dashed, very thick] (46.center) to (48.center);
[bend left=15, looseness=0.75, dashed, very thick] (48.center) to (49.center);
[bend left=15, looseness=1.25, dashed, very thick] (49.center) to (47.center);
[bend left=15, looseness=1.25, very thick] (47.center) to (51.center);
[bend left=15, looseness=0.75, very thick] (51.center) to (50.center);
[bend left=15, looseness=1.25, very thick] (50.center) to (46.center);
[bend left=15, looseness=1.25, dashed, very thick] (52.center) to (54.center);
[bend left=15, looseness=0.75, dashed, very thick] (54.center) to (55.center);
[bend left=15, looseness=1.25, dashed, very thick] (55.center) to (53.center);
[bend left=15, looseness=1.25, very thick] (53.center) to (57.center);
[bend left=15, looseness=0.75, very thick] (57.center) to (56.center);
[bend left=15, looseness=1.25, very thick] (56.center) to (52.center);
[bend left=15, looseness=1.25, dashed] (58.center) to (60.center);
[bend left=15, looseness=0.75, dashed] (60.center) to (61.center);
[bend left=15, looseness=1.25, dashed] (61.center) to (59.center);
[bend left=15, looseness=1.25] (59.center) to (63.center);
[bend left=15, looseness=0.75] (63.center) to (62.center);
[bend left=15, looseness=1.25] (62.center) to (58.center);
(60.center) to (63.center);
(62.center) to (61.center);
[->] (64.center) to (65.center);
[->] (66.center) to (67.center);
[->] (68.center) to (69.center);

We take the signs of <cit.> as a definition in those cases. By declaring that the sign of a disjoint union of covers is the product of each of their signs, it fixes the sign of any ramified Real cover $f : (X',\sigma') \rightarrow (\mathbb{P}^{1}_\mathbb{C},\tilde{\theta})$ unramified over $\mathbb{P}^1_\mathbb{C} \setminus B_{\mathbb{P}^1_\mathbb{C}}$.

We shall describe those signs in terms of of the monodromy data of the ramified Real covers. Choose a base point $p$ in the fixed locus. Given a ramified Real cover $f : (X',\sigma') \rightarrow (\mathbb{P}^{1}_\mathbb{C},\tilde{\theta})$ unramified over $\mathbb{P}^1_\mathbb{C} \setminus B_{\mathbb{P}^1_\mathbb{C}}$, we have a permutation $\epsilon$ of the fiber, of cycle type $\lambda$, by considering a loop around the fixed locus, and an involution $\tau$ of the fiber by considering the restriction of $\sigma'$. They satisfy
\begin{equation}
\epsilon \tau = \tau \epsilon.
\end{equation}
To such a pair, we associate the following numbers :

* Since $\epsilon$ and $\tau$ commute, $\tau$ preserves by conjugation the set $\mathcal{C}_i$ of $i$-cycles in $\epsilon$. Denote by $\tau_i$ the involution of $\mathcal{C}_i$ obtained and $m_i = \# \mathcal{C}_i$.

* $\tau_i$ being an involution, it has cycle type $(2,\ldots,2,1,\ldots,1)$. Denote by $k_i$ the number of $2$ appearing, so that the conjugation by $\tau$ preserves $m_i - 2k_i$ $i$-cycles of $\epsilon$.

* For each cycle $c$ fixed by $\tau$, we can consider the restriction of $\tau$ on it. If $i$ is odd, it must  be the identity, but if $i= 2j$, it might be the identity or $c^j$. Denote by $a_i$ the number of those $i$-cycles on which $\tau$ is the identity, and $b_i = m_i - 2k_i - a_i$.
As the proof of Lemma <ref> shows, $\sum_i k_i$ and $\sum_j b_{2j}$ correspond respectively to the number of doublets and of $(\mathbb{P}^{1}_\mathbb{C},\theta)$ in the source.

The sign of $f$ is
\begin{equation}
s(f) = (-1)^{\sum_{i=1}^\infty k_i + \sum_{j=1}^\infty b_{2j}}.
\label{equationFormulaSignRealLocus}
\end{equation}

The formula (<ref>) behaves well under disjoint unions of covers. Indeed, we have
\begin{equation}
s(f \sqcup f') = s(f) s(f').
\end{equation}
Since we have defined the signs to satisfy this formula, it is enough to prove that $s(f)$ is the required sign in the three cases of Example <ref>.

* If the source is a doublet, we can label the fiber as $\{ 1_+,1_-,\ldots,d'_+,d'_- \}$ such that
\begin{equation}
\tau = (1_+ \ \ 1_-) \ldots (d'_+ \ \ d'_-) \text{ and } \epsilon = (1_+ \ \ \ldots \ \ d'_+)(1_- \ \ \ldots \ \ d'_-).
\end{equation}
The only non-vanishing number is $k_{d'} = 1$, thus $s(f) = -1$.

* If the source is $(\mathbb{P}^{1}_\mathbb{C},\tilde{\theta})$, we label the fiber so that
\begin{equation}
\tau = id \text{ and } \epsilon = (1 \ \ \ldots \ \ d ).
\end{equation}
The only non-vanishing number is $a_d = 1$, and $s(f) = 1$.

* Finally, if the source is $(\mathbb{P}^{1}_\mathbb{C},{\theta})$ and the degree $d = 2d'$ is even, we label the fiber so that
\begin{equation}
\tau = (1 \ \ d'+1) \ldots (d',2d) \text{ and } \epsilon = (1 \ \ \ldots \ \ d ).
\end{equation}
The only non-vanishing number is $b_d = 1$, and $s(f) = -1$.
The lemma is proved.

Note that even though there exists ramified Real covers corresponding to the partition $(d)$ with $d$ even, the signed Real Hurwitz number $\mathbb{R}H_{0,d}((d))$ with $d$ even vanishes.

Not all the ramified Real covers described in Example <ref> truly contribute to the signed Real Hurwitz numbers. Indeed, the number
\begin{equation}
\mathbb{R}H_{0,d}((d))
\end{equation}
vanishes for $d$ even although there are two isomorphism classes of ramified Real covers of $(\mathbb{P}^1_\mathbb{C},\tilde{\theta})$ corresponding to the partition $(d)$. However, the signs are such that these isomorphism classes cancel each other. Thus, we say that a ramified Real cover of $(\mathbb{P}^1_\mathbb{C},\tilde{\theta},B_{\mathbb{P}^1_\mathbb{C}})$ is said to be contributing if

* it is isomorphic to the cover described in Example <ref> for the partition $(d)$ with $d$ odd or $(d,d)$,

* or it is a disjoint union of contributing ramified Real covers.
One can restrict the counts to the contributing ramified Real covers of $(\mathbb{P}^1_\mathbb{C},\tilde{\theta},B_{\mathbb{P}^1_\mathbb{C}})$ without changing the value of the signed sums. The partitions of $d$ corresponding to the ramification profile of a ramified Real cover are necessarily even. The notion of contributing cover is used in Subsection <ref>.

§.§ General case

Let $(X,\sigma,B)$ be a marked connected Real Riemann surface, of genus $g$, whose real locus $X^\sigma$ is non-empty. It admits a canonical degeneration obtained as follows. For each fixed circle $S$, choose a pair of conjugated circles homotopic to $S$ in $X^o$. Degenerating these pairs of conjugated circles leads to the union of copies of $(\mathbb{P}^1_\mathbb{C},\tilde{\theta},B_{\mathbb{P}^1_\mathbb{C}})$ as in Subsection <ref> and a marked Real Riemann surface $(X',\sigma',B')$ with empty real locus. The latter can be either a doublet or a connected Real Riemann surface.

During the degeneration process, pairs of conjugated marked points are created and need to be ordered. For the rest of the subsection, we choose an ordering of those points without placing any constraint on it. If $(X',\sigma')$ is a doublet, it leads to a puncture class $a$. If $(X',\sigma')$ is a connected Real Riemann surface, we choose an admissible class $a$ for the rest of the subsection. The definitions will essentially not depend on the ordering of the marked point created during the degeneration or on the admissible class.

Let $f$ be a ramified Real cover of $(X,\sigma)$ unramified over $X \setminus B$. It degenerates canonically to give a ramified Real cover of $(X',\sigma',B')$ unramified over $X' \setminus B'$ and for each fixed circle $S$ in $X$ a ramified Real cover $f_S$ of $(\mathbb{P}^1_\mathbb{C},\tilde{\theta},B_{\mathbb{P}^1_\mathbb{C}})$ as in Subsection <ref>. We define the sign of $f$ to be
\begin{equation}
s(f) = \varepsilon \rho_{f'}(a) \prod_{S} s(f_S).
\label{equationSignGeneral}
\end{equation}

Let $(X,\sigma,B)$ be as above and $\bm{\lambda} = (\bm{\lambda}_1,\ldots,\bm{\lambda}_n)$ a sequence of partitions of an integer $d$. The sum
\begin{equation}
\sum_{[f]} \frac{s(f)}{\# Aut(f)}
\end{equation}
over the isomorphism classes of ramified Real covers of $(X,\sigma)$ unramified over $X \setminus B$ with ramification profile $\bm{\lambda}$ equals
\begin{equation}
\mathbb{R}H^\bullet_{g,d} (\bm{\lambda})
\end{equation}

defined by replacing $\sigma$ by a fixed-point free involution as in Definition <ref>.

We transform the sum as a sum over $f',(f_S)$. The automorphisms are related by
\begin{equation}
\# Aut(f) = \# Aut(f') \prod_{S} \# Aut(f_S)
\end{equation}
and a given set $[f'],([f_S])$ of isomorphism classes has
\begin{equation}
\prod_{S} z_{\bm{\eta}_S}
\end{equation}
pre-images $[f]$, where $\bm{\eta}_S$ is the partition of $d$ corresponding to the monodromy around $S$. For each $S$, the relation
\begin{equation}
\sum_{[f_S]} \frac{s(f_S)}{\# Aut(f_S)} = \mathbb{R}H^\bullet_{0,d}(\bm{\eta}_S)
\end{equation}
holds by Subsection <ref>, where the sum is over the ramified Real covers whose ramification profile at a pair of conjugated points is $\eta_S$ and unramified elsewhere. Thus, depending on whether $(X',\sigma')$ is the doublet of a genus $h$ Riemann surface or a connected Real Riemann surface of genus $h$, we obtain
\begin{equation}
\sum_{[f]} \frac{s(f)}{\# Aut(f)} = \sum_{\bm{\eta}} H^\bullet_{h,d,a}(\bm{\lambda},\bm{\eta}) \prod_{S} z_{\bm{\eta}_S} \mathbb{R}H^\bullet_{0,d}(\bm{\eta}_S)
\end{equation}
\begin{equation}
\sum_{[f]} \frac{s(f)}{\# Aut(f)} = \sum_{\bm{\eta}} \mathbb{R}H^\bullet_{h,d}(\bm{\lambda},\bm{\eta}) \prod_{S} z_{\bm{\eta}_S} \mathbb{R}H^\bullet_{0,d}(\bm{\eta}_S).
\end{equation}
Using degeneration formulas of types (a) and (b), see Proposition <ref>, the right-hand side is $\mathbb{R}H^\bullet_{g,d}(\bm{\lambda})$ in both cases.

By Proposition <ref>, the signs introduced in Subsections <ref> and <ref> are such that the signed sum of ramified Real covers does not depend on the involution $\sigma$ on the target $X$.

We now explain to what extent the sign $s(f)$ defined in (<ref>) is independent of the choices made. Recall that they consist of the ordering of the marked points created during the canonical degeneration and, if $(X',\sigma')$ is connected, of an admissible class.

Due to the cancellations occuring in $\mathbb{R}H_{0,d}((d))$ for $d$ even, we can restrict the discussion to the Real ramified covers $f$ of $(X,\sigma)$ for which every $f_S$ is the union of covers contributing to $\mathbb{R}H_{0,d}((d))$ for $d$ odd or $\mathbb{R}H_{0,2d}((d,d))$. Under this assumption, the partition at a marked point created during the degeneration must be even. Therefore, the choice of the ordering at these marked points does not modify the signs. If one of the partitions in $\bm{\lambda}$ is odd, the sum vanishes by Proposition <ref>. Otherwise, the signs are well-defined under the assumption above.

Similarly to Example <ref>, consider the compactification $E$ of the plane curve
\begin{equation}
\{ y^2 = x (x-w)(x-1/\overline{w}) \}
\end{equation}
with $|w| \neq 1$. The ramified cover $f : (x,y) \mapsto [1:x]$ has branch points $[1:0],[0:1],[1:w],[\overline{w}:1]$. If $\mathbb{P}^1_\mathbb{C}$ is endowed with the involution $\tilde{\theta}$ instead of $\theta$, there are still two anti-holomorphic involutions $\sigma_\pm$ on $E$ for which $f$ is a ramified Real cover. On the subset $\{(x,y) \in E \ | \ |x | = 1  \}$, which is the union of two circles, $\sigma_+$ induces the identity while $\sigma_-$ switches the two circles, see Figure <ref>.

Let us compute the signs $s(f_+)$ and $s(f_-)$. They depend on the marking of the target. We choose the ordering in the two pairs of conjugated marked points in $E$ so that the positive marked points belong to the same half of $\mathbb{P}^1_\mathbb{C}$. The ramified Real covers $f_+,f_-$ are both contributing since $f_{S,+}$ is the union of twice
\begin{equation}
id : (\mathbb{P}^1_\mathbb{C},\tilde{\theta}) \rightarrow (\mathbb{P}^1_\mathbb{C},\tilde{\theta})
\end{equation}
and $f_{S,-}$ is the doublet of
\begin{equation}
id : \mathbb{P}^1_\mathbb{C} \rightarrow \mathbb{P}^1_\mathbb{C}.
\end{equation}
The Real Riemann surface $(X',\sigma')$ being a doublet in this case, the signs $s(f_+)$ and $s(f_-)$ are well-defined. By (<ref>) and Example <ref>, they are
\begin{equation}
s(f_\pm ) = \pm 1.
\end{equation}
The hyperelliptic involution $(x,y) \mapsto (x,-y)$ is the only non-trivial automorphism of $f_+$ and $f_-$ so that we recover
\begin{equation}
\mathbb{R}H_{0,2}((2),(2)) = \frac{1}{2} - \frac{1}{2} =  0,
\end{equation}
see Example <ref>.

[scale = 0.7]
(0) at (-0.25, 1) ;
(1) at (0.25, 1) ;
(2) at (-0.25, -1) ;
(3) at (0.25, -1) ;
(4) at (-0.5, 0) ;
(5) at (0.5, 0) ;
(6) at (0, 6) ;
(7) at (0, 5) ;
(8) at (0, 3) ;
(9) at (0, 4) ;
(10) at (-0.5, 4.5) ;
(11) at (0.5, 4.5) ;
(12) at (-1.5, 4.5) ;
(13) at (1.5, 4.5) ;
(14) at (3.75, 1) ;
(15) at (4.25, 1) ;
(16) at (3.75, -1) ;
(17) at (4.25, -1) ;
(18) at (3.5, 0) ;
(19) at (4.5, 0) ;
(20) at (4, 6) ;
(21) at (4, 5) ;
(22) at (4, 3) ;
(23) at (4, 4) ;
(24) at (3.5, 4.5) ;
(25) at (4.5, 4.5) ;
(26) at (2.5, 4.5) ;
(27) at (5.5, 4.5) ;
(28) at (-0.5, 0) ;
(29) at (0.5, 0) ;
(30) at (-0.25, 0.25) ;
(31) at (0.25, 0.25) ;
(32) at (-0.25, -0.25) ;
(33) at (0.25, -0.25) ;
(34) at (3.5, 0) ;
(35) at (4.5, 0) ;
(36) at (3.75, 0.25) ;
(37) at (4.25, 0.25) ;
(38) at (3.75, -0.25) ;
(39) at (4.25, -0.25) ;
(40) at (-1.5, 4.5) ;
(41) at (-0.5, 4.5) ;
(42) at (-1.25, 4.75) ;
(43) at (-0.75, 4.75) ;
(44) at (-1.25, 4.25) ;
(45) at (-0.75, 4.25) ;
(46) at (0.5, 4.5) ;
(47) at (1.5, 4.5) ;
(48) at (0.75, 4.75) ;
(49) at (1.25, 4.75) ;
(50) at (0.75, 4.25) ;
(51) at (1.25, 4.25) ;
(52) at (2.5, 4.5) ;
(53) at (3.5, 4.5) ;
(54) at (2.75, 4.75) ;
(55) at (3.25, 4.75) ;
(56) at (2.75, 4.25) ;
(57) at (3.25, 4.25) ;
(58) at (4.5, 4.5) ;
(59) at (5.5, 4.5) ;
(60) at (4.75, 4.75) ;
(61) at (5.25, 4.75) ;
(62) at (4.75, 4.25) ;
(63) at (5.25, 4.25) ;
(64) at (0, 6) $\bullet$;
(65) at (0, 5) $\bullet$;
(66) at (0, 4) $\bullet$;
(67) at (0, 3) $\bullet$;
(68) at (4, 6) $\bullet$;
(69) at (4, 5) $\bullet$;
(70) at (4, 4) $\bullet$;
(71) at (4, 3) $\bullet$;
(72) at (-0.25, 1) $\bullet$;
(73) at (0.25, 1) $\bullet$;
(74) at (-0.25, -1) $\bullet$;
(75) at (0.25, -1) $\bullet$;
(76) at (3.75, 1) $\bullet$;
(77) at (4.25, 1) $\bullet$;
(78) at (3.75, -1) $\bullet$;
(79) at (4.25, -1) $\bullet$;
(80) at (0, 2.25) ;
(81) at (0, 1.75) ;
(82) at (4, 2.25) ;
(83) at (4, 1.75) ;
[bend left=15] (4.center) to (0.center);
[bend left=60, looseness=1.50] (0.center) to (1.center);
[bend left=15] (1.center) to (5.center);
[bend left=15] (5.center) to (3.center);
[bend left=60, looseness=1.50] (3.center) to (2.center);
[bend left=15] (2.center) to (4.center);
[bend left=45] (10.center) to (7.center);
[bend left=45] (7.center) to (11.center);
[bend left=45] (11.center) to (9.center);
[bend left=45] (9.center) to (10.center);
[bend left=45] (12.center) to (6.center);
[bend left=45] (6.center) to (13.center);
[bend left=45] (13.center) to (8.center);
[bend left=45] (8.center) to (12.center);
[bend left=15] (18.center) to (14.center);
[bend left=60, looseness=1.50] (14.center) to (15.center);
[bend left=15] (15.center) to (19.center);
[bend left=15] (19.center) to (17.center);
[bend left=60, looseness=1.50] (17.center) to (16.center);
[bend left=15] (16.center) to (18.center);
[bend left=45] (24.center) to (21.center);
[bend left=45] (21.center) to (25.center);
[bend left=45] (25.center) to (23.center);
[bend left=45] (23.center) to (24.center);
[bend left=45] (26.center) to (20.center);
[bend left=45] (20.center) to (27.center);
[bend left=45] (27.center) to (22.center);
[bend left=45] (22.center) to (26.center);
[bend left=15, looseness=1.25, dashed, very thick] (28.center) to (30.center);
[bend left=15, looseness=0.75, dashed, very thick] (30.center) to (31.center);
[bend left=15, looseness=1.25, dashed, very thick] (31.center) to (29.center);
[bend left=15, looseness=1.25, very thick] (29.center) to (33.center);
[bend left=15, looseness=0.75, very thick] (33.center) to (32.center);
[bend left=15, looseness=1.25, very thick] (32.center) to (28.center);
[bend left=15, looseness=1.25, dashed, very thick] (34.center) to (36.center);
[bend left=15, looseness=0.75, dashed, very thick] (36.center) to (37.center);
[bend left=15, looseness=1.25, dashed, very thick] (37.center) to (35.center);
[bend left=15, looseness=1.25, very thick] (35.center) to (39.center);
[bend left=15, looseness=0.75, very thick] (39.center) to (38.center);
[bend left=15, looseness=1.25, very thick] (38.center) to (34.center);
[bend left=15, looseness=1.25, dashed, very thick] (40.center) to (42.center);
[bend left=15, looseness=0.75, dashed, very thick] (42.center) to (43.center);
[bend left=15, looseness=1.25, dashed, very thick] (43.center) to (41.center);
[bend left=15, looseness=1.25, very thick] (41.center) to (45.center);
[bend left=15, looseness=0.75, very thick] (45.center) to (44.center);
[bend left=15, looseness=1.25, very thick] (44.center) to (40.center);
[bend left=15, looseness=1.25, dashed, very thick] (46.center) to (48.center);
[bend left=15, looseness=0.75, dashed, very thick] (48.center) to (49.center);
[bend left=15, looseness=1.25, dashed, very thick] (49.center) to (47.center);
[bend left=15, looseness=1.25, very thick] (47.center) to (51.center);
[bend left=15, looseness=0.75, very thick] (51.center) to (50.center);
[bend left=15, looseness=1.25, very thick] (50.center) to (46.center);
[bend left=15, looseness=1.25, dashed] (52.center) to (54.center);
[bend left=15, looseness=0.75, dashed] (54.center) to (55.center);
[bend left=15, looseness=1.25, dashed] (55.center) to (53.center);
[bend left=15, looseness=1.25] (53.center) to (57.center);
[bend left=15, looseness=0.75] (57.center) to (56.center);
[bend left=15, looseness=1.25] (56.center) to (52.center);
[bend left=15, looseness=1.25, dashed] (58.center) to (60.center);
[bend left=15, looseness=0.75, dashed] (60.center) to (61.center);
[bend left=15, looseness=1.25, dashed] (61.center) to (59.center);
[bend left=15, looseness=1.25] (59.center) to (63.center);
[bend left=15, looseness=0.75] (63.center) to (62.center);
[bend left=15, looseness=1.25] (62.center) to (58.center);
[stealth-stealth, dotted] (53.center) to (58.center);
[->] (80.center) to (81.center);
[->] (82.center) to (83.center);

Description of the two ramified Real covers of Example <ref>. The involutions $\sigma_+$ and and $\sigma_-$ correspond respectively to left-hand side and right-hand side.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

Cambridge University Press

seriesLondon Mathematical Society Student Texts
subtitleA First Course in Hurwitz Theory
titleRiemann Surfaces and Algebraic Curves

seriesGraduate Texts in Mathematics
subtitleA first course
titleRepresentation theory

journaltitleAdv. Math.
titleA Klein TQFT : the local Real Gromov-Witten theory of curves

titleSplitting formulas for the local real Gromov-Witten invariants

journaltitleComment. Math. Helv.
titleHurwitz numbers for real polynomials

journaltitleC. R. Acad. Sci. Paris
titlePolynomial functions on the set of Young diagrams

Cambridge University Press

seriesLondon Mathematical Society Student Texts
titleFrobenius Algebras and 2D Topological Quantum Field Theories

titleKlein Topological Field Theories from Group Representations

journaltitleAnn. Math.
titleGromov-Witten theory, Hurwitz theory, and completed cycles

journaltitleJ. Lond. Math. Soc.
titleOn double Hurwitz numbers with completed cycles

journaltitleAlgebr. Geom. Topol.
titleUnoriented topological quantum field theory and link homology

journaltitleInven. Math.
titleInvariants of real rational symplectic 4-manifolds and lower bounds in real enumerative geometry


Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

ARQNL, Nancy, 2024

<EMAIL_ADDRESS>]<EMAIL_ADDRESS>url=https://sites.google.com/site/ophelielacroixnlp/, ]
[orcid=0000-0002-2401-9158<EMAIL_ADDRESS>url=http://www.lirmm.fr/ retore, ]

# A proof-theoretical approach to
some extensions of first order quantification

Loïc Allègre  LIRMM (Univ Montpellier & CNRS), Montpellier, France  Ophélie
Lacroix  Resolve, Copenhagen, Danemark  Christian Retoré

(2024)

###### Abstract

Generalised quantifiers, which include Henkin’s branching quantifiers, have
been introduced by Mostowski and Lindström and developed as a substantial
topic application of logic, especially model theory, to linguistics with work
by Barwise, Cooper, Keenan.

In this paper, we mainly study the proof theory of some non-standard
quantifiers as second order formulae . Our first example is the usual pair of
first order quantifiers (for all / there exists) when individuals are viewed
as individual concepts handled by second order deductive rules. Our second
example is the study of a second order translation of the simplest branching
quantifier: “A member of each team and a member of each board of directors
know each other", for which we propose a second order treatment.

###### keywords:

proof theory second order logic generalised quantifiers branching quantifiers
individual concepts

##  1 Generalisation of usual first order quantification

Common first order quantifiers $\exists$ and $\forall$ have been formalised
the way they are in standard mathematics by Frege [1] whose logical and
philosophical view matches Hilbert desiderata regarding logical foundations of
mathematics.[2, 3, 4, 5]

By that time, mathematicians and logicians were making little difference
between the interpretations of quantifiers in _the_ standard model and their
proof rules — before the work of Skolem or Gödel mathematicians and logicians
made little distinction between syntax and semantics, they worked with an
interpreted language, see e.g. [2] —— perhaps Hilbert was more demanding
regarding quantifiers because he focused on foundations of mathematics [3].

Extension of usual quantification have mainly been considered for modelling
faithfully quantification modes that one founds in ordinary language, like
numbers (“three students came to the party"), “most" (“most students came to
the party"), percentage (“a third of the students came to the party"), vague
quantifiers (“few students came to the party") etc.

This gave rise to the theory of generalised quantifiers, initially intended
for model theory [6, 7] that was intensively developed in connection with
linguistics.[8, 9, 10]. In such a setting, the lexical item expressing a
quantifier (say “most A are B") is viewed as a function with two arguments
that are predicates. This fits in well with the logico-functional view known
as Montague semantics[11]. Most (!) generalised quantifiers can be viewed as a
second order construction. For instance the interpretation of a generalised
quantifier depending on two unary predicates like “most" is interpreted as a
second order construction, i.e. is true whenever the pairs of unary predicates
it is applied to is a “legal" pair of subsets of the domain, namely a pair of
sets $(A,B)$ such that $|A\cap B|>|A\setminus B|$.

The paper is organised as follows. We first provide a reminder on second order
logic, because this topic is not so common. Next, we present a second order
view of usual first order quantification as second order quantification over
individual concepts — and show the two formulations are proved to be
equivalent provided the individual concepts are standard (i.e. they may not be
empty, as opposed to some Kripke and Muskens variants). Then, after a quick
presentation of generalised quantifiers, we study the simplest branching
quantifier as a second order construction, and we propose direct rules for
this quantifier.

##  2 A reminder on second order logic

We briefly remind the reader with basic facts about second order logic,
following [12, Chapter 5], and one may also refer to the survey [13].

###  2.1 Language

A second-order language is based on a first-order language (the first three
items in the list below), and extended with an infinitely enumerable set of
predicate variables, each of them endowed with an arity (the last item in this
list).

  * •

an infinite enumerable set of first order (a.k.a. individual) variables
$x_{i}$, with $i$ in $\mathbb{N}$

  * •

a set of constants $c_{i}$, with $i$ in $I$ ($I$ is often enumerable, but this
is not required);111The first order language may also include an enumerable
set of first order functions, but an $n$-ary function $g$ in the language can
replaced with an $n+1$-ary predicate $G$ with an axiom that $F$ is a function,
and at second order there is a formula $F[X]$ saying that the $n+1$-ary
predicate $X$ corresponds to an $n$-ary function.

  * •

an enumerable (or finite) set of predicate constants $P_{i}^{n}$ with $i$ in
$\mathbb{N}$ each of them with an arity $n$ (as in a first order language) – a
predicate constant with arity $0$ is a proposition;

  * •

an enumerable set of predicate variables $X_{i}^{n}$ $i$ in $\mathbb{N}$ each
of them with an arity $n$ – a predicate variable with arity $0$ is a
propositional variable.

Second order formulae are defined “as expected": an atomic formula is
$Z^{n}(u_{1},\ldots,u_{n})$ with $Z$ a predicate constant or a predicate
variable of arity $n$ and the $u_{i}$ being $n$ first order terms (here first
order variables or first order constants since we have no functions). Les us
call $\mathcal{A}$ the set of atomic formulae . Then the set of second order
formulae $\mathcal{F}$ is defined by

$\mathcal{F}\ {=::}\
\mathcal{A}\mathrel{|}\lnot\mathcal{F}\mathrel{|}\mathcal{F}\land\mathcal{F}\mathrel{|}\mathcal{F}\lor\mathcal{F}\mathrel{|}\mathcal{F}\mathbin{\rightarrow}\mathcal{F}\mathrel{|}\forall
x\mathcal{F}\mathrel{|}\exists
x\mathcal{F}\mathrel{|}\forall^{n}X_{i}^{n}\mathcal{F}\mathrel{|}\exists^{n}X_{i}^{n}\mathcal{F}$

where $x$ stands for an individual variable while $X_{i}^{n}$ stands for a
predicate variable of arity $n$.

The formula $A\Leftrightarrow B$ is just a short-hand for
$(A\mathbin{\rightarrow}B)\land(B\mathbin{\rightarrow}A)$.

Although we shall not always write the n superscript in $\forall^{n}$ and
$\exists^{n}$ beware that there are different pairs of second order
quantifiers ($\exists^{n}/\forall^{n}$), one pair for each arity. The
occurrences of the variable $x_{i}$ or $X_{i}^{n}$ are bound by the closest
$\forall x,\exists x,\forall^{n}X_{i}^{n},\exists^{n}X_{i}^{n}$ — if any —
above them in the formula tree.

###  2.2 Proof rules in natural deduction

We use natural deduction with standard rules as can be found in [12]. As we
limit ourselves to classical logic, an extra principle is needed: tertium non
datur ($A\lor\lnot A$ for all $A$) or reductio ad absurdum (from a deduction
with conclusion $\bot$ under hypothesis $\lnot A$, conclude $A$), see e.g.
[14]

The proof rules for second order quantifiers, namely the introduction and
elimination rules of $\forall^{n}$ and $\exists^{n}$ are as expected, they are
similar to the rules for first order quantifiers, mutatis mutandi:

$\begin{array}[]{ccc}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 32.63138pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
25.18457pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 23.79568pt$\vbox to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\forall^{n}X_{i}^{n}\ T[X_{i}^{n}]$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=125.6319pt\hbox{\kern
3.00003pt$(\forall^{n})_{E}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
T[X_{i,k}^{n}(t^{1}_{k},\ldots,t^{n}_{k}):=\phi^{n}(t^{1}_{k},\ldots,t^{n}_{k})]$}}}}&&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
8.2911pt\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
11.89346pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 10.50458pt$\vbox to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle T[X_{i}^{n}]$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=50.36914pt\hbox{\kern
3.00003pt$(\forall^{n})_{I}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\forall^{n}X_{i}^{n}\
T[X_{i}^{n}]$}}}}\\\\[50.00008pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\exists^{n}X_{i}^{n}\
T[X_{i}^{n}]\hskip 5.0pt plus 1.0fil{\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\bigg{[}T[X_{i}^{n}]\bigg{]}^{k}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 17.88374pt$\vbox to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
16.01567pt\hbox{$\displaystyle\psi$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=98.91441pt\hbox{\kern
3.00003pt$(\exists^{n})_{E}^{k}$}}}\hbox{\kern
46.20024pt\hbox{$\displaystyle\psi$}}}}&&{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
62.81595pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 61.42706pt$\vbox to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle
T[X_{i,k}^{n}(t^{1}_{k},\ldots,t^{n}_{k}):=\phi^{n}(t^{1}_{k},\ldots,t^{n}_{k})]$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=135.6319pt\hbox{\kern
3.00003pt$(\exists^{n})_{I}$}}}\hbox{\kern
45.13138pt\hbox{$\displaystyle\exists^{n}X_{i}^{n}T[X_{i}^{n}]$}}}}\end{array}$

where

  1. 1.

$T[X_{i}^{n}]$ stands for a formula in which the predicate variable
$X_{i}^{n}$ may occur (but that is not mandatory, as for first order
quantification).

  2. 2.

There should be no free occurrence of $X_{i}^{n}$ in the hypotheses of the
introduction rule $(\forall^{n}X_{i}^{n})_{I}$ nor in the elimination rule
$(\exists X_{i}^{n})_{E}$ — as in the first order $\forall_{I}$ and
$\exists_{E}$ introduction rules.

  3. 3.

The obscure notation222This point if often under explained in the literature.
$T[X_{i,k}^{n}(t^{1}_{k},\ldots,t^{n}_{k}):=\phi^{n}(t^{1}_{k},\ldots,t^{n}_{k})]$
requires some explanation. This formula stands for the formula obtained by
replacing

     * •

the $k^{\mathrm{th}}$ occurrence $X_{i,k}^{n}$ of $X_{i}^{n}$ which is applied
to $n$ terms $(t^{1}_{k},\ldots,t^{n}_{k})$

     * •

with a formula with $n$ free variables applied to the very same terms
$(t^{1}_{k},\ldots,t^{n}_{k})$

with the requirement that no originally free variable in
$(t^{1}_{k},\ldots,t^{n}_{k})$ becomes bound after the application of $\phi$
to $(t^{1}_{k},\ldots,t^{n}_{k})$.
Here is an example: let $\phi(x,y)=P(x,y)\land Q(y,a)$, let
$T[X_{1}^{2}]=X_{1,1}^{2}(z,a)\land X_{1,2}^{2}(a,b)$ – mind the second
subscript of $X_{1,\bullet}^{2}$ which indicates the occurrence number (there
are two occurrences of the predicate variable $X_{1}^{2}$ in $T[X_{1}^{2}]$.
Then $T[X_{1,k}^{2}:=\phi(t^{1}_{k},\ldots,t^{n}_{k})]$ is
$(\phi(x,y)=P(x,y)\land Q(y,a))[x:=z;y:=a]\land(\phi(x,y)=P(x,y)\land
Q(y,a))[x:=a;y:=b]$ that is $(P(z,a)\land Q(a,a))\land(P(a,b)\land Q(b,a))$.
From the definition and the example, it is unsurprising that second order
unification, is undecidable [15].

  4. 4.

In the rule $(\exists^{n})_{E}$ the expression
$\bigg{[}T[X_{i}^{n}]\bigg{]}_{k}$ indicates that the hypothesis
$T[X_{i}^{n}]$ has been cancelled during the $(\exists^{n})_{E}$ number $k$.

Some remarks:

  1. 1.

this proof system can derive the comprehension axiom:

$\exists X^{n}\forall x_{1}\ldots
x_{n}\left[\varphi\left(x_{1},\ldots,x_{n}\right)\leftrightarrow
X^{n}\left(x_{1},\ldots,x_{n}\right)\right]$

  2. 2.

equality can be defined à la Leibnitz:
$x=y:\forall^{1}X^{1}X^{1}(x)\mathbin{\rightarrow}X^{1}(y)$ (because of
negation there is no need to use $\Leftrightarrow$ in this definition)

  3. 3.

being equal to $x$ is a property
$E_{x}(y):\forall^{1}X^{1}(x)\mathbin{\rightarrow}X^{1}(y)$.

  4. 4.

the Dedekind finiteness, “any injective function is surjective" is definable:

$\forall^{2}X^{2}\quad((\forall x\forall y\forall z(X(x,y)\land
X(x,z)\mathbin{\rightarrow}y=z))\land(\forall x\forall y\forall z(X(y,x)\land
X(z,x)\mathbin{\rightarrow}y=z)))$

$\mathbin{\rightarrow}(\forall w\exists u\ X(u,w))$

Finally, using implication $\mathbin{\rightarrow}$, first order $\forall$, and
propositional second order $\forall^{0}$ one can define false, $\bot$,
negation $\lnot$, the propositional connective $\land$, $\lor$, first order
existential quantification $\exists$. Adding $\forall^{n}$ to
$\mathbin{\rightarrow}$, $\forall$, one can also define $\exists^{n}$. Thus,
the expressive power of second order propositional quantifier $\forall^{0}$ is
impressive.

###  2.3 Standard and non-standard models, completeness

We here follow [16, 13, 12].

A second order model consists in a first order model, i.e. with a domain $D$,
endowed with a set of sets of tuples of length $n$ for each $n\in\mathbb{N}$
in order to interpret predicate variables of arity $n$: they may vary in a
fixed subset $A^{n}$ of $\mathcal{P}(D^{n})$ which is not necessarily the full
powerset $\mathcal{P}(D^{n})$; for this structure to define a model, it must
enjoy the comprehension axiom scheme $\exists^{n}X^{n}\forall
x_{1}\cdots\forall x_{n}[\phi(x_{1},\ldots,x_{n})\leftrightarrow
X^{n}(x_{1},\ldots,x_{n})]$ where the $n$-ary predicate variable $X^{n}$ does
not appear in $\phi$ — in other words the subsets of $A^{n}$ must include the
interpretations of the formulae with $n$ free variables. The comprehension
axiom scheme is derivable from the existential introduction rule given above.

When for any arity $n$ this subset $A^{n}$ is $\mathcal{P}(D^{n})$ the model
is said to be _standard_ (or full). Standard models, which satisfy the
comprehension scheme, match the easiest intuition: a predicate variable of
arity $n$ varies in all possible subsets of $D^{n}$. As second order logic can
express the finiteness of the model, completeness and compactness do not hold
with standard models.

Second order logic may be encoded in first order logic: predicate variables
$X_{i}^{n}$ are viewed as individual constants interpreted in a domain (that
also contains standard individuals), and some additional predicate constants
of arity $n+1$ are needed to mimic the application of a predicate variable of
arity $n$ to $n$ terms. Then a second order formula is provable within second
order logic whenever its first order translation is provable in first order
logic. So applying first order completeness theorem one gets that a second
order formula is provable in second order logic if and only if it is true in
all second order models (including the non standard ones). As a consequence of
completeness, compactness holds, so one can have a model with at least $n$
elements for each integer $n$, which is Dedekind finite.

##  3 A second order view of first order quantification:
quantifying over individual concepts

###  3.1 Individual concepts

Individual concepts view an individual as a formula $\phi[x]$ with a single
free variable $x$ such that there is a single individual satisfying the
formula $\phi[x]$.333This notion of concept is somehow related to concepts in
description logics, and the individual concepts that we use correspond to
individual names cf. e.g. [17]. This can be said in second order logic: a
formula $\phi[x]$ with a single free variable $x$ is said to be an individual
concept whenever there is at most one individual $x$ such that $\phi[x]$ and
at least one $x$ such that $\phi[x]$ — so it makes exactly one $x$ such that
$phi[x]$. That the concept $\phi$ is an _individual concept_ can actually be
expressed in second order logic:

$C(\phi):(\forall x\forall
y\phi(x)\land\phi(y)\mathbin{\rightarrow}x=y)\land\exists z\phi(z)$

Individual concepts are close to Montague semantics and Leibnitz identity
(where an individual is identified with the set of all properties it enjoys)
[18, 19, 11]. For reasons like possible worlds semantics, see e.g. the
discussion in [20, chapter 4], some logicians consider a variant of individual
concepts that are possibly empty. This may look strange but if you think
individual concepts are some kind of proper name that are part of the logical
language, it is hard to tell what a proper name refers to before the reference
actually exists. For instance, the individual concept $\mathrm{G\"{o}del}(x)$
has no reference in Egyptian times. Hence Kripke in the 70s dropped the
existence condition from individual concepts (see [21] for a recent account of
those ideas), thus obtaining a formula with a lower logical complexity
profile:

$C(\phi):(\forall x\forall y\phi(x)\land\phi(y)\mathbin{\rightarrow}x=y)$

###  3.2 First order universal quantification as universal quantification over
non-empty individual concepts

The simplest quantifiers one can try to view as a second order construction
are clearly the usual first order quantifiers $\forall,\exists$. So let us
compare the second order quantification over individual concepts to usual
quantification.

######  Proposition 1.

First order universal quantification and second order quantification over
individual concepts are equivalent:

  1. 1.

given a property $\varphi(X)$ of individual concepts, the following
equivalence holds: $\forall x\varphi^{\downarrow}(x)\Leftrightarrow\forall
X(C(X)\mathbin{\rightarrow}\varphi(X))$ where
$\varphi^{\downarrow}(x):=\exists X(C(X)\wedge$ $X(x)\wedge\varphi(X))$.

  2. 2.

given a property $\psi(x)$ of individuals, the following equivalence holds:
$\forall x\psi(x)\Leftrightarrow\forall
X\left(C(X)\mathbin{\rightarrow}\psi^{\uparrow}(X)\right)$ where
$\psi^{\uparrow}(X):=\exists x(X(x)\wedge\psi(x))$.

###### Proof.

Let us first observe that there is a simple formal proof without assumption
that $C(E_{x})$ i.e. that “being equal to $x$" (cf. section 2 item 3) is an
individual concept, $E_{x}(y):y=x:\forall^{1}X^{1}\
(X^{1}(x)\mathbin{\rightarrow}X^{1}(y))$, and let us call this proof $\delta$,
because we are going to use it several times:

$\delta:$

  1. 1.

    1. (a)

Assuming $\forall x\varphi^{\downarrow}(x)$ one can prove $\forall
X(C(X)\mathbin{\rightarrow}\varphi(X))$

    2. (b)

Assuming $\forall X(C(X)\mathbin{\rightarrow}\varphi(X))$ one can prove
$\forall x\varphi^{\downarrow}(x)$. In the proof below, we use $\delta$ the
proof that $E_{x}(\\_)=``\\_=x"$ is an individual concept.

  2. 2.

    1. (a)

Assuming $\forall x\psi(x)$ one can prove $\forall
X\left(C(X)\mathbin{\rightarrow}\psi^{\uparrow}(X)\right)$

    2. (b)

Finally assuming $\forall
X\left(C(X)\mathbin{\rightarrow}\psi^{\uparrow}(X)\right)$ one can prove:
$\forall x\psi(x)$

∎

###  3.3 First order existential quantification as existential quantification
over non-empty individual concepts

As for the universal quantification, we have:

######  Proposition 2.

First order existential quantification and second order quantification over
individual concepts are equivalent:

  1. 1.

when $\phi$ is a property of individual concepts, one has $\exists
x\varphi^{\downarrow}(x)\Leftrightarrow\exists X(C(X)\wedge\varphi(X))$ where
$\varphi^{\downarrow}(x):=\exists X(C(X)\wedge$ $X(x)\wedge\varphi(X))$.

  2. 2.

when $\psi$ is a property of individuals, one has $\exists
x\psi(x)\Leftrightarrow\exists X\left(C(X)\wedge\psi^{\uparrow}(X)\right)$
where $\psi^{\uparrow}(X):=\exists x(X(x)\wedge\psi(x))$

###### Proof.

At point 2.a) we will also use the proof $\delta$ of $C(E_{x})$ from the proof
of proposition 1.

  1. 1.

$\exists x\varphi^{\downarrow}(x)\Leftrightarrow\exists
X(C(X)\wedge\varphi(X))$ where $\varphi^{\downarrow}(x):=\exists X(C(X)\wedge$
$X(x)\wedge\varphi(X)$

    1. (a)

Let us prove $\exists X(C(X)\wedge\varphi(X))$ under the assumption $\exists
x\varphi^{\downarrow}(x)$.

    2. (b)

Now let us prove $\exists x\varphi^{\downarrow}(x)$ under the assumption
$\exists X(C(X)\wedge\varphi(X))$. We first need $\alpha,\beta,\gamma$ i.e.
the three following proofs :

$\begin{array}[]{ll}\alpha:&\\\ &\includegraphics[scale={1.2}]{alpha.pdf}\\\
\end{array}$

$\begin{array}[]{ll}\beta:&\\\ &\includegraphics[scale={1.2}]{beta.pdf}\\\
\end{array}$

$\begin{array}[]{ll}\gamma:&\\\ &\includegraphics[scale={1.4}]{gamma.pdf}\\\
\end{array}$

and the proof we are looking for is:

  2. 2.

$\exists x\psi(x)\Leftrightarrow\exists
X\left(C(X)\wedge\psi^{\uparrow}(X)\right)$ where $\psi^{\uparrow}(X):=\exists
x(X(x)\wedge\psi(x))$

    1. (a)

Let us prove $\exists X\left(C(X)\wedge\psi^{\uparrow}(X)\right)$ under the
assumption $\exists x\psi(x)$ – $\delta$ is the proof of $C(E_{x})$ defined in
the proof of proposition 1.

    2. (b)

Let us prove $\exists x\psi(x)$ under the assumption $\exists
X\left(C(X)\wedge\psi^{\uparrow}(X)\right)$

∎

###  3.4 Dealing with possibly empty individual concepts

When individual concepts are possibly empty the second order formula
expressing that $X$ is an individual concept is $C(X)=\forall x\forall
y(Xx\wedge Xy\mathbin{\rightarrow}x=y)$ — the $\exists xX(x)$ left out of our
initial definition of individual concepts.

Regarding universal quantification, $\forall
X(C(X)\mathbin{\rightarrow}\varphi(X))$ still entails $\forall
x\varphi^{\downarrow}(x)$, but $\forall x\varphi^{\downarrow}(x)$ does not
entail $\forall X(C(X)\mathbin{\rightarrow}\varphi(X))$ anymore. This is
logical: when all individual concepts have a property be they empty or not,
all individuals enjoy the corresponding first order property. The converse
does not hold: when all individuals enjoy a property, all the non empty
concepts enjoy the property, but why should the empty individual concept enjoy
this property as well?

Of course regarding existential quantification, that’s the opposite. $\exists
x\varphi(x)$ entails $\exists X(C(X)\wedge\varphi(X)))$ but $\exists
X(C(X)\wedge\varphi(X))$ does not entail $\exists x\varphi(x)$. When an
individual enjoys a property, so does the corresponding individual concept.
But when a possibly empty individual concept enjoys a property, it does not
entail that an individual enjoys this property, because this individual
concept might be an empty individual concept.

So the second order view of usual quantification does not fit in well with
possibly empty individual concepts.

##  4 A reminder on generalised and branching quantifiers

This reminder mainly relies on the presentation given by Peters and
Westerståhl [22], oen may also consult the survey [10]. Generalised
quantifiers, initially introduced by Mostowski [6] and further developed by
Lindström[7] are a generalisation of standard universal and existential
quantification. Roughly speaking, generalised quantifiers view quantifiers as
relations over relations (or tuples of relations) — those relations are
relations on the domain (a.k.a universe, model) of an interpretation: thus,
quantifiers are viewed as second-order concepts.

###  4.1 Generalised quantifiers

Given $k$ integers $n_{1},...,n_{k}$, a quantifier $\mathcal{Q}$ of type
$\langle n_{1},...,n_{k}\rangle$ can be viewed as a function endowing each
domain $M$ with a $k$-ary relation $Q_{M}$ such that if $(R_{1},...,R_{k})\in
Q_{M}$, then for all $i$ in between $1$ and $k$, $R_{i}$ is a $n_{i}$-ary
relation over elements of $M$. Let us give some examples.

The usual quantifiers $\forall$ and $\exists$ can be then expressed as simple
type $\langle 1\rangle$ quantifiers : $\exists_{M}=\\{A\subseteq M,\
A\neq\emptyset\\}$ and $\forall_{M}=\\{A\subseteq M,\ A=M\\}$. Thus, the
existential quantifier is in every domain the unary relation which holds true
for all non-empty predicates, and the universal quantifier is the relation
which holds true only for the whole domain $M$.

Some generalised quantifiers have an equivalent formulation in usual first-
order logic, such as the quantifier “at least two": $(\exists_{\geq
2})_{M}=\\{A\subseteq M,\ |A|\geq 2\\}$ which can be expressed with the
following first-order formula: $\exists x\exists yx\neq y$ However this is not
always the case. Take for example the type $\langle 1,1\rangle$ quantifier
expressing that most $A$ are $B$:
$\textbf{Most}_{M}(A,B)\Longleftrightarrow|A\cap B|>|A-B|$ which notably
cannot be expressed as a first-order formula.

It is worth noting that universal and existential quantification on individual
concepts as we presented in Section 3 can also be formulated in terms of
generalised quantifiers. To say that all (resp. some) individual concepts
satisfy a property $\varphi$ is in fact a second-order statement about the
predicates $C$ (“to be an individual concept") and $\varphi$. Hence the second
order view of first order quantification that we presented in the previous
section can be expressed as generalised quantifiers $\forall_{C}$ and
$\exists_{C}$ with type $\langle 1,1\rangle$:

$\quad\forall_{C}(C,\varphi)\Longleftrightarrow
C\subset\varphi\quad\quad\exists_{C}(C,\varphi)\Longleftrightarrow
C\cap\varphi\neq\emptyset$

###  4.2 Branching quantifiers

Among generalised quantifiers, branching quantifiers are of particular
interest, both for logic and linguistics. Initially introduced by Henkin [23]
and much later on studied by Hintikka [24] — independently of generalised
quantifiers — branching quantification is a generalisation of classical
quantification that allows the expression of independence between some
existentially quantified variable and some previously universally quantified
variables. This cannot be expressed within usual quantification because
quantifiers are supposed to be linearly ordered. The simplest example of such
a non-first-order quantifier is the following Henkin quantifier where, as the
notation suggests, $x^{\prime}$ only depends on $x$, while $y^{\prime}$, only
depends on $y$.

$F(x,y,x^{\prime},y^{\prime})$$\forall x\exists x^{\prime}$$\forall y\exists
y^{\prime}$

As proven by Ehrenfeucht (in Henkin [23]), this construction has no first-
order equivalent. Notably, it cannot be expressed with a linear quantifier
prefix such as $\forall x\exists x^{\prime}\forall y\exists y^{\prime}$ or
$\forall x\forall y\exists x^{\prime}\exists y^{\prime}$, since there would be
unwanted dependencies between $x^{\prime}$ and $y$, and $y^{\prime}$ and $x$.

Although not initially introduced as such, branching quantifiers can in fact
be seen as specific generalised quantifiers. Indeed, the (in)dependencies
between variables can be expressed using Skolem functions, e.g. the Henkin
quantifier above can be written as follows:

$\exists f\exists g\forall x\forall y\ F(x,f(x),y,g(y))$

This in turn allows us to translate it as a generalised quantifier, for
example here as the type $\langle 4\rangle$ quantifier:

$H_{M}=\\{R\subseteq M^{4}\ |\ \exists f\exists g\forall x\forall y\
(x,f(x),y,g(y))\in R\\}$

##  5 Second-order proof rules for branching quantifiers

#### Branching quantifiers as second-order formulae

In this part, we focus on the expression of branching quantifiers as second-
order constructions. Such quantifiers can be quite complex, so we limit
ourselves to studying the simplest branching quantifier. Our main object of
study is the typical branching constructions found in natural language in the
so-called Hintikka sentences, such as :

(H) A member of each team and a member of each board of directors know each
other

The branching-quantifier reading of the above English sentence can be
formulated within second-order logic:444There is also a first-order reading of
this sentence, which the ’each other’ (perhaps) makes less perceptible, and
which can be expressed within first-order logic: $[\forall x\exists
x^{\prime}\forall y\exists y^{\prime}\quad T(x)\wedge
B(y)\mathbin{\rightarrow}M(x,x^{\prime})\wedge M(y,y^{\prime})\wedge
K(x^{\prime},y^{\prime})]\land[\forall y\exists y^{\prime}\forall x\exists
x^{\prime}\quad T(x)\wedge B(y)\mathbin{\rightarrow}M(x,x^{\prime})\wedge
M(y,y^{\prime})\wedge K(x^{\prime},y^{\prime})]$. According to Szymanik [25],
in two-thirds of cases, the first first-order reading is preferred to the
branching quantifier reading.

$T(x)\wedge B(y)\mathbin{\rightarrow}M(x,x^{\prime})\wedge
M(y,y^{\prime})\wedge K(x^{\prime},y^{\prime})$$\forall x\exists
x^{\prime}$$\forall y\exists y^{\prime}$

As mentioned earlier, this formula can be expressed as a second order formula
with existential quantification over functions:

$(\mathsf{Hfun}):\exists f\exists g\forall x\forall y\ T(x)\wedge
B(y)\mathbin{\rightarrow}K(f(x),g(y))$

#### Natural deduction rules with binary predicates

This formulation of the Henkin quantifier as a second-order formula with
quantification over functions is however not fully satisfactory, for it
actually provides a stronger effect than needed: defining $f$ and $g$ as
functions implies the unicity of $f(x)$ and $g(y)$ for any given $x$ and $y$,
while the original formula with a branching quantifier only requires that
there exists one (possibly more) $x^{\prime}$ for each $x$ and $y^{\prime}$
for each $y$. Thus $f$ and $g$ need not be functions, but only need be non-
empty binary predicates — as always with Skolem functions, the choice of
$f(x)$ for each $x$ is part of the interpretation of the function symbol.

Therefore, we propose another second-order representation of this reading of
the sentence using quantification over predicates instead of quantification
over functions:

$\begin{split}(\mathsf{Hpred}):&\exists F\exists G[\forall x\exists
x^{\prime}T(x)\mathbin{\rightarrow}F(x,x^{\prime})]\wedge[\forall y\exists
y^{\prime}B(y)\mathbin{\rightarrow}G(y,y^{\prime})]\\\ &\wedge[\forall
x\forall x^{\prime}\forall y\forall y^{\prime}T(x)\wedge B(y)\wedge
F(x,x^{\prime})\wedge
G(y,y^{\prime})\mathbin{\rightarrow}K(x^{\prime},y^{\prime})]\end{split}$

This formula simply replaces each of the two functions $f$ and $g$ of $(Hfun)$
above with the binary predicates $F$ and $G$. These two predicates act
intuitively as relations that select suitable $x^{\prime}$ and $y^{\prime}$,
since all we need to ensure is that whenever $x^{\prime}$ is a valid
representative for $x$ (and $y^{\prime}$ for $y$), then $x^{\prime}$ and
$y^{\prime}$ know each other. The binary predicates $F$ and $G$ are required
to relate each possible value of their first argument which ought to be in the
proper set/predicate ($T$ for $x$, $B$ for $y$) to at least one value of their
second argument.555Similarly, we could ask that $x^{\prime}$ and $y^{\prime}$
are in the proper set/predicate ($T$ for $x^{\prime}$, $B$ for $y^{\prime}$)
but it is less important. Thus we do not add this precision, which is not
needed — unlike the restriction to $x$ and $y$ — and makes the formulae, which
are already long enough, considerably longer: $\mathsf{Hpred}^{\prime}:\exists
F\exists G[\forall x\exists
x^{\prime}T(x)\mathbin{\rightarrow}F(x,x^{\prime})\land
T(x^{\prime})]\wedge[\forall y\exists
y^{\prime}B(y)\mathbin{\rightarrow}G(y,y^{\prime})\land
B(y^{\prime})]\wedge[\forall x\forall x^{\prime}\forall y\forall
y^{\prime}T(x)\wedge T(x^{\prime})\wedge B(y)\wedge B(y^{\prime})\wedge
F(x,x^{\prime})\wedge
G(y,y^{\prime})\mathbin{\rightarrow}K(x^{\prime},y^{\prime})]$ There is
nevertheless a difference between using function as in $(\mathsf{Hfun})$ and
$(\mathsf{Hpred})$: in $(\mathsf{Hpred})$ there may well exist several values
of $x^{\prime}$ (resp. $y^{\prime}$) such that $F(x,x^{\prime})$ (resp.
$G(y,y^{\prime})$), there is no need to chose one as opposed to
$(\mathsf{Hfun})$, where one is explicitly chosen.

The natural deduction rules for second-order logic from section 2.2 give us
the introduction and elimination rules for the branching Henkin quantifier.
For the sake of readability, let us write from here on:

$\Phi(F,G,x,x^{\prime},y,y^{\prime})=T(x)\wedge B(y)\wedge
F(x,x^{\prime})\wedge G(y,y^{\prime})\rightarrow K(x^{\prime},y^{\prime})$

and

$\begin{split}\Psi(F,G)=\ &[\forall x\exists
x^{\prime}T(x)\mathbin{\rightarrow}F(x,x^{\prime})]\wedge[\forall y\exists
y^{\prime}B(y)\mathbin{\rightarrow}G(y,y^{\prime})]\\\ &\wedge[\forall
x,\forall x^{\prime}\forall y\forall
y^{\prime}\Phi(F,G,x,x^{\prime},y,y^{\prime})]\end{split}$

The introduction rule is quite straightforward:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
105.17618pt\hbox{$\displaystyle\penalty
1\varphi(x,t)\qquad\psi(y,u)\qquad\Phi(\varphi,\psi,x,x^{\prime},y,y^{\prime})$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=383.4764pt\hbox{\kern
3.00003pt$H_{I}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\exists F\exists
G[\forall x\exists
x^{\prime}T(x)\mathbin{\rightarrow}F(x,x^{\prime})]\wedge[\forall y\exists
y^{\prime}B(y)\mathbin{\rightarrow}G(y,y^{\prime})]\wedge[\forall x,\forall
x^{\prime}\forall y\forall
y^{\prime}\Phi(F,G,x,x^{\prime},y,y^{\prime})]$}}}}$

where $\varphi$ is a formula with free variables exactly $x,x^{\prime}$,
$\psi$ a formula with free variables exactly $y,y^{\prime}$, and $t,u$ are
terms.

The elimination rule, however, is more complicated due to the use of two
second-order eliminations of $\exists^{2}$:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\exists F\exists G\Psi(F,G)\quad\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1[\exists G\Psi(A,G)]^{(2)}\quad\hskip
5.0pt plus 1.0fil{\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1[\Psi(A,B)]^{(1)}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 22.7601pt$\vbox to16.14578pt{\leaders\vbox
to5.38193pt{\vss\hbox{$\cdot$}\vss}\vfill}$\hbox{}}}\hbox{\kern
20.87816pt\hbox{$\displaystyle\varphi$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\quad$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=141.45634pt\hbox{\kern
3.00003pt$\exists^{2}E^{(1)}$}}}\hbox{\kern
67.45734pt\hbox{$\displaystyle\varphi$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=277.17508pt\hbox{\kern
3.00003pt$\exists^{2}E^{(2)}$}}}\hbox{\kern
135.31671pt\hbox{$\displaystyle\varphi$}}}}$

in which $A$ and $B$ must not appear free in $\varphi$.

Let us write as above $H(x,x^{\prime},y,y^{\prime})$ the branching quantifier
that binds the two universally quantified variables $x,y$ and the two
existentially quantified variables $x^{\prime},y^{\prime}$ e.g. the example
above may be written $H(x,x^{\prime},y,y^{\prime})\
\Phi(F,G,x,x^{\prime},y,y^{\prime})$.

Let $\mathcal{H}$ be the set of closed formulae that can be written with this
quantifier and the two usual first order quantifiers $\exists x$ and $\forall
y$.

In the near future, we intend to determine whether our direct rules can be
used to derive all the formulae in $\mathcal{H}$ that can be derived with the
usual rules for second and first quantifiers. It seems plausible to us,
because cut-elimination holds for second order logic. [26] However, we are not
yet fully certain, and this is one aspect that we intend to clarify in the
near future.

##  6 Conclusion

This ongoing work deals with the proof rules of extensions of first order
quantification viewed as second order logic constructions which do not need
the full expressive power (and complexity) of second order logic.

We first described usual first order quantifiers within the second order logic
as quantification over individual concepts and obtained that this description
works provided individual concepts are asked to be non empty — unsurprisingly
it does not work without this restriction.

Thereafter we focused on the non first order reading of the simplest branching
quantifier that one finds in sentences like: “A member of each team and a
member of each board of directors know each other". Regarding this (reading of
this) quantifier, we proposed a definition of it within second order logic and
provided direct introduction and elimination rules for this complex quantifier
which is often only described in model-theoretic terms. Later on we shall
prove that the complete set of second order rules does not derive more
sentences with those connectives than our direct rules.

By way of conclusion, let us mention a prospect that has opened up to us
recently. The epsilon calculus,[27, 28] may express readings that are close to
branching quantifier readings, with epsilon formulas that have no equivalent
in first or higher order logic. Indeed, the subnectors epsilon and tau express
quantification with some scope ambiguities (under-specification). However, it
is presently too early to say anything definite about this question.

Last minute remark: While we were revising this article we realised that
Matthias Baaz and Anela Lolic [29] proposed an analytic calculus for Henkin
quantifiers. In their paper, Henkin quantifiers are viewed as the existence of
functions (i.e. as a particular form of second order quantification), and they
proved cut-elimination for this calculus. It is too late for this paper of
ours to examine how their account of Henkin quantifiers differs from ours, but
this will be be our first aim in continuing our work. A first remark is that
$(1):\exists F\forall u\exists vF(u,v)$ seems slightly weaker than
$(2):\exists fF(u,f(u))$: in order to derive $(2)$ from $1$, it is necessary
to utilise some form of the axiom of choice. Another difference, a very small
one actually, is that our rules are natural deduction rules
(introduction/elimination rules) and not sequent calculus: sequent-calculus
right-rules correspond to natural-deduction introduction-rules but sequent-
calculus left-rules do not correspond to natural-deduction elimination-rules.

###### Acknowledgements.

We would like to express our gratitude to the anonymous reviewers of ARQNL2024
for their valuable feedback, which has been instrumental in helping us to
enhance this article. Furthermore, we would like to extend our gratitude to
the programme chairs who accepted some late modifications.

## References

  * Frege [1879] G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Verlag von Louis Nebert, Halle, 1879.
  * Kneale and Kneale [1986] W. Kneale, M. Kneale, The development of logic, 3${}^{\textrm{rd}}$ ed., Oxford University Press, 1986.
  * Goldfarb [1979] W. D. Goldfarb,  Logic in the twenties: The nature of the quantifier,  J. Symb. Log. 44 (1979) 351–368. URL: https://doi.org/10.2307/2273128. doi:10.2307/2273128.
  * Hilbert and Bernays [1934] D. Hilbert, P. Bernays, Grundlagen der Mathematik. Bd. 1., Berlin: Julius Springer. XII, 471 S., 1934. Traduction française de F. Gaillard et M. Guillaume, L’Harmattan, 2001.
  * Hilbert and Bernays [1939] D. Hilbert, P. Bernays, Grundlagen der Mathematik. Bd. 2., Springer, 1939. Traduction française de F. Gaillard, E. Guillaume et M. Guillaume, L’Harmattan, 2001.
  * Mostowski [1957] A. Mostowski,  On a generalization of quantifiers,  Fundamenta Mathematicae 44 (1957) 12–36.
  * Lindström [1966] P. Lindström,  First order predicate logic with generalized quantifiers,  Theoria 32 (1966) 186–195.
  * Barwise and Cooper [1981] J. Barwise, R. Cooper,  Generalized quantifiers and natural language,  Linguistics and Philosophy 4 (1981) 159–219. doi:10.1007/BF00350139.
  * Keenan and Stavi [1986] E. Keenan, J. Stavi,  A semantic characterization of natural language determiners,  Linguistic and Philosophy 9 (1986) 253–326.
  * Westerståhl [2019] D. Westerståhl,  Generalized Quantifiers,  in: E. N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy, Winter 2019 ed., Metaphysics Research Lab, Stanford University, 2019.
  * Montague [2002] R. Montague, The Proper Treatment of Quantification in Ordinary English, Blackwell Publishers, 2002.
  * van Dalen [2013] D. van Dalen, Logic and Structure, Universitext, fifth ed., Springer-Verlag, 2013.
  * Väänänen [2021] J. Väänänen,  Second-order and Higher-order Logic,  in: E. N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy, Fall 2021 ed., Metaphysics Research Lab, Stanford University, 2021.
  * Moot and Retoré [2016] R. Moot, C. Retoré, Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation, 2016. arXiv:1602.07608.
  * Goldfarb [1981] W. D. Goldfarb,  The undecidability of the second-order unification problem,  Theor. Comput. Sci. 13 (1981) 225–230. URL: https://doi.org/10.1016/0304-3975(81)90040-2. doi:10.1016/0304-3975(81)90040-2.
  * Henkin [1950] L. Henkin,  Completeness in the theory of types,  J. Symb. Log. 15 (1950) 81–91. URL: https://doi.org/10.2307/2266967.
  * Rudolph [2011] S. Rudolph,  Foundations of description logics,  in: A. Polleres, C. d’Amato, M. Arenas, S. Handschuh, P. Kroner, S. Ossowski, P. F. Patel-Schneider (Eds.), Reasoning Web. Semantic Technologies for the Web of Data - 7th International Summer School 2011, Tutorial Lectures, volume 6848 of LNCS, Springer, 2011, pp. 76–136. doi:10.1007/978-3-642-23032-5_2.
  * Kripke [1971] S. Kripke,  Identity and necessity,  in: M. Munitz (Ed.), Indentity and Individuation, New-York University Press, 1971, pp. 135–164.
  * Kripke [1972] S. Kripke,  Naming and necessity,  in: D. Davidson, G. Harman (Eds.), Semantics of Natural Language, Reidel, 1972, pp. 253–355.
  * Fitting and Mendelsohn [1998] M. Fitting, R. Mendelsohn, First-Order Modal Logic, Springer Netherlands, 1998.
  * Muskens [2012] R. Muskens,  A theory of names and true intensionality,  in: M. Aloni, V. Kimmelman, F. Roelofsen, G. W. Sassoon, K. Schulz, M. Westera (Eds.), Amsterdam Colloquium 2011, volume 7218 of LNCS/FoLLI, Springer-Verlag, 2012, pp. 441–449.
  * Peters and Westerståhl [2006] S. Peters, D. Westerståhl, Quantifiers in Language and Logic, Clarendon Press, 2006.
  * Henkin [1961] L. Henkin,  Some remarks on infinitely long formulas,  in: Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics, Warsaw, 1959, Panstwowe Wydawnictwo Naukowe / Pergamon Press, Warsaw, 1961, pp. 167–183.
  * Hintikka and Sandu [1996] J. Hintikka, G. Sandu,  Game-theoretical semantics,  in: J. van Benthem, A. ter Meulen (Eds.), Handbook of Logic and Language, North-Holland Elsevier, Amsterdam, 1996, pp. 361–410.
  * Szymanik [2016] J. Szymanik, Branching Quantifiers, Springer International Publishing, Cham, 2016, pp. 143–162. doi:10.1007/978-3-319-28749-2_9.
  * Hetzl et al. [2011] S. Hetzl, A. Leitsch, D. Weller,  CERES in higher-order logic,  Ann. Pure Appl. Log. 162 (2011) 1001–1034. doi:10.1016/J.APAL.2011.06.005.
  * Avigad and Zach [2008] J. Avigad, R. Zach,  The epsilon calculus,  in: E. N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information, 2008. URL: http://plato.stanford.edu/.
  * Chatzikyriakidis et al. [2017] S. Chatzikyriakidis, F. Pasquali, C. Retoré,  From logical and linguistic generics to Hilbert’s tau and epsilon quantifiers,  IfCoLog Journal of Logics and their Applications 4 (2017) 231–255.
  * Baaz and Lolic [2021] M. Baaz, A. Lolic,  Towards a proof theory for Henkin quantifiers,  J. Log. Comput. 31 (2021) 40–66. URL: https://doi.org/10.1093/logcom/exaa071.