State-based Modal Logics for Free Choice
State-based Modal Logics for Free Choice

Maria Aloni, Aleksi Anttila, and Fan Yang

Institute for Logic, Language and Computation & Philosophy

University of Amsterdam

Science Park 107

1098 XG Amsterdam

Department of Mathematics and Statistics

University of Helsinki

P.O. Box 4

00014 University of Helsinki

Department of Philosophy and Religious Studies

Utrecht University

Janskerkhof 13

3512 BL Utrecht

M. Aloni, A. Anttila, and F. Yang

We study the mathematical properties of bilateral state-based modal logic (BSML), a modal logic employing state-based semantics (also known as team semantics), which has been used to account for free choice inferences and related linguistic phenomena. This logic extends classical modal logic with a non-emptiness atom which is true in a state if and only if the state is empty. We introduce two extensions of BSML and show that the extensions are expressively complete, and we develop natural deduction axiomatizations for the three logics.

[Primary ]03B65 [; Secondary ]03B60 03B45

team semantics free choice modal logic

§ INTRODUCTION

In this paper, we study bilateral state-based modal logic ($\BSML$), a modal logic employing team semantics. was introduced in <cit.> to account for Free Choice ($\FC$) inferences. In $\FC$-inferences, conjunctive meanings  are unexpectedly derived from  disjunctive sentences:
. Free choice   <cit.>
. You may go to the beach or   to the

$\implicates$ You may go to the beach
and you may go to the cinema.
.̱  $\Diamond (b \vee c) \implicates \Diamond b \wedge \Diamond c$

The novel hypothesis at the core of the account in <cit.> is that $\FC$ and other related inferences are a consequence of a tendency in human cognition to disregard structures that verify sentences by virtue of some empty configuration (neglect-zero tendency) <cit.>. Models that verify sentences by virtue of an empty witness-set are called zero-models—see Figure <ref> for an illustration.

$\quad[\blacksquare, \blacksquare, \blacksquare]\quad$
$[\blacksquare, \square, \blacksquare]$
$[ \  ]$; $[\triangle, \triangle, \triangle]$; $[\Diamond, \blacktriangle, \spadesuit]$
Models for the sentence Every square is black.

is introduced as a framework allowing for the formalization of the neglect-zero tendency and the rigorous study of its impact on linguistic interpretation. It extends classical modal logic ($\ML$) with a special non-emptiness atom () requiring the adoption of team semantics. In team semantics (introduced originally in <cit.> and developed further in dependence logic <cit.>), formulas are interpreted with respect to sets of evaluation points called teams, rather than single points. In the type of modal team semantics employed by , teams are sets of possible worlds. In <cit.>, teams are also called states since they represent speakers' information states; we will use these terms interchangeably. The atom $\NE$ (introduced in <cit.>) is true (or supported) in a state iff the state is not empty: $s\vDash \NE$ iff $s\neq \emptyset$. This atom is used, in <cit.>, to define a pragmatic enrichment function $[\ ]^+$ whose core effect is to disallow zero-models; it is then shown that pragmatic enrichment yields non-trivial effects including the prediction (given certain preconditions) of both narrow-scope ($\Diamond (b \vee c) \implicates \Diamond b \wedge \Diamond c$) and wide-scope ($\Diamond b \vee \Diamond c \implicates \Diamond b \wedge \Diamond c$) $\FC$-inferences, as well as their cancellation under negation (see <ref> below). See Figure <ref> for illustrations of zero-models and the narrow-scope $\FC$-prediction in $\BSML$.[The state $\{w_q\}$ in Figure <ref> supports  $p \vee q$. This is because we can find substates of $\{w_q\}$ supporting each disjunct: $\{w_q\}$ itself supports $q$ and the empty state vacuously supports $p$. But $\{w_q\}$ is a zero-model for $p \vee q$ because no non-empty substate supports the first disjunct. Pragmatic enrichment has the effect of ruling out this zero-model—$\{w_q\}$ does not support $[p \vee q]^+$. The state $\{w_p,w_q\}$ in <ref> is a non-zero verifier for $p\vee q$, so it supports $[p \vee q]^+$. The state $\{w_\emptyset\}$ in <ref> is a zero-model for $\Di(p\lor q)$, and it does not support $\Di p\land \Di q$. The state $\{w_{pq}\}$, on the other hand, is a non-zero verifier for $\Di(p \lor q)$. We will see that such a verifier must also verify $\Di p\land \Di q$—in other words, narrow-scope $\FC$ is predicted by the fact that $[ \Di (p\lor q)]^+\vDash \Di p\land \Di q$. See Section <ref> for the definition of the pragmatic enrichment function and more details.] See <cit.> for more discussion and for comparisons with other accounts of $\FC$.

. Cancellation of $\FC$ under negation   <cit.> .  You are not allowed to eat the cake or the  ice-cream.

$\implicates$   You are not allowed to eat   either one. .̱   $\neg \Diamond  (\alpha \vee \beta)$ $\implicates$   $ \neg  \Diamond  \alpha \wedge \neg \Diamond  \beta $

[$\{w_q\}\nvDash \lbrack p \vee q \rbrack^{+}$; zero-model for $p\lor q$]

[opaque,rounded corners] (0.1,1.4) rectangle (1.4, .1);

[draw=gray] (-1.5,1.5) rectangle (1.5, -1.5);

(-0.75,.75) node[index gray, scale=0.9] (yy) $w_{p}$;
(0.75,.75) node[index gray, scale=0.9] (yn) $w_q$;
(-0.75,-0.75) node[index gray, scale=0.9] (ny) $w_{pq}$;
(0.75,-0.75) node[index gray, scale=0.9] (nn) $w_{\emptyset}$;

[$\{w_p,w_q\}\vDash \lbrack p \vee q \rbrack^{+}$; non-zero verifier for $p\lor q$]

[opaque,rounded corners] (-1.4,1.4) rectangle (1.4, .1);

[draw=gray] (-1.5,1.5) rectangle (1.5, -1.5);

(-0.75,.75) node[index gray, scale=0.9] (yy) $w_{p}$;
(0.75,.75) node[index gray, scale=0.9] (yn) $w_q$;
(-0.75,-0.75) node[index gray, scale=0.9] (ny) $w_{pq}$;
(0.75,-0.75) node[index gray, scale=0.9] (nn) $w_{\emptyset}$;

[$\{w_\emptyset\}\nvDash \lbrack \Di( p \vee q) \rbrack^{+}$; $\{w_{pq}\}\vDash \lbrack \Di( p \vee q) \rbrack^+$]

[opaque,rounded corners] (0.1,-0.1) rectangle (1.4, -1.4);
[opaque,rounded corners] (-1.4,-0.1) rectangle (-0.1, -1.4);

[draw=gray] (-1.5,1.5) rectangle (1.5, -1.5);

(-0.75,.75) node[index gray, scale=0.9] (yy) $w_{p}$;
(0.75,.75) node[index gray, scale=0.9] (yn) $w_q$;
(-0.75,-0.75) node[index gray, scale=0.9] (ny) $w_{pq}$;
(0.75,-0.75) node[index gray, scale=0.9] (nn) $w_{\emptyset}$;

[->] (nn) edge[](yn);
[->] (ny) edge[](yn);
[->] (ny) edge[](yy);

Zero-models and $\FC$ in $\BSML$. Worlds are labelled according to what is true in them: $w_p$ stands for a world where only $p$ is true, $w_{pq}$ for one in which only $p$ and $q$ are, etc. The accessibility relation is depicted using arrows.

$\BSML$ is closely related to modal logics in the lineage of dependence logic <cit.>, such as modal dependence <cit.>, inclusion <cit.>, independence <cit.>, and team <cit.> logic. It is also similar to modal inquisitive logic <cit.>. However, the specific combination of connectives ($\NE,\lor,\Di,\lnot$) on which the account of $\FC$ in <cit.> depends is unique to $\BSML$. Let us briefly discuss each of these in turn.

The most crucial component in the account of $\FC$ is the non-emptiness atom $\NE$. This atom also sets $\BSML$ apart from dependence and inquisitive logic in that formulas containing $\NE$ might not be downward closed and might not have the empty state (or empty team) property. Logics which violate these properties are commonly known as team logics (see, for example, <cit.>). Most team logics incorporate the Boolean negation $\sim$ ($s\vDash\sim \phi$ iff $s\nvDash \phi$). This negation is very strong in terms of expressive power: the extension of classical modal logic $\ML$ with $\sim$ (known as modal team logic ($\MTL$)) can express all modally definable state properties <cit.>. $\BSML$, being essentially $\ML$ together with $\NE$, is a more modest extension. The propositional fragment of $\BSML$ (that is, classical propositional logic extended with $\NE$) was studied already in <cit.>.

The disjunction $\dis$ in $\BSML$ is the standard disjunction in the dependence logic lineage, commonly referred to as the tensor disjunction or local disjunction. Inquisitive logic makes use of a different disjunction, the global disjunction $\intd$ (also known as the inquisitive disjunction).

\begin{align*}
&s\vDash \phi \lor \psi &&\text{iff} &&\text{there are }t,u\subseteq s \text{ s.t. }s=t\cup u \text{ and }t\vDash\phi \text{ and }u\vDash \psi  \\
&s\vDash \phi \intd \psi &&\text{iff} &&s\vDash \phi \text{ or }s\vDash \psi
\end{align*}

The predictions in <cit.> rely on the use of $\dis$, but it is interesting to note that similar accounts of $\FC$ have been given in inquisitive semantics, making use of $\intd$ instead of $\dis$—see, for example, <cit.>, and see <cit.> for a comparison.

The modalities $\Di$ and $\Bo$ of $\BSML$ (essential for the $\FC$-predictions) are equivalent to ones considered in an early version of modal inquisitive logic <cit.>, as well as to the modalities in possibility semantics <cit.>. They are distinct from the standard modalities of modal team semantics—we refer the reader to <cit.> for a comparison.

For its predictions involving negation (such as <ref>), $\BSML$ relies on a bilateral semantics (see, for example, <cit.>): in addition to support/assertion conditions each formula is also provided with anti-support/rejection conditions. The semantics of what we will call the bilateral negation $\lnot$ are then defined using the anti-support conditions. It should be noted that differs from bilateral systems such as Rumfitt's <cit.> in that the latter type of system makes use of a special rejection sign as well as a negation operator; in , this distinction is elided and the negation operator is interpreted as directly expressing rejection. The bilateral negation is essentially the same notion as the dual or game-theoretic negation of independence-friendly logic <cit.> and some formulations of dependence logic <cit.>.

In this paper, we study the logical properties of , as well as two new extensions of $\BSML$: $\BSML$ with the global disjunction $\intd$ ($\BSMLI$), and $\BSML$ with the novel emptiness operator $\OC$ ($\BSMLO$). The emptiness operator is a natural counterpart to $\NE$ which can be used to cancel out its effects: a state $s$ supports $\OC\phi$ iff $s$ supports $\phi$ or $s$ is empty ($s\vDash \OC\phi$ iff $s\vDash \phi$ or $s =\emptyset$), meaning that, for instance, $\OC\NE$ is always supported. While these extensions may prove to have interesting applications of their own (we return to this in the conclusion), our introduction of them is motivated primarily by technical considerations: as we show in the first part of the paper, each extension is expressively complete for a natural class of state properties. Moreover, in the second part of the paper, we axiomatize the logics, and our completeness proofs make essential use of the expressive completeness of the extensions.

In the first part, then, we focus on expressive power. We characterize the expressiveness of our logics in terms of the notion of state (or team) bisimulation as introduced in the literature on modal team semantics <cit.>. We show that $\BSMLI$ is expressively complete for the class of all state properties invariant under bounded bisimulation (meaning that $\BSMLI$ and $\MTL$ are equivalent in expressive power <cit.>), and that $\BSMLO$ is expressively complete for the class of all union-closed state properties invariant under bounded bisimulation. These results build on similar results in, for instance, <cit.>. $\BSML$, as we will demonstrate, is union closed but cannot express all union-closed properties.

In the second part, we develop natural deduction axiomatizations for all three logics. These systems build on systems presented in <cit.> for logics which are essentially the propositional fragments of $\BSML$ and $\BSMLI$. For other similar natural deduction axiomatizations for modal state-based logics, see, for instance, <cit.>.

The paper is structured as follows. In Section <ref>, we define the syntax and semantics of $\BSML$ and the extensions, and discuss some basic properties of these logics. In Section <ref>, we show the expressive power results described above. We also derive some simple consequences of these results such as the finite model property (for each of the logics) and uniform interpolation (for $\BSMLI$ and $\BSMLO$). In Section <ref>, we present our natural deduction axiomatizations, and in Section <ref> we conclude by noting some open problems. The paper is partly based on <cit.>, which contains preliminary versions of some of the results.

§ BILATERAL STATE-BASED MODAL LOGIC

In this section we define the syntax and semantics of $\BSML$ and its extensions, discuss the basic properties of the logics, and recall standard notions and results from team semantics.

Fix a (countably infinite) set $\mathsf{Prop}$ of propositional variables. The set of formulas of bilateral state-based modal logic $\BSML$ is generated by:

\begin{align*}
\phi ::= p \sepp \bnot \phi \sepp ( \phi \land \phi )  \sepp ( \phi \dis \phi ) \sepp \Di \phi   \sepp \NE
\end{align*}

where $p\in \mathsf{Prop}$.
Classical modal logic $\ML$ is the $\NE$-free fragment of $\BSML$.

$\BSMLI$ is $\BSML$ extended with the global disjunction $\intd$: the set of formulas of $\BSMLI$ is generated by the definition for $\BSML$ augmented with the case $\phi \intd \phi$.

$\BSMLO$ is $\BSML$ extended with the emptiness operator $\OC$: the set of formulas of $\BSMLO$ is generated by the definition for $\BSML$ augmented with the case $\OC\phi$.

Throughout the paper, we use the first Greek letters $\alpha,\beta,\gamma,\dots$ to stand for formulas of (also called classical formulas).
We write $\mathsf{P}(\phi)$ for the set of propositional variables in $\phi$ and $\phi (p_{1},\ldots ,p_{n})$ if $\mathsf{P}(\phi)\subseteq \{p_{1},\ldots ,p_{n}\}$. We write $\phi (\psi/p)$ for the result of replacing all occurrences of $p$ in $\phi$ by $\psi$.

A (Kripke) model (over $\mathsf{X}\subseteq \mathsf{Prop}$) is a triple $M = (W,R,V)$, where

– $W$ is a nonempty set, whose elements are called (possible) worlds;

– $R \subseteq W \times W$ is a binary relation, called the accessibility relation;

$V: \mathsf{X} \to \wp(W)$
is a function, called the valuation.

We call a subset $s\subseteq W$ of $W$ a state on $M$.

For any world $w$ in $M$, define, as usual, $R[w]:=\{v \in W\sepp wRv\}$. Similarly, for any state $s$ on $M$, define $R[s]:=\bigcup_{w\in s}R[w]$.

In the standard world-based semantics for modal logic, formulas are evaluated with respect to worlds: one writes $M,w\vDash \phi$ if $\phi$ is true in the world $w$ in the model $M$. In our state-based semantics, formulas are instead evaluated with respect to states. We will also make use of two fundamental semantic notions—support and anti-support—rather than one. As noted in Section <ref>, states in $\BSML$ represent speakers' information states. Support of a formula by (or in) a state represents that what the formula expresses is assertible given the information in the state; anti-support, similarly, represents rejectability in a state.

For a model $M=(W,R,V)$ over $\mathsf{X}$, a
state $s$ on $M$, and formula $\phi$ with $\mathsf{P}(\phi)\subseteq \mathsf{X}$, the notions of $\phi$ being supported/anti-supported by $s$ in $M$, written $M,s \vDash \phi$/$M,s\Dashv \phi$ (or simply $s \vDash \phi$/$s\Dashv \phi$), are defined recursively as follows:

$M,s \vDash   p$      $:\iff$     for all $ w \in s: w \in V(p)$

$M,s \Dashv  p  $    $:\iff$    for all $ w \in s: w \notin V(p)$

$M,s \vDash    \NE$    $ :\iff$   $ s \neq \emptyset$

$M,s \Dashv    \NE $   $ :\iff$   $ s =\emptyset$

$M,s \vDash    \bnot \phi$     $:\iff$     $M,s\Dashv \phi$

$M,s \Dashv    \bnot \phi $   $ :\iff $   $ M,s \vDash \phi $

$M,s \vDash    \phi \land \psi  $   $ :\iff $   $ M,s \vDash  \phi\text{ and } M,s \vDash \psi$

$M,s \Dashv    \phi \land \psi  $    $:\iff$    there exist $t,s$ s.t. $ s=t \cup u\text{ and } M,t \Dashv  \phi\text{ and } M,u \Dashv  \psi$

$M,s \vDash    \phi \dis \psi  $    $:\iff$    there exist $t,s $ s.t. $ s=t\cup u\text{ and } M,t \vDash  \phi\text{ and } M,u \vDash  \psi$

$M,s \Dashv    \phi \dis \psi  $   $ :\iff $   $ M,s \Dashv  \phi\text{ and } M,s \Dashv  \psi$

$M,s \vDash    \phi \intd \psi  $   $ :\iff$   $ M,s \vDash  \phi \text{ or } M,s \vDash  \psi$

$M,s \Dashv    \phi \intd \psi  $   $ :\iff$   $  M,s \Dashv  \phi\text{ and } M,s \Dashv  \psi$

$M,s \vDash    \Di \phi  $    $:\iff$    for all $ w \in s$ there exists $  t \subseteq R[w]$ s.t. $ t\neq \emptyset \text{ and }M,t \vDash \phi$

$M,s \Dashv    \Di \phi  $   $ :\iff$    for all $ w \in s : M,R[w]\Dashv \phi$

$M,s \vDash    \OC \phi  $    $:\iff$    $M,s\vDash \phi \text{ or }s=\emptyset$

$M,s \Dashv    \OC \phi  $    $:\iff$    $M,s\Dashv \phi $

For a set $\Phi$ of formulas, we write $M,s\vDash\Phi$ if $M,s \vDash \phi$ for all $\phi \in \Phi$. We say that $\Phi$ entails $\psi$, written $\Phi \vDash \psi$, if for all models $M$ and states $s$ on $M$:  $M,s \vDash \Phi$  implies $M,s\vDash \psi$. We also write simply $\phi_1,\dots,\phi_n\vDash\psi$ for $\{\phi_1,\dots,\phi_n\}\vDash\psi$, and $\Phi,\phi\vDash \psi$ for $\Phi\cup\{\phi\}\vDash \psi$. We write $\vDash\phi$ for $\emptyset \vDash \phi$ and in this case say that $\phi$ is valid. If both $\phi\vDash\psi$ and $\psi\vDash\phi$, then we write $\phi\equiv\psi$ and say that $\phi$ and $\psi$ are equivalent. If both $\phi \equiv \psi$ and $\lnot \phi \equiv \lnot \psi$, then $\phi$ and $\psi$ are said to be strongly equivalent, written $\phi \equivclosed \psi$.

The box modality $\Bo$ is defined as the dual of the diamond: $\Box \phi:=\lnot \Di\lnot \phi$; the resulting support/antisupport clauses are:

$M,s \vDash    \Bo \phi  $   $ \iff$   for all $ w \in s:  M,R[w]\vDash \phi$

$M,s \Dashv    \Bo \phi  $    $\iff$   for all $ w \in s$ there exists $ t \subseteq R[w]$ s.t. $ t\neq \emptyset \text{ and }M,t \Dashv \phi$

We also define a weak contradiction $\bot:=p \land \bnot p$ (for some fixed $p$), a strong contradiction $\Bot:=\bot \land \NE$, and a strong tautology $\Top:=p\lor \lnot p$. Clearly, the weak contradiction is supported only in the empty state, the strong contradiction in no state, and the strong tautology in all states. The atom $\NE$ (supported in all non-empty states) can  also be viewed as the weak tautology $\top$; accordingly, we let $\top:=\NE$. Note that we have the following equivalences:

\begin{align*}
&\lnot \bot \equiv \Top &&\lnot \Top \equiv \bot && \lnot \Bot \equiv \Top &&\lnot \top \equiv \bot
\end{align*}

These contradictions and tautologies also interpret the  empty disjunctions and conjunction:

\begin{align*}
&\bigdis \emptyset := \bot &&\bigintdd \hspace{-2pt} \emptyset := \Bot && \bigwedge \emptyset := \Top
\end{align*}

We now give some examples to illustrate the semantics—consider Figure <ref>. A (local) disjunction $\phi \lor \psi$ is supported in $s$ if $s$ can be split into two states $t$ and $u$ such that $t\vDash \phi$ and $u\vDash \psi$. Note that one or both of these substates might be empty; for instance, in <ref> we have $\{w_q\}\vDash p\lor q$. One can force these substates to be non-empty using $\NE$: we have $\{w_p,w_q\}\vDash (p\land \NE) \lor (q\land \NE)$. A global disjunction, on the other hand, is supported if either disjunct is supported: $\{w_q\}\vDash  (p\land \NE) \intd (q\land \NE)$, whereas $\{w_p,w_q\}\nvDash  (p\land \NE) \intd (q\land \NE)$. The emptiness operator $\OC$ is essentially a restricted variant of $\intd$ in that $\OC\phi \equiv \phi \intd \bot$: $\{w_q\}\vDash \OC (p\land \NE)\lor \OC (q\land \NE)$ and $\{w_p,w_q\}\vDash \OC (p\land \NE)\lor \OC (q\land \NE)$. $\Di \phi$ is supported in $s$ if for each world $w$ in $s$ there is a non-empty substate $t$ of the state of all worlds $R[w]$ accessible from $w$ that supports $\phi$; for example, in <ref> we have $s_b\vDash \Di q$ and $s_b\nvDash \Di p$. $\Bo\phi$ is supported in $s$ if for each $w\in s$, $R[w]$ as a whole supports $\phi$: $s_b\nvDash \Bo q$ and $s_b\vDash \Bo p \lor \Bo q$. It is easy to verify that the conjunction and (local) disjunction distribute over the global disjunction: $\phi\wedge(\psi\intd\chi)\equiv(\phi\wedge\psi)\intd(\phi\wedge\chi)$ and $\phi\vee(\psi\intd\chi)\equiv(\phi\vee\psi)\intd(\phi\vee\chi)$; whereas the modalities do not distribute over $\intd$, as, for example, $s_b \vDash \Bo (p \intd q)$ but $s_b \nvDash \Bo p \intd \Bo q$. We have instead $\Di (\phi \intd \psi)\equiv \Di \phi \lor \Di \psi$ and $\Bo (\phi \intd \psi)\equiv \Bo \phi \lor \Bo \psi$.

[$\{w_q\}\vDash p\lor q$; $\{w_{p},w_q\}\vDash (p\land \NE)\lor (q\land \NE)$]

[opaque,rounded corners] (-1.4,1.4) rectangle (1.4, .1);
[opaque,rounded corners] (0.2,1.3) rectangle (1.3, .2);

[draw=gray] (-1.5,1.5) rectangle (1.5, -1.5);

(-0.75,.75) node[index gray, scale=0.9] (yy) $w_{p}$;
(0.75,.75) node[index gray, scale=0.9] (yn) $w_q$;
(-0.75,-0.75) node[index gray, scale=0.9] (ny) $w_{pq}$;
(0.75,-0.75) node[index gray, scale=0.9] (nn) $w_{\emptyset}$;

[$s_b\vDash \Di q$]

[opaque,rounded corners] (0.-1.4,-0.1) rectangle (1.4, -1.4);

[draw=gray] (-1.5,1.5) rectangle (1.5, -1.5);

(-0.75,.75) node[index gray, scale=0.9] (yy) $w_{p}$;
(0.75,.75) node[index gray, scale=0.9] (yn) $w_q$;
(-0.75,-0.75) node[index gray, scale=0.9] (ny) $w_{pq}$;
(0.75,-0.75) node[index gray, scale=0.9] (nn) $w_{\emptyset}$;

[->] (nn) edge[](yn);
[->] (ny) edge[](yy);
[->,loop,looseness=4,in=30,out=330] (ny) edge[] (ny);

[$s_c\vDash \lbrack \Di( p \vee q) \rbrack^{+}$]

[opaque,rounded corners] (-1.4,-0.1) rectangle (-0.1, -1.4);

[draw=gray] (-1.5,1.5) rectangle (1.5, -1.5);

(-0.75,.75) node[index gray, scale=0.9] (yy) $w_{p}$;
(0.75,.75) node[index gray, scale=0.9] (yn) $w_q$;
(-0.75,-0.75) node[index gray, scale=0.9] (ny) $w_{pq}$;
(0.75,-0.75) node[index gray, scale=0.9] (nn) $w_{\emptyset}$;

[->] (ny) edge[](yn);
[->] (ny) edge[](yy);

Examples of the semantics

Let us also revisit the pragmatic enrichment function $[\ ]^+:\ML\to \BSML$ described in Section <ref>, which can now be formally and recursively defined as:

\begin{align*}
&[p]^+ &&:= &&p \land \NE&&\\
&[\medcircle \alpha]^+ &&:= && \medcircle([\alpha]^+) \land \NE&&\text{for }\medcircle\in \{\lnot,\Di,\Bo\}\\
&[\alpha \triangle \beta]^+ &&:= && ([\alpha]^+ \triangle [\beta]^+) \land \NE&&\text{for }\triangle\in \{\land,\lor\}
\end{align*}

It is easy to see that $[\ ]^+$ disallows zero-models as described in Section <ref>. Consider, for instance, $[p\lor q]^+=(p\land \NE)\lor (q\land \NE) \land \NE\equiv (p\land \NE)\lor (q\land \NE)$. The state $\{w_q\}$ is a zero-model for $p\lor q$ since $\{w_q\}\vDash p\lor q$ but $\{w_q\}\nvDash (p\land \NE)\lor (q\land \NE)$, whereas $\{w_p,w_q\}$ is a non-zero verifier since $\{w_p,w_q\}\vDash (p\land \NE)\lor (q\land \NE)$. For a formula $\Di(\alpha \lor \beta)$ as in the antecedent of a narrow-scope $\FC$-inference, we have $[\Di(\alpha \lor \beta)]^+\equiv \Di ((\alpha \land \NE) \lor (\beta \land \NE))\land \NE$. It is then also easy to see that $[\Di(\alpha \lor \beta)]^+\vDash \Di \alpha \land \Di \beta$—a non-zero verifier for $\Di (\alpha \lor \beta)$ must verify $\Di \alpha \land \Di \beta$. In Figure <ref>, $s_b$ is a zero-model for $\Di(p\lor q)$ and $s_c$ is a non-zero verifier: we have $s_b\vDash p\lor q$, $s_b\nvDash \Di((p\land \NE)\lor (q\land \NE))$, and $s_b\nvDash \Di p\land \Di q$; whereas $s_c\vDash \Di((p\land \NE)\lor (q\land \NE))$ and $s_c\vDash \Di p\land \Di q$.

Similarly to many other logics employing team semantics (see, for example, <cit.>), $\BSML$ and its extensions do not admit uniform substitution: $\phi(p)\vDash \psi(p)$ need not imply $\phi(\chi/p)\vDash \psi(\chi/p)$. For instance, we have $\vDash p\lor \lnot p$ and $p\lor p\vDash p$, whereas $\nvDash \NE\lor \lnot \NE$ and $(p\intd \lnot p)\lor (p\intd \lnot p)\nvDash p\intd \lnot p$.

Closely related is the failure of preservation of equivalence under replacement: $\phi\equiv \psi$ need not imply $\theta(\phi/p)\equiv\theta(\psi/p)$. For instance, we have $\lnot (\phi \lor \psi)\equiv \lnot (\phi \intd \psi)$ but $\lnot\lnot (\phi \lor \psi) \equiv\phi \lor \psi \notequiv  \phi \intd \psi \equiv\lnot \lnot (\phi \intd \psi)$, and $ \bot\equiv \lnot \NE$ but $ \lnot \bot\equiv \Top \notequiv \NE \equiv \lnot \lnot\NE$. This failure is occasioned by the bilateral negation: it is easy to show that if $p$ is not within the scope of $\lnot$, it does follow that $\theta(\phi/p)\equiv\theta(\psi/p)$. Strong equivalence, on the other hand, is preserved under replacement, as we prove in the following proposition (cf. a similar replacement theorem in <cit.>). We write $\phi[\chi]$ (or simply $[\chi]$) to refer to a specific occurrence of the subformula $\chi$ in $\phi$, and $\phi[\psi/\chi]$ for the result of replacing this occurrence of $\chi$ in $\phi$ with $\psi$. These notations are also extended to sequences of occurrences $\phi[\chi_1,\ldots ,\chi_n]$ and sequences or replacements $\phi[\psi_1/\chi_1,\ldots ,\psi_n/\chi_n]$ in the obvious way.

For any formulas $\theta,\phi$, and $\psi$, if $\phi \equivclosed \psi$, then $ \theta[\phi/p] \equivclosed \theta[\psi/p]$.

By induction on $\theta$. We only give a detailed proof for a few  interesting cases.

$\theta=\lnot \eta$.  By  the induction hypothesis, $\eta[\phi/p]\equivclosed \eta[\psi/p]$, so $\lnot \eta[\phi/p]\equiv \lnot \eta[\psi/p]$ and $\lnot \lnot \eta[\phi/p]\equiv \eta[\phi/p]\equiv \eta[\psi/p] \equiv \lnot \lnot \eta[\psi/p]$. Therefore, $\lnot \eta[\phi/p
]\equivclosed \lnot \eta[\psi/p]$.

$\theta=\Di\eta$. By the induction hypothesis, we have $\eta[\phi/p]\equivclosed\eta[\psi/p]$. To show $\Di \eta[\phi/p]\vDash \Di\eta[\psi/p]$, assume $s\vDash \Di \eta[\phi/p]$. Then for all $w\in s$ there is a non-empty $ t\subseteq R[w]$ such that $t\vDash \eta[\phi/p]$. But then also for each such $t$ we have $t\vDash \eta[\psi/p]$, so $s\vDash \Di \eta[\psi/p]$. The proof of $\Di \eta[\psi/p]\vDash \Di\eta[\phi/p]$ is analogous. To show $\lnot \Di \eta[\phi/p]\vDash \lnot \Di\eta[\psi/p]$, assume $s\vDash \lnot \Di \eta[\phi/p]$. Then $R[w]\vDash \lnot \eta[\phi/p]$ for all $w\in s$. But then also $ R[w]\vDash \lnot \eta[\psi/p]$ for all $w\in s$, so $s\vDash \lnot \Di \eta[\psi/p]$. The proof of $\lnot \Di \eta[\psi/p]\vDash \lnot \Di\eta[\phi/p]$ is analogous.

$\theta=\OC\eta$.  By the induction hypothesis, we have $\eta[\phi/p]\equivclosed\eta[\psi/p]$. Then $\OC \eta[\phi/p]\equiv \eta[\phi/p]\intd \bot\equiv \eta[\psi/p] \intd \bot\equiv \OC\eta[\psi/p]$ and $\lnot \OC \eta[\phi/p]\equiv \lnot\eta[\phi/p]\equiv\\ \lnot\eta[\psi/p] \equiv \lnot\OC\eta[\psi/p]$.

As usual, each formula in our logics can be turned into an equivalent one in negation normal form, that is, a formula in which negation occurs only in front of propositional variables $p$ and the atom $\NE$, and as part of the defined connective $\Bo$.

[Negation normal form]
For any formula $\phi$, there exists a formula
$\phi'$ in negation normal form such that  $\phi \equiv \phi'$. Moreover, if $\phi \in \BSML$, then $\phi\equivclosed\phi'$.

Follows easily from the following (strong) equivalences:

\begin{align*}
\lnot \lnot \phi&\equivclosed \phi    & \lnot (\phi\land \psi)&\equivclosed \lnot \phi \lor\lnot \psi &\lnot (\phi\intd \psi) &\equiv \lnot \phi \land\lnot \psi&\\
\lnot \Di \phi&\equivclosed \Bo \lnot \phi&\lnot (\phi\lor \psi)&\equivclosed \lnot \phi \land\lnot \psi & \lnot \OC \phi&\equiv \lnot \phi&\tag*{\qedhere}
\end{align*}

Throughout the paper, we make extensive use of the following properties:

We say that a formula $\phi$

– is downward closed, provided   $[M,s \vDash \phi \text{ and } t \subseteq s] \implies M,t \vDash \phi$;

– is union closed, provided $[M,s \vDash \phi \text{ for all } s\in S\neq \emptyset] \implies M, \bigcup S  \vDash \phi$;

– has the empty state property, provided $M, \emptyset \vDash \phi \text{ for all }M$;

– is flat, provided $M, s\vDash\phi  \iff M,\{w\}\vDash \phi\text{ for all }w\in s$.

It is easy to check that a formula is flat if and only if it is downwards closed, union closed, and has the empty state property. A simple induction shows:

If a formula $\phi$ does not contain $\NE$, then it is downward closed and has the empty state property. If $\phi$ does not contain $\intd$, then it is union closed.

In particular, formulas of and are union closed; formulas of are flat (as they are downward  and union closed, and have the empty state property).

It is also easy to verify that $\Di\phi$ and $\Bo \phi$ are always flat. It follows from the flatness of -formulas that the state-based semantics for $\ML$ correspond with the standard (single-world) semantics in the sense of the following fact:

For any formula $\alpha\in \ML$:

\begin{align*}
&M,s \vDash \alpha &&\iff &&M,\{w\}\vDash\alpha\text{ for all }w\in s&&\iff &&M,w \vDash \alpha \text{ for all }w \in s.
\end{align*}

The first equivalence follows from flatness, and the second from $\{w\}\vDash \alpha$ iff $w\vDash \alpha$ (proved by an easy induction).

As an immediate consequence of Fact <ref>, we have that for any set $\Delta \cup \{\alpha\}$ of $\ML$-formulas, $\Delta \vDash \alpha$ in the state-semantics sense iff $\Delta \vDash \alpha$ in the usual single-world-semantics sense. For this reason, when discussing $\ML$-formulas, we simply use the notation $\vDash$ to refer to both state-based and world-based entailment (similarly for $\equiv$).

§ EXPRESSIVE POWER AND NORMAL FORMS

In this section, we study the expressive power of and its extensions. We measure the expressive power of the logics in terms of the properties—sets of pointed models—they can express. It is well-known that the expressive power of classical modal logic $\ML$ is characterized by bisimulation-invariance: the properties expressible in $\ML$ are invariant (closed) under bisimulation. This also holds in the state-based modal setting: our logics are invariant under state bisimulation. In Section <ref>, we present state bisimulation and prove bisimulation-invariance; in Section <ref>, we apply this notion to show expressive completeness results for our logics.

§.§ Bisimulation

We recall briefly some standard results concerning bisimulation for classical modal logic and standard Kripke semantics; for more comprehensive discussions, we refer the reader to, for instance, <cit.>.

Throughout this section, we fix a set $\mathsf{X}$ of propositional variables. A pointed model (over $\mathsf{X}$) is a pair $(M,w)$ where $M$ is a model over $\mathsf{X}$ and $w\in W$.

Let $k \in \mathbb{N}$ and let $(M,w)$ and $(M',w')$ be pointed models. We write $M,w \bisim_k M',w'$ (or simply $w\bisim_k w'$) and say $(M,w)$ and $(M',w')$ are $k$-bisimilar if the following recursively defined relation holds:

– $M,w \bisim_0 M,w :\iff $ for all $p \in \mathsf{X}$ we have $M,w \vDash p$ iff $M',w' \vDash p$.

– $M,w \bisim_{k+1} M',w' :\iff M,w \bisim_0 M',w'$ and

* [forth] for all $v \in R[w]$ there is a $v' \in R' [w']$ such that $M,v \bisim_k M',v'$;

* [back] for all $v' \in R'[w']$ there is a $v \in R [w]$ such that $M,v \bisim_k M',v'$.

The modal depth $md(\phi)$ of a formula $\phi$ is defined recursively as:

– $md(p)=md(\NE)=0$

– $md(\bnot \phi)=md(\OC\phi)=md(\phi)$

– $md(\phi \land \psi)=md(\phi \dis \psi)=md(\phi \intd \psi)=max\{md(\phi),md(\psi)\}$

– $md(\Di \phi)= md(\phi)+1$

We say that $(M,w)$ and $(M,w')$ are $k$-equivalent ($k\in \mathbb{N}$), written $M,w \equiv_k M',w'$ (or simply $w\equiv_k w'$), if for all $\alpha \in \ML$ with $md(\alpha)\leq k$: $M,w\vDash \alpha \iff  M',w'\vDash \alpha$.

Let $k \in \N$ and let $(M,w)$ be a pointed model. We define the $k$-th Hintikka formula $\chi^{\mathsf{X},k}_{M,w} $ (or simply $\chi^k_{w} $) of $(M,w)$ recursively as:

\begin{align*}
&\chi^0_{w}   &&:= &&\bigwedge \{p \sepp p \in \mathsf{X} , w \in V(p)\} \land \bigwedge \{\lnot p \sepp p \in \mathsf{X} , w \notin V(p)\}\\
&\chi^{k+1}_{w} &&:= &&\chi^{k}_{w}
\land \underset{v \in R[w]}{\bigwedge}\Di \chi^{k}_{v}
\land \Bo \underset{v \in R[w]}{\bigdis}\chi^{k}_{v}
\end{align*}

(see, for instance, <cit.>.

\begin{align*}
&w \equiv_k w'  &&\iff &&w \bisim_k w' &&\iff   &&w'\vDash \chi^{k}_{w} && \iff && \chi^k_w \equiv \chi^k_{w'}
\end{align*}

In the context of standard Kripke semantics, we measure the expressive power of a logic in terms of the classes of pointed models expressible in the logic:

A property (over $\mathsf{X}$) is a set of pointed models over $\mathsf{X}$. Each formula $\alpha$ expresses a property (over $\mathsf{X}\supseteq \mathsf{P}(\phi)$)

$$\llbracket \alpha \rrbracket_{\mathsf{X}}:=\{(M,w)\text{ over $\mathsf{X}$}\sepp M,w\vDash \alpha\}.$$

We often drop the subscript $\mathsf{X}$ and write simply $\llbracket \alpha \rrbracket$. We say a logic $L$ is expressively complete for a class of properties $\mathbb{P}$ if $\mathbb{P}$ is the class of properties expressible by formulas of $L$, that is, if

$$\mathbb{P}=\llbracket L\rrbracket :=\{\llbracket \alpha \rrbracket\sepp \alpha \in L\}.$$

We say that a property $\PPP$ is invariant under $k$-bisimulation if $(M,w)\in \PPP$ and $M,w\bisim_k M',w'$ imply $(M',w')\in \PPP$. Theorem <ref> allows us to prove a world-based expressive completeness theorem for $\ML$: $\ML$ can express all world-based properties that are invariant under bounded bisimulation.

$$\llbracket \ML\rrbracket =\{\text{property }\PPP\sepp \PPP \text{ is invariant under $k$-bisimulation for some $k\in \mathbb{N}$}\}.$$

For the inclusion $\subseteq$, for any $\alpha\in \ML$, we have that $\llbracket\alpha \rrbracket$ is invariant under $k$-bisimulation for $k=md(\alpha)$ by Theorem <ref>. For the converse inclusion $\supseteq$, for any $\PPP$ invariant under $k$-bisimulation, it follows easily from Theorem <ref> that

$$M',w'\vDash \bigdis_{(M,w)\in \PPP} \chi^k_w \iff (M',w')\in \PPP \quad \text{(i.e., }\PPP=\llbracket \bigdis_{(M,w)\in \PPP} \chi^k_w\rrbracket\in \llbracket \ML \rrbracket).$$

Note that since there are only finitely many non-equivalent Hintikka formulas $\chi^k_w$ for a given $\mathsf{X}$, we may assume the disjunction in the above formula $\bigdis_{(M,w)\in \PPP} \chi^k_w$ is finite and hence that the formula is well-defined.

The formula $\bigdis_{(M,w)\in \PPP} \chi^k_w$ in the above proof can be viewed as a characteristic formula for $\PPP$. The proof also yields a disjunctive normal form for formulas of $\ML$: given that $\llbracket\alpha\rrbracket$ is invariant under $k$-bisimulation for $k=md(\alpha)$, $\llbracket\alpha \rrbracket=\llbracket \bigdis_{(M,w)\in \llbracket\alpha\rrbracket} \chi^{md(\alpha)}_w\rrbracket$, that is, $\alpha \equiv \bigdis_{(M,w)\in \llbracket\alpha\rrbracket} \chi^{md(\alpha)}_w$.

We now introduce state-based analogues of the preceding notions and results. A pointed (state) model (over $\mathsf{X}$) is a pair $(M,s)$ where $M$ is a model over $\mathsf{X}$ and $s$ is a state on $M$. For a given $k\in \mathbb{N}$, $(M,s)$ and $(M,s')$ are $k$-equivalent, written $M,s \equiv_k M',s'$, if for all $\phi$ with $md(\phi)\leq k: M,s\vDash \phi \iff M',s'\vDash \phi$.

State-based bisimulation (introduced first in <cit.>) is a natural generalization of the world-based notion: two pointed state models are bisimilar if for each world in one there is a bisimilar world in the other, and vice versa.

For any $k \in \mathbb{N}$, $(M,s)$ and $(M',s')$ are $k$-bisimilar, written $M,s \bisim_k M',s'$ (or simply $s\bisim_k s'$), if

– [forth] for each $w \in s$ there is some $w' \in s'$ such that $M,w \bisim_k M',w'$;

– [back] for each $w' \in s'$ there is some $w \in s$ such that $M,w \bisim_k M',w'$.

State bisimulation is clearly a conservative extension of the world-based bisimilation in that $\{w\}\bisim_k\{w'\}$ iff $w\bisim_kw'$. We thus use the same symbol $\bisim_k$  for both world-based and state based bisimulation, and we sometimes write simply $w\bisim_ks'$ for $\{w\}\bisim_ks'$. It is also easy to see that for any $k \in \N$, if $s \bisim_k s'$, then $s \bisim_n s'$ for all $n < k$ (for $w\bisim_k w'$ similarly implies $w \bisim_n w'$ for all $n< k$).

We list below some useful properties of state bisimulation;  see <cit.> for a proof.

If $s \bisim_{k+1} s'$, then:

currentlabel(i) $R[s] \bisim_k R'[s'] $;

currentlabel(ii) for all $t,u \subseteq s$ such that $s=t\cup u$ there are $t',u' \subseteq s'$ such that $s'= t'\cup u'$, $t\bisim_{k+1} t'$, and $u\bisim_{k+1} u'$.

As expected, state $k$-bisimilarity implies $k$-equivalence:

If $s\bisim_k s'$, then $s\equiv_k s'$.

For any $\phi$, we show by induction on  $\phi$ that  if $s\bisim_k s'$ for $k=md(\phi)$, then $s \vDash \phi$ iff $s'\vDash \phi$. By Fact <ref>, we may assume that $\phi$ is in negation normal form. Most cases can be found in <cit.>; note that the $\dis$-case follows by Lemma <ref> <ref>.
The case $\phi=\OC \psi$ follows by $\OC\psi\equiv \psi \intd \bnot \NE$ and the other cases. We now show the cases for the modalities. We only give the detailed proof for one direction of each implication.

$\phi=\Di \psi$. Suppose $s \bisim_k s'$ for $k= md(\Di\psi)=md(\psi)+1$, and  $s \vDash \Di \psi$. Let $w'\in s'$. By $s \bisim_k s'$, there is some $w\in s$ such that $w \bisim_k w'$. Since $s\vDash \Di \psi$, there is a non-empty $t \subseteq R[w]$ such that $t \vDash \psi$. By $w \bisim_k w'$ we obtain $R[w]\bisim_{k-1} R'[w']$ by Lemma <ref> <ref>. Then by Lemma <ref> <ref> there is some $t'\subseteq R'[w']$ such that $t\bisim_{k-1} t'$. By induction hypothesis, $t'\vDash \psi$. Since $t\neq \emptyset$ and $t \bisim_{k-1}t'$, we also have $t'\neq \emptyset$. Hence, $s' \vDash \Di \psi$.

$\phi=\Bo \psi$. Suppose $s \bisim_k s'$ for $k= md(\Bo\psi)=md(\psi)+1$, and $s \vDash \Bo \psi$. Let $w' \in s'$. By $s \bisim_k s'$, there is a $w\in s$ such that $w \bisim_k w'$. Since $s\vDash \Bo \psi$, we have $R[w]\vDash \psi$. By $w \bisim_k w'$ we obtain $R[w]\bisim_{k-1} R'[w']$ by Lemma <ref> <ref>. Then by induction hypothesis, $R'[w']\vDash \psi$, so $s' \vDash \Bo \psi$.

§.§ Expressive completeness

We move on to the main results concerning the expressive power of our logics. In the classical world-based setting we measured the expressive power of a logic in terms of classes of pointed models expressible in the logic; we now use classes of pointed state models.

A state property (over $\mathsf{X}$) is a set of pointed state models over $\mathsf{X}$. Each formula $\phi$ expresses a property (over $\mathsf{X}\supseteq \mathsf{P}(\phi)$)

$$||\phi||_{\mathsf{X}}:=\{(M,s)\text{ over }\mathsf{X}\sepp M,s \vDash \phi\}.$$

We say a logic $L$ is expressively complete for a class of properties $\mathbb{P}$ if $\mathbb{P}$ is the class of properties expressible by formulas of $L$, that is, if

$$\mathbb{P}=||L||:=\{||\phi|| \sepp \phi \in L\}.$$

We say that a state property $\PPP$  is invariant under $k$-bisimulation ($k\in \N$) if

\[[M,s\bisim_k M',s'] \implies (M',s')\in \PPP ,\]

and $\PPP$  is invariant under  bounded bisimulation if   $\PPP$  is invariant under $k$-bisimulation for some $k\in \N$. Similarly, $\PPP$  is union closed if
\[[(M,s)\in \PPP \text{ for all } s\in S\neq \emptyset] \implies (M, \bigcup S  )\in \PPP,\]

and $\PPP$ is flat if

\[(M, s)\in \PPP  \iff (M,\{w\})\in \PPP \text{ for all }w\in s .\]

Clearly, $\PPP$ is flat iff $\PPP$ is union closed and downward closed (i.e., $(M,s)\in \PPP$ and $t \subseteq s$ imply $(M,t)\in \PPP$), and has the empty state property (i.e., $(M,\emptyset)\in \PPP$ for all $M$).

We aim to show three results. First, is expressively complete for

$$\mathbb{B}:=\{\PPP\sepp \PPP\text{ is invariant under bounded bisimulation}\}.$$

Second, is complete for

$$\mathbb{U}:=\{\PPP\sepp \PPP\text{ is union closed and invariant under bounded bisimulation}\}.$$

Third, although properties expressed by formulas of are union closed and invariant under bounded bisimulation, is not complete for $\mathbb{U}$. Using the concepts we introduced it is also easy to show that $\ML$ is expressively complete for
$$\mathbb{F}:=\{\PPP\sepp \PPP\text{ is flat and invariant under bounded bisimulation}\}.$$

We include below a brief proof of this folklore result as it is instructive to see the result alongside the other expressive completeness theorems. Summing up, we have:

$$|| \ML || \subset ||\BSML  ||\subset  ||\BSMLO  ||\subset ||\BSMLI ||.$$

We begin by using Hintikka formulas $\chi^k_w \in \ML$ for pointed models to construct Hintikka formulas $\chi^k_s\in \ML$ and $\theta^k_s\in \BSML$ for pointed state models.

Let $\mathsf{X}\subseteq \mathsf{Prop}$.  For any pointed state model $(M,s)$ and any $k \in \N$, the $k$-th Hintikka formula $\chi^{\mathsf{X},k}_{M,s}$ (or simply $\chi_s^k$) and the $k$-th strong Hintikka formula $\theta^{\mathsf{X},k}_{M,s}$ (or simply $\theta_s^k$) of $(M,s)$ are defined as follows:

\begin{align*}
\chi^k_{s}&:=\displaystyle\bigvee_{w\in s}\chi^k_{w},\\
\theta^k_{s}&:=\displaystyle\bigvee_{w\in s}(\chi^k_{w}\land \NE)
\end{align*}

where we stipulate that $\bigvee\emptyset=\bot$.

Note that since there are only finitely many non-equivalent $\chi^k_w$ for a given $\mathsf{X}$, we may assume the disjunctions in $\theta^k_s$ and $\chi^k_w$ are finite, and hence the formulas are well-defined. These formulas function as characteristic formulas for states in the sense of the following proposition.

currentlabel(i) $M',s' \vDash \chi^{k}_{s} \iff $ there is a state $t\subseteq s$ such that $M,t\bisim_k M',s'$.

currentlabel(ii) $M',s' \vDash \theta^{k}_{s} \iff M,s \bisim_k M',s'$.

We prove the two items simultaneously. If $s=\emptyset$, then $\theta^{k}_{\emptyset}=\chi^{k}_{\emptyset}=\bot$, and
$s'\vDash \bot \iff s'=\emptyset \iff s\bisim_k s' \iff \exists t\subseteq s:t\bisim_k s' $. Now assume that $s \neq \emptyset$.

$\Longleftarrow$: We first prove <ref>. Suppose $t\bisim_k s'$ for some $t\subseteq s$. Then for any $w'\in s'$, there exists $w\in t\subseteq s$ such that $w \bisim_k w'$, which, by Theorem <ref>, implies that $w' \vDash \chi^{k}_{w}$ and so $w'\vDash \chi_s^k$. Since the classical formula $\chi_s^k$ is flat (Fact <ref>), we conclude that $s'\vDash\chi_s^k$.

For <ref>, suppose $s \bisim_k s'$. First observe that the back condition for  $s \bisim_k s'$ implies that there is some $t\subseteq s$ such that $t\bisim_k s'$. Thus, by  <ref>, we have $s'\vDash\chi_s^k$, which means that for every $w\in s$, there exists $s'_w\subseteq s'$ such that $s'=\bigcup_{w\in s}s'_w$ and $s'_w\vDash\chi_w^k$. Meanwhile, by the forth condition for $s \bisim_k s'$, we know that for every $w\in s$, there exists $w'\in s'$ such that $w\bisim_kw'$, which implies $w'\vDash \chi_w^k$ by Theorem <ref>.  Thus, we may w.l.o.g. assume that each $s_w'\neq \emptyset$ (for we can simply include the world $w'$ in $s_w'$), giving that $s_w'\vDash\chi_w^k\wedge \NE$. Hence, $s'\vDash\theta_s^k$.

$\Longrightarrow$: For <ref>, suppose $s'\vDash\chi_s^k$. Then, for each $w\in s$, there exists a subset $s_w'\subseteq s'$ such that $s'=\bigcup_{w \in s}s_w'$ and $s_w' \vDash \chi^{k}_{w}$. By the empty state property of classical formulas and Theorem <ref>, we have that either $s_w'=\emptyset$ or $w\bisim_ks_w'$. Let $t=\{w\in s\mid s_w'\neq \emptyset\}\subseteq s$. Clearly, the forth condition for $t\bisim_ks'$ is satisfied. To verify the back condition, observe that for any $v'\in s'=\bigcup_{w \in s}s_w'$, there exists $w\in s$ such that $v'\in s_w'\neq \emptyset$. Thus, $w\in t$ and $w\bisim_ks'_w$, whereby $w\bisim_kv'$.

For <ref>, suppose $s'\vDash\theta_s^k$. Then, for every $w\in s$, there exists $s_w'\subseteq s'$ such that $s'=\bigcup_{w \in s}s_w'$ and  $s_w' \vDash \chi^{k}_{w}\wedge\NE$. We then have $s_w'\neq \emptyset$ and $w\bisim_ks'$ (by Theorem <ref> again). Analogous to the above proof for <ref>, we define $t=\{w\in s\mid s_w'\neq \emptyset\}\subseteq s$ and obtain $t\bisim_ks'$ by the same argument. But since now each $s_w'\neq \emptyset$, we have actually $t=s$ and thus $s\bisim_ks'$.

The formulas $\chi^k_s$ are discussed also in <cit.>, and the formulas $\chi^k_s$ and $\theta^k_s$ are modal versions of the propositional characteristic formulas defined in <cit.>. Table <ref> presents a summary of the different characteristic formulas we consider.

Hintikka formula     Logic     Characterization effect     Defined in

$\chi^k_w$     $\ML$     $w'\vDash \chi^k_w \iff w\bisim_k w'$     Definition <ref>

$\chi^k_s=\bigdis_{w\in s}\chi^k_w$     $\ML$     $s'\vDash \chi^k_s \iff t\bisim_k s'$ for some $t\subseteq s$     Definition <ref>

$\theta^k_s=\bigdis_{w\in s}(\chi^k_w\land \NE)$     $\BSML$     $s'\vDash \theta^k_s \iff s\bisim_k s'$     Definition <ref>

Normal form     Logic     Characterization effect     Defined in

$\nu^k_\PPP=\bigdis_{(M,s)\in \PPP}\chi^k_s$     $\ML$     $M,s\vDash \nu^k_\PPP \iff (M,s)\in \PPP \text{ (}\PPP \in \mathbb{F})$     Definition <ref>

$\xi^k_\PPP=\bigintd_{(M,s)\in \PPP}\theta^k_s$     $\BSMLI$     $M,s\vDash \xi^k_\PPP \iff (M,s)\in \PPP \text{ (}\PPP \in \mathbb{B})$     Definition <ref>

$\zeta^k_\PPP=\bigdis_{(M,s)\in \PPP} \OC \theta^k_s$     $\BSMLO$     $M,s\vDash \zeta^k_\PPP \iff (M,s)\in \PPP \text{ (}\PPP \in \mathbb{U}^\emptyset\subseteq \mathbb{U})$     Definition <ref>

$\NE\land \zeta^k_\PPP$     $\BSMLO$     $M,s\vDash \NE \land  \zeta^k_\PPP\iff (M,s)\in \PPP \text{ (}\PPP \in \mathbb{U}^{\NE}\subseteq \mathbb{U})$     Definition <ref>

Characteristic formulas

Table <ref> also illustrates the main results in the remaining part of this section: we will use Hintikka formulas $\chi^k_s$ and $\theta^k_s$ for states to construct characteristic formulas for different types of state properties, and the formula for a given type of property will, in turn, be used to show that the logic it belongs to is expressively complete with respect to that type of property. Each of the property characteristic formulas also exemplifies the disjunctive normal form for the logic in question. Similar disjunctive normal forms  are studied in the modal context in, for example, <cit.>; and in the propositional context in, for example, <cit.>.

We now give the proofs of our expressive completeness results in order. We start with a folklore result that $\ML$ is complete for $\mathbb{F}$. Hereafter, we often abbreviate a pointed state model $(M,s)$ in a property $\PPP$ simply as $s$.

For any $\PPP\in \mathbb{F}$ and $k\in \mathbb{N}$, the $k$-th characteristic formula $\nu^k_\PPP\in \ML$ of $\PPP$ is defined as follows:

$$\nu^k_\PPP:=\bigdis_{s\in \PPP}\chi^k_s$$

$$||\ML||=\mathbb{F}:=\{\mathcal{P}\sepp \mathcal{P}\text{ is flat and invariant under bounded bisimulation}\}.$$

The inclusion $\subseteq$ follows from Theorem <ref> and Fact <ref>. For the converse inclusion $\supseteq$, we show that for any $\PPP\in \mathbb{F}$ invariant under $k$-bisimulation:

$$M',s'\vDash \bigdis_{(M,s)\in \PPP}\chi^k_s\iff (M',s')\in \PPP\quad \text{(i.e., $\PPP=||\nu^k_\PPP||\in || \ML ||$).}$$

$\Longleftarrow$: Suppose $(M',s') \in \PPP$. Since $s'\bisim_k s'$, we have $M',s' \vDash \chi^k_{s'}$ by Proposition <ref><ref>, which implies $M',s' \vDash \bigdis_{(M,s)\in \PPP}\chi^k_s$ by the empty state property of $\chi_s^k$.

$\Longrightarrow$: Suppose $M',s' \vDash \bigdis_{(M,s)\in \PPP}\chi^k_s$. If $s'=\emptyset$, then $(M',s')\in \PPP$, as $\PPP$ has the empty state property. Now, assume  $s'\neq\emptyset$. For each $(M,s)\in \PPP$, there exists $t_s'\subseteq s'$ such that $s'=\bigcup_{(M,s)\in \PPP}t_s'$ and $t_s'\vDash \chi_s^k$. The latter means, by Proposition <ref><ref>, that there exists $t\subseteq s$ such that $t_s'\bisim_kt$. Since $\mathbb{F}$ is downward closed and closed under $k$-bisimulation, we have $t_s'\in \PPP$. Finally, since $\mathbb{F}$ is  union closed, we conclude  $s'=\bigcup_{(M,s)\in \PPP}t_s'\in \PPP$.

The theorem also yields an alternative normal form for formulas in $\ML$: For an arbitrary $\ML$-formula $\alpha$, since $||\alpha||$ is invariant under $k$-bisimulation for $k=md(\alpha)$, we have $||\alpha||=||\nu_{||\alpha||}^{md(\alpha)}||$, that is, $\alpha \equiv \bigdis_{s\in ||\alpha||}\chi^{md(\alpha)}_s$.

Next, we  show the first of our main results: $\BSMLI$ is complete for $\mathbb{B}$, and is thus the expressively strongest logic. The proof is similar to the one given for $\ML$ and $\mathbb{F}$, but the addition of $\NE$ and $\intd$ allow us to fully characterize states and to capture all properties invariant under bounded bisimulation.

For any $\PPP\in \mathbb{B}$ and $k\in \mathbb{N}$, the $k$-th characteristic formula $\xi^k_\PPP\in \BSMLI$ of $\PPP$ is defined as follows:

$$\xi^k_\PPP:=\bigintdd_{s\in \PPP}\theta^k_s$$

where we stipulate $\bigintd\emptyset=\Bot$, and the formula is well-defined as there are only finitely many non-equivalent $\theta^k_s$ for a given $\mathsf{X}$.

$$||\BSMLI||=\mathbb{B}=\{\PPP\sepp \PPP\text{ is invariant under bounded bisimulation}\}$$

The inclusion $\subseteq$ follows from Theorem <ref>. For the nontrivial inclusion $\supseteq $, we show that for any $\PPP\in\mathbb{B}$ invariant under $k$-bisimulation:
$$M',s'\vDash \bigintdd_{(M,s)\in \PPP}\theta^k_s\iff (M',s')\in \PPP\quad\text{(i.e., }\PPP=||\xi^k_\PPP||\in ||\BSMLI||).$$

If $\PPP=\emptyset$, then $\xi^k_\PPP=\Bot$, and thus $\PPP=||\Bot||=||\xi^k_\PPP||$. Now, suppose $\PPP\neq \emptyset$. If $M',s' \vDash \xi^k_\PPP$, then $M',s' \vDash \theta^{k}_{s}$ for some $(M,s) \in \PPP$. By Proposition <ref><ref>, we have $s \bisim_k s'$, which implies $(M',s')\in \PPP$ by closure under $k$-bisimulation.

Conversely, if $(M',s')\in \PPP$, since $s'\bisim_k s'$, we have $M',s' \vDash \theta^k_{s'}$ by Proposition <ref><ref> and so $M',s' \vDash \xi^k_\PPP$.

As above, this also provides us with a disjunctive normal form: for each $\BSMLI$-formula $\phi$: $||\phi||=||\xi^{md(\phi)}_{||\phi||}||$, that is, $\phi \equiv \bigintd_{s\in ||\phi||}\theta^{md(\phi)}_s$.

The expressive completeness of $\BSMLO$ for $\mathbb{U}$ is proved in a similar way, but there is a small twist in this case. First define:

\begin{align*}
\mathbb{U}^\emptyset&:=\{\PPP\in \mathbb{U}\sepp \PPP\text{ has the empty state property}\}\\
\mathbb{U}^{\NE}&:=\{\PPP\in \mathbb{U}\sepp \PPP\text{ does not have the empty state property}\}
\end{align*}

So that $\mathbb{U}=\mathbb{U}^\emptyset\cup \mathbb{U}^{\NE}$. Note that if $\PPP\in \mathbb{U}^{\NE}$ so that for some $M$ we have $(M,\emptyset)\notin \PPP$, then in fact by closure under $k$-bisimulation $(M',\emptyset)\notin \PPP$ for all $M'$.

For any $\PPP\in \mathbb{U}$ let $k\in \N$ be such that $\PPP$ is invariant $k$-bisimulation. Let

\begin{align*}
&\zeta^{k}_\PPP:=\bigdis_{s\in \PPP}\OC\theta^{k}_{s}
\end{align*}

If $\PPP\in \mathbb{U}^\emptyset$, the characteristic formula of $\PPP$ is $\zeta^{k}_\PPP$. If $\PPP\in \mathbb{U}^\emptyset$, the characteristic formula of $\PPP$ is $\NE\land \zeta^{k}_\PPP$.

$$||\BSMLO||=\mathbb{U}=\{\PPP\sepp \PPP\text{ is union closed and invariant under bounded bisimulation}\}.$$

The inclusion $\subseteq$ follows from Fact <ref> and Theorem <ref>. For the nontrivial inclusion $\supseteq$, we first show that for any $\PPP\in\mathbb{U}^\emptyset$ invariant under $k$-bisimulation,

$$M',s'\vDash \bigdis_{(M,s)\in \PPP}\OC\theta^{k}_{s}\iff (M',s')\in \PPP\quad\text{(i.e., $\PPP=||\zeta^{k}_\PPP||\in ||\BSMLO||$).}$$

For $\Longleftarrow$, suppose $(M',s')\in \PPP\in \mathbb{U}^\emptyset$. Since $s'\bisim_k s'$, by Proposition <ref> <ref>, we have $M,s'\vDash \theta^k_{s'}$, whereby $M',s'\vDash\oslash \theta^k_{s'}$. Hence, $M',s'\vDash \bigdis_{(M,s)\in \PPP}\OC\theta^{k}_{s}$.

For $\Longrightarrow$, suppose $M',s'\vDash \bigdis_{(M,s)\in \PPP}\oslash\theta^k_{s}$. If $s'=\emptyset$, then $(M,s')\in \PPP$, as $\PPP \in\mathbb{U}^\emptyset$ has the empty state property. Now, assume that $s'\neq\emptyset$. Then, for every $(M,s)\in \PPP$, there exists $t_s'\subseteq s'$ such that $s'=\bigcup_{(M,s)\in \PPP}t_s'$ and $t_s'\vDash \oslash\theta^k_{s}$. The latter implies, by Proposition <ref> <ref>, that $t_s'=\emptyset$ or $t_s'\bisim_k s$. Since $\PPP$ is closed under $k$-bisimulation, each $(M,t_s')\in \PPP$. Finally, since $\PPP$ is union closed, we conclude $s'=\bigcup_{(M,s)\in \PPP}t_s'\in \PPP$.

Next, we show that for any $\PPP\in\mathbb{U}^{\NE}$ invariant under $k$-bisimulation,

$$M',s'\vDash \NE \land \bigdis_{(M,s)\in \PPP}\OC\theta^{k}_{s}\iff (M',s')\in \PPP\quad\text{(i.e., $\PPP=||\NE\land \zeta^{k}_\PPP||\in ||\BSMLO||$).}$$

For $\Longleftarrow$, suppose $(M',s')\in \PPP\in \mathbb{U}^{\NE}$. By the same argument as in the above case, we obtain $M',s'\vDash \bigdis_{(M,s)\in \PPP}\OC\theta^{k}_{s}$. Moreover, since $\PPP\in \mathbb{U}^{\NE}$, we have $s'\neq \emptyset$ so $s'\vDash \NE$. In conclusion, $M',s'\vDash \NE\wedge \bigdis_{(M,s)\in \PPP}\OC\theta^{k}_{s}$.

For $\Longrightarrow$, , if $M',s'\vDash\NE\land  \bigdis_{(M,s)\in P}\oslash\theta^k_{s}$, then $s'\neq \emptyset$, and by the same argument as in the proof above, we obtain  $(M',s')\in\PPP\in\mathbb{U}^{\NE}$ as well.

Again the proof yields a disjunctive normal form: for any $\BSMLO$-formula $\phi$, either $\phi\equiv \zeta^{md(\phi)}_{||\phi||}$ or $\phi\equiv\NE\land \zeta^{md(\phi)}_{||\phi||}$.

Finally, let us also point out that while $\BSML$ is union closed and invariant under bisimulations, it is not complete for $\mathbb{U}$. To prove this, we show first that for -formulas, the empty state property implies the downward closure property. Note that while converse might also appear to hold, it does not—for instance, the formula $\Bot$ is downward closed but does not have the empty state property.

For any $\phi\in\BSML$, if $\phi$ has the empty state property, then $\phi $ is downward closed.

By induction on $\phi$ (assumed to be in negation normal form). We only show the nontrivial cases.

Let $\phi = \psi \land \chi$. If $M,\emptyset \vDash \psi \land \chi$, then $M,\emptyset\vDash \psi$ and $M,\emptyset\vDash \chi$. By the induction hypothesis, $\psi$ and $\chi$ are downward closed. So if $s\vDash \psi \land \chi$ and $t\subseteq s$, then $t\vDash \psi$ and $t \vDash \chi$, and therefore $t\vDash \psi \land \chi$.

Let $\phi = \psi \dis \chi$. If $M,\emptyset \vDash \psi \dis \chi$, then clearly $M, \emptyset\vDash \psi$ and $M,\emptyset\vDash \chi$. By the induction hypothesis, $\psi$ and $\chi$ are downward closed. If $s\vDash \psi \dis \chi$, and $t\subseteq s$, then there are $s_1,s_2$ such that $s=s_1\cup s_2$, $s_1\vDash \psi$ and $s_2\vDash \chi$. By downward closure we have $t\cap s_1\vDash \psi$ and $s\cap t_2 \vDash \chi$ and therefore $t=(t\cap s_1)\cup (t\cap s_2)\vDash \psi \dis \chi$.

[$\BSMLBF$ is not expressively complete for $\mathbb{U}$]

$$||\BSML||\subset \mathbb{U}=\{\PPP\sepp \PPP\text{ is invariant under bounded bisimulation and union closed}\}.$$

The inclusion $\subseteq$ follows from Fact <ref> and Theorem <ref>. For inequality, let
$$\PPP:=||(p\land \NE)\lor (\lnot p \land \NE)||\cup ||\bot||.$$
Clearly $\PPP\in \mathbb{U}$. Assume for contradiction that  $||\phi ||=\PPP$ for some $\phi$ in $\BSML$. Then $\phi$ has the empty state property so  is downward closed by Lemma <ref>. Let $(M,s)\in || (p \land \NE) \dis (\bnot p \land \NE)||\subseteq \PPP$. Then there are $t,u$ such that $s=t\cup u$, $t\vDash p \land \NE$, and $u\vDash \bnot p \land \NE$. By $||\phi ||=\PPP$, we have $s\vDash \phi$. By downward closure, $t\vDash \phi$, so $(M,t)\in \PPP$. But
$t\nvDash (p \land \NE) \dis (\bnot p \land \NE) $ and $t\nvDash \bot$; a contradiction.

The property $\PPP\in \mathbb{U}$ in the above proof is clearly expressible in the expressively complete logic as $\PPP=||\OC((p \land \NE)\lor (\lnot p \land \NE))||$.

We conclude this section by noting some consequences of the expressive power results. First, it is shown in <cit.> that any state-based modal logic with the locality property and which is also forgetting enjoys uniform interpolation. Each of our logics has the locality property, and it follows from our expressive completeness results that $\BSMLI$ and $\BSMLO$ are forgetting. Therefore $\BSMLI$ and $\BSMLO$ enjoy uniform interpolation. (See <cit.> for details; for the locality requirement see <cit.>.)

Second, the finite model property for our logics follows from that
for $\ML$, by a simple argument that makes use of disjoint unions of models. The disjoint union $\biguplus_{i\in I}M_i$ of the models $\{M_i\sepp i\in I\neq \emptyset\}$ is defined as usual. Recall in particular that the domain of the disjoint union is defined as $\bigcup_{i\in I}(W_i\times \{i\})$. We also extend the notion to state properties in a natural way: the disjoint union of a non-empty property $\PPP=\{(M_i,s_i)\sepp i\in I\}$ is $\biguplus \PPP:=(\biguplus_{i\in I} M_i, \biguplus_{i\in I} s_i)$, where $\biguplus_{i\in I} s_i:=\bigcup_{i\in I}(s_i \times\{i\})$. To simplify notation, we define the disjoint union $\biguplus \emptyset$ of the empty property to be $(M,\emptyset)$ for some fixed $M$. We refer to an element $(w,i)$ in the disjoint union as simply $w$, and similarly for states. The following is standard (see, for example, <cit.>):

For all $i\in I,w\in W_i,k\in \mathbb{N}: M_i,w \bisim_k \biguplus_{i\in I} M_i, w $. Consequently, for all $s\subseteq W_i,k\in \mathbb{N}: M_i,s\bisim_k \biguplus_{i\in I} M_i, s $.

If $\nvDash\phi$, then there is some finite model $M$ and state $s$ such that $M,s\nvDash \phi$.

Let $(M,s)$ be such that $M,s\nvDash \phi$ and let $k=md(\phi)$. If $s=\emptyset$, we clearly have $M',s\nvDash \phi$ for all finite $M'$. Now assume $s\neq \emptyset$. Since there are only finitely many $k$-th bisimilarity types (or Hintikka formulas), we can take a finite $t\subseteq s$ such that $t \bisim_k s$. Clearly for any $w\in t$ we have $\chi^k_w\notequiv \bot$; therefore, by the finite model property for $\ML$, there is some finite $(M_w,v_w)$ such that $M_w,v_w\vDash \chi^k_w$. Then by Theorem <ref>, $M_w,v_w \bisim_k M,w$. By Proposition <ref>, $\biguplus_{w\in t}M_w,v_w\bisim_k M_w,v_w$ for all $w\in t$; then also $\biguplus_{w\in t}M_w,v_w\bisim_k M,w$ for all $w\in t$, so $\biguplus_{w\in t}M_w,\{v_w\sepp w\in t\}\bisim_k M,t$, whence $\biguplus_{w\in t}M_w,\{v_w\sepp w\in t\}\nvDash \phi$ by Theorem <ref>, where $\biguplus_{w\in t}M_w$ is clearly finite.

Together with the completeness results to be proved in Section <ref>, this implies that our logics $\BSML$, $\BSMLO$, and $\BSMLI$ are decidable.

§ AXIOMATIZATIONS

In this section we introduce sound and complete natural deduction systems for $\BSML$ and its extensions. The strategy we employ in proving completeness makes essential use of the expressive power results in Section <ref>: for the expressively complete logics $\BSMLI$ and $\BSMLO$, we show that each formula is provably equivalent to some formula in disjunctive normal form—completeness then reduces to showing it for formulas in normal form. As for $\BSML$, for which no similar normal form is available, our strategy involves simulating the $\BSMLI$-normal form by using sets of $\BSML$-formulas. For this reason we first axiomatize the extensions.

§ CONCLUSION

In this paper, we presented natural deduction axiomatizations for $\BSML$ and the two extensions we introduced, $\BSMLI$ ($\BSML$ with the global/inquisitive disjunction $\intd$) and $\BSMLO$ ($\BSML$ with the novel emptiness operator $\OC$). We also proved the expressive completeness of the two extensions: $\BSMLI$ is expressively complete for the class of all state properties invariant under bounded bisimulation; $\BSMLO$ for the class of all union-closed state properties invariant under bounded bisimulation.
We conclude by listing some possible directions for further investigation.

We saw that is union closed but not expressively complete for union-closed properties. It is an open question whether is expressively complete for some natural class of state properties.

The semantics of the quantifiers in first-order dependence logic are analogous to the semantics of the modalities used in modal dependence logic, which are distinct from the -modalities $\Di$ and $\Bo$. Defining first-order quantifiers whose semantics are analogous to those of $\Di$ and $\Bo$ may result in first-order state-based logics with interesting properties.

In inquisitive semantics, the global disjunction $\intd$ is used to model the meanings of questions. Similarly, in the context of the extension $\BSMLI$, this disjunction might allow one to model questions and their interaction with free choice phenomena <ref>, and to arrive at a full account of examples of overt free choice cancellation <ref>,  which were left open in <cit.>.

.  Can I have coffee or tea?   $\Diamond (c \vee t) \intd \neg \Diamond (c \vee t)$
. Yes $\implicates$ you can have coffee and you can have tea
.̱ No $\implicates$ you cannot have either

.  You may have coffee or tea, I don't know which.

Finally, given that the emptiness operator $\OC$ is a natural counterpart to $\NE$ and that it can be used to cancel out the effects of pragmatic enrichment in the sense that $\OC(\alpha \land \NE)\equiv \alpha$, investigating the applications of this operator in formal semantics may yield some interesting results.


# Elementary Continued Fractions for Linear Combinations of Zeta and $L$
Values

Henri Cohen,
<EMAIL_ADDRESS>
###### Abstract

We show how to obtain infinitely many continued fractions for certain
${\mathbb{Z}}$-linear combinations of zeta and $L$-values. The methods are
completely elementary.

##  1 Introduction and Main Goal

In [4], the authors give five continued fractions for certain
${\mathbb{Z}}$-linear combinations of zeta values, only obtained and checked
numerically, as well as other linear combinations involving powers of $\pi$,
Catalan’s constant, etc… The purpose of the present paper is to show that
these continued fractions are completely elementary. In fact, we explain three
general methods for constructing them. In particular we give seven infinite
families of such continued fractions. We also discuss analogous results
involving $L$-values for Dirichlet characters of conductor $3$ and $4$.

We use the following notation for a continued fraction $S$, which may differ
from notation used in other papers in the literature:

$S=a(0)+b(0)/(a(1)+b(1)/(a(2)+b(2)/(a(3)+\cdots)))\;,$

and we denote as usual by $p(n)/q(n)$ the $n$th convergent, so that
$p(0)/q(0)=a(0)/1$, $p(1)/q(1)=(a(0)a(1)+b(0))/a(1)$, etc…

When $a(n)$ and $b(n)$ are polynomials $A(n)$ and $B(n)$ for $n\geq 1$, we
will write the continued fraction as $S=[[a(0),A(n)],[b(0),B(n)]]$. For
instance, the continued fraction

$\zeta(2)=2/(1+1/(3+16/(5+81/(7+256/(9+\cdots)))))$

will simply be written as $\zeta(2)=[[0,2n-1],[2,n^{4}]]$.

We recall the following trivial result due to Euler:

###### Lemma 1.1

Let $f(n)$ be a nonzero arithmetic function, and set by convention $f(0)=0$.
When the left-hand side converges, we have

$\sum_{n\geq 1}\dfrac{z^{n}}{f(n)}=[[0,f(n)+zf(n-1)],[z,-zf(n)^{2}]]\;,$

and in addition the $N$th partial sum of the series is equal to the $N$th
convergent $p(N)/q(N)$ of the continued fraction.

As a trivial application, for $k\geq 2$, we have the trivial continued
fraction

$\zeta(k)=[[0,n^{k}+(n-1)^{k}],[1,-n^{2k}]]\;.$

The second trivial lemma that we will use is the following:

###### Lemma 1.2

Let $(a(n),b(n))$ define a continued fraction with convergents $(p(n),q(n))$,
and let $r(n)$ be an arbitrary nonzero arithmetic function with $r(0)=1$. Then
if we set $a^{\prime}(n)=r(n)a(n)$ and $b^{\prime}(n)=r(n)r(n+1)b(n)$, the
corresponding convergents $(p^{\prime}(n),q^{\prime}(n))$ are given by
$(p^{\prime}(n),q^{\prime}(n))=r!(n)(p(n),q(n))$ with evident notation, and in
particular $p^{\prime}(n)/q^{\prime}(n)=p(n)/q(n)$.

Thanks to the first lemma above, we can thus transform any series into a
continued fraction, not really interesting. For instance, assume that I want a
CF for $\zeta(2)+\zeta(3)$: we have $\zeta(2)+\zeta(3)=\sum_{n\geq
1}(n+1)/n^{3}$, so applying the first lemma to $f(n)=n^{3}/(n+1)$ and $z=1$,
we get

$\zeta(2)+\zeta(3)=[[0,n^{3}/(n+1)+(n-1)^{3}/n],[1,-n^{6}/(n+1)^{2}]]\;,$

and applying the second lemma to $r(0)=1$, $r(n)=n^{2}+n$ for $n\geq 1$, we
get

$\zeta(2)+\zeta(3)=[[0,2n^{4}-2n^{3}+2n-1],[2,-(n^{8}+2n^{7})]]\;.$

As mentioned, not very interesting, in particular because continued fractions
involving $\zeta(3)$ should have $a(n)$ a polynomial of degree at most $3$,
and $b(n)$ at most $6$.

We can now more precisely state our goal, much wider than the simple proofs of
the continued fractions given in [4]. First, we set the following definition:

###### Definition 1.3

Let $d\geq 0$ be an integer. A _rational period_ of degree $k$ is the sum of a
convergent series of the form $\sum_{n\geq 1}\chi(n)f(n)$, where $\chi(n)$ is
a periodic arithmetic function taking rational values, and
$f\in{\mathbb{Q}}(x)$ is a rational function with rational coefficients, whose
denominator is of degree $k$.

Two remarks concerning this definition: first, it is _not_ compatible with the
definition of periods as given in [3]. Second, one could ask the coefficients
to be algebraic instead of rational, but this leads to a theory which is too
general.

Examples: $\log(2)$, $\pi$, and $L(\chi,1)$ for a nontrivial Dirichlet
character all have degree $1$, more generally $\pi^{k}$ and $L(\chi,k)$ are
rational periods of degree $k$. Note also that a ${\mathbb{Q}}$-linear
combination of rational periods of degree $\leq k$ is again a rational period
of degree $\leq k$.

Thus, our goal will be as follows: find continued fractions $(a(n),b(n))$ for
rational periods degree $k$ where for $n$ sufficiently large $a(n)$ is a
polynomial of degree at most $k$ and $b(n)$ of degree at most $2k$, which we
abbreviate by saying that it has _bidegree_ at most $(k,2k)$.

The prototypical “trivial” example is $S=\sum_{n\geq 1}1/P(n)$ with $P$ a
polynomial of degree $k\geq 2$, and $S=[[0,P(n)+P(n-1)],[1,-P(n)^{2}]]$ is a
continued fraction of required bidegree $(k,2k)$, by Euler’s lemma above, and
similarly for $S=\sum_{n\geq 1}(-1)^{n-1}/P(n)$. On the contrary, as mentioned
above, such a continued fraction does not seem to exist for $\sum_{n\geq
1}(n+1)/n^{3}$.

##  2 First Method: use of Polynomial Multipliers

###### Proposition 2.1

Fix an integer $k\geq 2$, and let $P\in{\mathbb{Q}}[x]$ be a nonzero
polynomial with rational coefficients such that $P(x)$ divides
$x^{k}P(x+1)+(x-1)^{k}P(x-1)$, and set
$R(x)=(x^{k}P(x+1)+(x-1)^{k}P(x-1))/P(x)$.

  1. (1)

We have the continued fraction expansion

$S=\sum_{n\geq
1}\dfrac{1}{n^{k}P(n)P(n+1)}=[[0,R(x)],[1/P(0)^{2},-n^{2k}]]\;,$

which is a continued fraction of bidegree $(k,2k)$.

  2. (2)

If $P(x)$ and $P(x+1)$ are coprime polynomials and $d=\deg(P)\leq k$, $S$ is a
rational period of degree at most $k$.

Proof. (1). By Euler’s lemma above we have

$S=[[0,n^{k}P(n)P(n+1)+(n-1)^{k}P(n-1)P(n)],[1,-n^{2k}P(n)^{2}P(n+1)^{2}]]\;.$

I claim that $P(1)\neq 0$: indeed, if $P(1)=0$ we deduce that
$1^{k}P(2)=R(1)P(1)$ so $P(2)=0$, and the recursion
$(n-1)^{k}P(n)=R(n-1)P(n-1)-(n-2)^{k}P(n-2)$ for $n\geq 3$ implies that
$P(n)=0$ for all $n$, so $P$ has infinitely many roots so is identically zero,
contradiction. We can thus apply the second lemma to $r(n)=1/P(n)^{2}$ for
$n\geq 1$ and $r(0)=1$ and we obtain immediately
$S=[[0,R(n)],[1/P(1)^{2},-n^{2k}]]$, proving (1).

For (2), we first note that using the same proof as in (1) but using the
recursion backwards, we have $P(0)\neq 0$. We can thus write a partial
fraction decomposition in the form

$\dfrac{1}{x^{k}P(x)P(x+1)}=\sum_{1\leq j\leq
k}\dfrac{c_{j}}{x^{j}}+\dfrac{N(x)}{P(x)P(x+1)}\;,$

where the $c_{j}$ are constants and $\deg(N(x))\leq 2d-1$, where $d=\deg(P)$.
Since by assumption $P(x)$ and $P(x+1)$ are coprime, by the extended Euclidean
algorithm, there exist polynomials $U$ and $V$ such that
$U(x)P(x)+V(x)P(x+1)=N(x)$, and $U$ and $V$ can be chose of degree less than
or equal to $d-1$. Thus $N(x)/(P(x)P(x+1))=U(x)/P(x+1)+V(x)/P(x)$, so $S$ is a
rational period of degree at most $d\leq k$.  $\sqcap$$\sqcup$

Remarks

  1. (1)

It is possible that the condition that $P(x)$ and $P(x+1)$ are coprime can be
lifted.

  2. (2)

One can prove that $P(x)$ satisfies the identity $P(x+1)=(-1)^{d}P(-x)$, or
equivalently $P(1-x)=(-1)^{d}P(x)$. I am grateful to “Ilya Bogdanov” from the
MathOverflow forum for the proof of this fact.

Exactly the same proposition with an identical proof can be applied to
alternating sums:

###### Proposition 2.2

Fix an integer $k\geq 2$, and let $P\in{\mathbb{Q}}[x]$ be a nonzero
polynomial with rational coefficients such that $P(x)$ divides
$x^{k}P(x+1)-(x-1)^{k}P(x-1)$, and set
$R(x)=(x^{k}P(x+1)-(x-1)^{k}P(x-1))/P(x)$.

  1. (1)

We have the continued fraction expansion

$S=\sum_{n\geq
1}\dfrac{(-1)^{n-1}}{n^{k}P(n)P(n+1)}=[[0,R(x)],[1/P(0)^{2},n^{2k}]]\;,$

which is a continued fraction of bidegree $(k-1,2k)$.

  2. (2)

If $P(x)$ and $P(x+1)$ are coprime polynomials and $d=\deg(P)\leq k$, $S$ is a
rational period of degree at most $k$.

The next section consists in searching for suitable polynomials $P(x)$ and
writing the corresponding rational period and continued fraction.

##  3 Examples

###### Proposition 3.1

The condition of the proposition $P\in{\mathbb{Q}}[x]$ dividing
$x^{k}P(x+1)+(x-1)^{k}P(x-1)$ is satisfied in the following cases:

  1. (1)

$k\equiv 0\allowbreak\ ({\rm{mod}}\,\,2)$ and $P(x)=2x-1$.

  2. (2)

$k\equiv-1\allowbreak\ ({\rm{mod}}\,\,3)$ and $P(x)=3x^{2}-3x+1$.

  3. (3)

$k\equiv-1\allowbreak\ ({\rm{mod}}\,\,4)$ and $P(x)=2x^{2}-2x+1$.

  4. (4)

$k\equiv-1\allowbreak\ ({\rm{mod}}\,\,6)$ and $P(x)=x^{2}-x+1$.

  5. (5)

$k=5$ and $P(x)=5x^{4}-10x^{3}+19x^{2}-14x+4$.

Proof. In the first four cases, it is sufficient to check that any root of
$P(x)=0$ is also a root of $x^{k}P(x+1)+(x-1)^{k}P(x-1)$. For instance in the
first case $P(x)=2x-1$, for $a=1/2$ we have $P(a+1)=2$ and $P(a-1)=-2$, and
indeed $2^{-k}\cdot 2+(-2)^{-k}\cdot(-2)=0$ when $k$ is even. The last case is
done by a direct divisibility test.  $\sqcap$$\sqcup$

The same proof shows the following:

###### Proposition 3.2

The condition of the proposition $P\in{\mathbb{Q}}[x]$ dividing
$x^{k}P(x+1)-(x-1)^{k}P(x-1)$ is satisfied in the following cases:

  1. (1)

$k\equiv 1\allowbreak\ ({\rm{mod}}\,\,2)$ and $P(x)=2x-1$.

  2. (2)

$k\equiv 1\allowbreak\ ({\rm{mod}}\,\,4)$ and $P(x)=2x^{2}-2x+1$.

  3. (3)

$k\equiv 2\allowbreak\ ({\rm{mod}}\,\,6)$ and $P(x)=x^{2}-x+1$.

Note that I have not found any other examples than the ones given in the above
two propositions, but I may have missed some.

Thanks to these propositions, it is now just a matter of working out
explicitly all the above examples, in other words of computing the partial
fraction expansions of the expressions $1/(x^{k}P(x)P(x+1))$, which is routine
so not given explicitly. In particular, we will see that in the non-
alternating cases, the sum $S$ is a ${\mathbb{Q}}$-linear combination of $1$
and $\zeta(k)$ for $k\geq 2$ of fixed parity, and in the alternating cases,
with in addition $\log(2)$.

We now give the corresponding formulas, and give examples after. The following
corollary immediately follows from the above propositions:

###### Corollary 3.3

By convention, set $\zeta(0)=\zeta^{*}(0)=0$, $\zeta^{*}(1)=\log(2)$, and
$\zeta^{*}(k)=(2^{k-1}-1)\zeta(k)$ for $k\geq 2$. We have the following
general continued fractions:

$\displaystyle\sum_{j=0}^{k-1}2^{2j}\zeta(2(k-j))=[[2^{2k-1},R_{1}(n)],[-1,-n^{4k}]]\;,\text{
with}$ $\displaystyle R_{1}(x)=(x^{2k}(2x+1)+(x-1)^{2k}(2x-3))/(2x-1)\;,$
$\displaystyle\sum_{j=0}^{k}(-3)^{3j}(\zeta(6(k-j)+2)+3\zeta(6(k-j)))=[[-(-3)^{3k+1}/2,R_{2}(n)],[1,-n^{12k+4}]]\;,\text{
with}$ $\displaystyle
R_{2}(x)=(x^{6k+2}(3x^{2}+3x+1)+(x-1)^{6k+2}(3x^{2}-9x+7))/(3x^{2}-3x+1)\;,$
$\displaystyle\sum_{j=0}^{k}(-3)^{3j}(\zeta(6(k-j)+5)+3\zeta(6(k-j)+3))=[[(-3)^{3k+2}/2,R_{3}(n)],[1,-n^{12k+10}]]\;,\text{
with}$ $\displaystyle
R_{3}(x)=(x^{6k+5}(3x^{2}+3x+1)+(x-1)^{6k+5}(3x^{2}-9x+7))/(3x^{2}-3x+1)\;,$
$\displaystyle\sum_{j=0}^{k}(-4)^{j}\zeta(4(k-j)+3)=[[4^{k},R_{4}(n)],[1,-n^{8k+6}]]\;,\text{
with}$ $\displaystyle
R_{4}(x)=(x^{4k+3}(2x^{2}+2x+1)+(x-1)^{4k+3}(2x^{2}-6x+5))/(2x^{2}-2x+1)\;,$
$\displaystyle\sum_{j=0}^{k}(\zeta(6(k-j)+5)-\zeta(6(k-j)+3))=[[-1/2,R_{5}(n)],[1,-n^{12k+10}]]\;,\text{
with}$ $\displaystyle
R_{5}(x)=(x^{6k+5}(x^{2}+x+1)+(x-1)^{6k+5}(x^{3}-3x+3))/(x^{2}-x+1)\;,$
$\displaystyle\sum_{j=0}^{k}2^{4j}\zeta^{*}(2(k-j)+1)=[[2^{4k},R_{6}(n)],[-2^{2k},n^{4k+2}]]\;,\text{
with}$ $\displaystyle R_{6}(x)=(x^{2k+1}(2x+1)-(x-1)^{2k+1}(2x-3))/(2x-1)\;,$
$\displaystyle\sum_{j=0}^{k}(-64)^{j}\zeta^{*}(4(k-j)+1)=[[(-1)^{k}2^{6k-1},R_{7}(n)],[2^{4k},n^{8k+2}]]\;,\text{
with}$ $\displaystyle
R_{7}(x)=(x^{4k+1}(2x^{2}+2x+1)-(x-1)^{4k+1}(2x^{2}-6x+5))/(2x^{2}-2x+1)\;,$
$\displaystyle\sum_{j=0}^{k}2^{6j}(\zeta^{*}(6(k-j)+2)-4\zeta^{*}(6(k-j)))=[[2^{6k},R_{8}(n)],[2^{6k+1},n^{12k+4}]]\;,\text{
with}$ $\displaystyle
R_{8}(x)=(x^{6k+2}(x^{2}+x+1)-(x-1)^{6k+2}(x^{2}-3x+3))/(x^{2}-x+1)\;.$

We now give corresponding examples:

$\displaystyle\zeta(4)+4\zeta(2)=[[8,2n^{4}-4n^{3}+10n^{2}-8n+3],[-1,-n^{8}]]\;,$
$\displaystyle
27\zeta(2)-3\zeta(6)-\zeta(8)=[[81/2,R(n)],[-1,-n^{16}]]\;,\text{ with}$
$\displaystyle
R(n)=2n^{8}-8n^{7}+46n^{6}-110n^{5}+178n^{4}-182n^{3}+118n^{2}-44n+7\;,$
$\displaystyle\zeta(5)+3\zeta(3)=[[9/2,2n^{5}-5n^{4}+22n^{3}-28n^{2}+23n-7],[1,-n^{10}]]\;,$
$\displaystyle
4\zeta(3)-\zeta(7)=[[4,2n^{7}-7n^{6}+37n^{5}-75n^{4}+99n^{3}-77n^{2}+31n-5],[-1,-n^{14}]]\;,$
$\displaystyle\zeta(3)-\zeta(5)=[[1/2,2n^{5}-5n^{4}+22n^{3}-28n^{2}+15n-3],[-1,-n^{10}]]\;,$
$\displaystyle
4\zeta(5)+11\zeta(3)=[[273/16,2n^{5}-5n^{4}+42n^{3}-58n^{2}+45n-13],[4,-n^{10}]]\;,$
$\displaystyle 3\zeta(3)+16\log(2)=[[16,5n^{2}-5n+3],[-4,n^{6}]]\;,$
$\displaystyle
15\zeta(5)+48\zeta(3)+256\log(2)=[[256,7n^{4}-14n^{3}+18n^{2}-11n+3],[-16,n^{10}]]\;,$
$\displaystyle
64\log(2)-15\zeta(5)=[[32,9n^{4}-18n^{3}+30n^{2}-21n+5],[-16,n^{10}]]\;,$
$\displaystyle
127\zeta(8)-124\zeta(6)+64\zeta(2)=[[64,R(n)],[128,n^{16}]]\;,\text{ with}$
$\displaystyle
R(n)=12n^{7}-42n^{6}+110n^{5}-170n^{4}+154n^{3}-82n^{2}+24n-3\;.$

##  4 Second Method: use of the $\psi$ Function and Derivatives

Recall that $\psi(z)$ is the logarithmic derivative of the gamma function
(most authors call $\psi$ the digamma function, and $\psi^{\prime}$,
$\psi^{\prime\prime}$, etc… the trigamma, tetragamma functions, but this is
terrible terminology).

By orthogonality of characters, it is immediate to show that for $k\geq 1$

$\psi^{(k)}(r/m)=(-1)^{k-1}\dfrac{k!m^{k+1}}{\phi(m)}\sum_{\chi\bmod
m}\overline{\chi}(r)L(\chi,k+1)\;,$

and for $k=0$ the same formula is valid if we interpret $L(\chi_{0},1)$ as

$L(\chi_{0},1)=\sum_{d\mid
m}\dfrac{\mu(d)}{d}\log(d)-\dfrac{\phi(m)\log(m)}{m}\;.$

In particular, for $m=1$, $2$, $3$, $4$, and $6$, which are the values of $m$
for which $\phi(m)\leq 2$, we obtain the following table, where as usual we
set $G=L(\chi_{-4},2)$, Catalan’s constant, and $G_{3}=L(\chi_{-3},2)$:

$r/m$ $\psi(r/m)+\gamma$ $\psi^{\prime}(r/m)$ $\psi^{\prime\prime}(r/m)$ 1 $0$
$\zeta(2)$ $-2\zeta(3)$ 1/2 $-2\log(2)$ $3\zeta(2)$ $-14\zeta(3)$ 1/3
$-3\log(3)/2-\pi/(2\sqrt{3})$ $4\zeta(2)+9G_{3}/2$
$-26\zeta(3)-4\pi^{3}/(3\sqrt{3})$ 2/3 $-3\log(3)/2+\pi/(2\sqrt{3})$
$4\zeta(2)-9G_{3}/2$ $-26\zeta(3)+4\pi^{3}/(3\sqrt{3})$ 1/4 $-3\log(2)-\pi/2$
$6\zeta(2)+8G$ $-56\zeta(3)-2\pi^{3}$ 3/4 $-3\log(2)+\pi/2$ $6\zeta(2)-8G$
$-56\zeta(3)+2\pi^{3}$ 1/6 $-\log(432)/2-3\pi/(2\sqrt{3})$
$12\zeta(2)+45G_{3}/2$ $-182\zeta(3)-12\pi^{3}/\sqrt{3}$ 5/6
$-\log(432)/2+3\pi/(2\sqrt{3})$ $12\zeta(2)-45G_{3}/2$
$-182\zeta(3)+12\pi^{3}/\sqrt{3}$

On the other hand, there exist many continued fractions for $\psi(z)$ and its
derivatives. The ones for $\psi(z)$ itself are rather complicated, and those
for $\psi^{(k)}(z)$ for $k\geq 3$ are trivial transformations of the defining
series, so the only remaining interesting ones are those for
$\psi^{\prime}(z)$ and $\psi^{\prime\prime}(z)$. This of course implies that
we restrict to rational periods of degree two and three.

We choose the nicest continued fractions, taken from [2]:

For $\psi^{\prime}(z)$ we have

$\psi^{\prime}(z)=[[0,(2z-1)(2n-1)],[2,n^{4}]]\;,$

valid for $z>1/2$. However, from the trivial identity
$\psi^{\prime}(z)=\psi^{\prime}(z+1)+1/z^{2}$, we can deduce infinitely many
other continued fractions:

$\psi^{\prime}(z)=[[\sum_{0\leq
j<k}1/(z+j)^{2},(2z+2k-1)(2n-1)],[2,n^{4}]]\;,$

now valid for $z>1/2-k$. Referring to the above table and choosing $z=1/3$,
$2/3$, $1/4$, $3/4$, $1/6$, and $5/6$, and $k=0$, $1$, etc…, we obtain as many
continued fractions as we like for $8\zeta(2)\pm 9G_{3}$, $3\zeta(2)\pm 4G$,
and $8\zeta(2)\pm 15G_{3}$. For instance, after simplifications:

$\displaystyle 8\zeta(2)-9G_{3}$ $\displaystyle=[[0,2n-1],[12,9n^{4}]]\;,$
$\displaystyle 8\zeta(2)+9G_{3}$ $\displaystyle=[[18,10n-5],[12,9n^{4}]]\;,$
$\displaystyle 3\zeta(2)-4G$ $\displaystyle=[[0,2n-1],[2,4n^{4}]]\;,$
$\displaystyle 3\zeta(2)+4G$ $\displaystyle=[[8,6n-3],[2,4n^{4}]]\;,$
$\displaystyle 8\zeta(2)-15G_{3}$ $\displaystyle=[[0,4n-2],[4,9n^{4}]]\;,$
$\displaystyle 8\zeta(2)+15G_{3}$ $\displaystyle=[[24,8n-4],[4,9n^{4}]]\;.$

For $\psi^{\prime\prime}(z)$ we have

$\psi^{\prime\prime}(z)=[[0,(2n-1)(n^{2}-n+1+2z(z-1))],[-2,-n^{6}]]\;,$

valid for $z>1/2$. However, from the trivial identity
$\psi^{\prime\prime}(z)=\psi^{\prime\prime}(z+1)-2/z^{3}$, we can deduce
infinitely many other continued fractions:

$\psi^{\prime\prime}(z)=[[-2\sum_{0\leq
j<k}1/(z+j)^{3},(2n-1)(n^{2}-n+1+2(z+k)(z+k-1))],[-2,-n^{6}]]\;,$

now valid for $z>1/2-k$. Referring to the above table and choosing $z=1/3$,
$2/3$, $1/4$, $3/4$, $1/6$, and $5/6$, and $k=0$, $1$, etc…, we obtain as many
continued fractions as we like for $39\zeta(3)\pm 2\pi^{3}/\sqrt{3}$,
$28\zeta(3)\pm\pi^{3}$, and $91\zeta(3)\pm 6\pi^{3}/\sqrt{3}$. For instance,
after simplifications:

$\displaystyle 39\zeta(3)-2\pi^{3}/\sqrt{3}$
$\displaystyle=[[0,(2n-1)(9n^{2}-9n+5)],[27,-81n^{6}]]\;,$ $\displaystyle
39\zeta(3)+2\pi^{3}/\sqrt{3}$
$\displaystyle=[[81,(2n-1)(9n^{2}-9n+17)],[27,-81n^{6}]]\;,$ $\displaystyle
28\zeta(3)-\pi^{3}$ $\displaystyle=[[0,(2n-1)(8n^{2}-8n+5)],[8,-64n^{6}]]\;,$
$\displaystyle 28\zeta(3)+\pi^{3}$
$\displaystyle=[[64,(2n-1)(8n^{2}-8n+13)],[8,-64n^{6}]]\;,$ $\displaystyle
91\zeta(3)-6\pi^{3}/\sqrt{3}$
$\displaystyle=[[0,(2n-1)(9n^{2}-9n+13/2)],[9,-81n^{6}]]\;,$ $\displaystyle
91\zeta(3)+6\pi^{3}/\sqrt{3}$
$\displaystyle=[[216,(2n-1)(9n^{2}-9n+25/2)],[9,-81n^{6}]]\;.$

##  5 Third Method: Bauer–Muir Acceleration

This very classical method is just as elementary as the previous ones, but the
formulas are slightly more complicated.

Let $(a(n),b(n))_{n\geq 0}$ be a continued fraction with convergents
$(p(n),q(n))$, and let $r(n)_{n\geq 1}$ be any sequence (for now). For $n\geq
1$ we define

$R(n)=a(n)+r(n)\text{ and }d(n)=r(n)R(n+1)-b(n)=r(n)(a(n+1)+b(n+1))-b(n)\;.$

We make the following two essential assumptions: $R(1)=a(1)+r(1)\neq 0$, and
$d(n)\neq 0$ for all $n\geq 1$.

We define:

$\displaystyle A(0)$ $\displaystyle=a(0)+\dfrac{b(0)}{R(1)}\;,\quad
B(0)=\dfrac{b(0)d(1)}{R(1)^{2}}\;,\quad A(1)=\dfrac{a(1)R(2)+b(1)}{R(1)}\;,$
$\displaystyle A(n)$ $\displaystyle=R(n+1)-r(n-1)\dfrac{d(n)}{d(n-1)}\text{
for $n\geq 2$, and }B(n)=b(n)\dfrac{d(n+1)}{d(n)}\text{ for $n\geq 1$.}$

The following result is easy to prove by induction:

###### Proposition 5.1

Let $(P(n),Q(n))$ be the convergents of the continued fraction defined by
$(A(n),B(n))$. For $n\geq 2$ we have

$(P(n),Q(n))=(p(n+1),q(n+1))+r(n+1)(p(n),q(n))\;.$

In particular, if $p(n)/q(n)$ and $P(n)/Q(n)$ both tend to a limit as
$n\to\infty$, these limits are equal.

This process is called Bauer–Muir acceleration, because if $r(n)$ is chosen
appropriately, it accelerates the convergence of the continued fraction. An
important fact is that if the accelerated formulas are simple enough, for
instance when $d(n)$ is _constant_ , the acceleration process can be
_iterated_. This fact, combined with a suitable diagonal process, is the basis
of Apéry’s initial proofs of the irrationality of $\zeta(2)$ and $\zeta(3)$.
However, we will not consider this here.

Let us consider some simple examples.

Example 1: $\log(2)$

The trivial continued fraction for $\log(2)$, directly coming from the series
$\log(2)=\sum_{n\geq 1}(-1)^{n-1}/n$, is $\log(2)=[[0,1],[1,n^{2}]]$. Applying
Bauer–Muir acceleration iteratively, we immediately obtain

$\log(2)=[[0,1],[1,n^{2}]]=[[1,3],[-1,n^{2}]]=[[1/2,5],[1,n^{2}]]=[[5/6,7],[-1,n^{2}]]\;,$

and so on, the general formula being

$\log(2)=[[\sum_{1\leq j\leq k}(-1)^{j-1}/j,2k+1],[(-1)^{k},n^{2}]]\;.$

Note that this is _not_ the same as the trivial continued fraction obtained
from $\sum_{n>k}(-1)^{n-1}/n$, since this converges like $(-1)^{n}/n$ as the
initial one, while the accelerated formula given above converges like
$(-1)^{n}/n^{2k+1}$.

Example 2: $\pi^{2}/6$

The trivial continued fraction for $\zeta(2)=\pi^{2}/6$, directly coming from
the series $\pi^{2}/6=\sum_{n\geq 1}1/n^{2}$, is
$\pi^{2}/6=[[0,2n^{2}-2n+1],[1,-n^{4}]]$. Applying Bauer–Muir acceleration
iteratively, we immediately obtain

$\displaystyle\pi^{2}/6$
$\displaystyle=[[0,2n^{2}-2n+1],[1,-n^{4}]]=[[2,2n^{2}-2n+3],[-1,-n^{4}]]$
$\displaystyle=[[3/2,2n^{2}-2n+7],[1,-n^{4}]]=[[31/18,2n^{2}-2n+13],[-1,-n^{4}]]$
$\displaystyle=[[115/72,2n^{2}-2n+21],[1,-n^{4}]]=[[3019/1800,2n^{2}-2n+31],[-1,-n^{4}]]$
$\displaystyle=[[973/600,2n^{2}-2n+43],[1,-n^{4}]]\;,$

and so on, the general formula being

$\pi^{2}/6=[[2\sum_{1\leq j\leq
k}(-1)^{j-1}/j^{2},2n^{2}-2n+k^{2}+k+1],[(-1)^{k},-n^{4}]]\;.$

Once again, this is not the tail of the series defining $\pi^{2}/6$, since it
converges like $1/n^{2k+1}$.

Example 3: $\pi^{2}/6$ (again)

Another trivial continued fraction for $\pi^{2}/6$, directly coming from the
series $\pi^{2}/6=2\sum_{n\geq 1}(-1)^{n-1}/n^{2}$, is
$\pi^{2}/6=[[0,2n-1],[2,n^{4}]]$. Applying Bauer–Muir acceleration
iteratively, we immediately obtain

$\displaystyle\pi^{2}/6$
$\displaystyle=[[0,2n-1],[2,n^{4}]]=[[1,6n-3],[2,n^{4}]]=[[5/4,10n-5],[2,n^{4}]]$
$\displaystyle=[[49/36,14n-7],[2,n^{4}]]=[[205/144,18n-9],[2,n^{4}]]$
$\displaystyle=[[5269/3600,22n-11],[2,n^{4}]]\;,$

and so on, the general formula being

$\pi^{2}/6=[[\sum_{1\leq j\leq k}1/j^{2},(2k+1)(2n-1)],[2,n^{4}]]\;.$

Note that the constant term of the continued fraction for $\sum_{j\geq
1}1/j^{2}$ is the partial sum of the series $\sum_{j\geq 1}(-1)^{j-1}/j^{2}$
and the constant term of the continued fraction for $\sum_{j\geq
1}(-1)^{j-1}/j^{2}$ is the partial sum of the series $\sum_{j\geq 1}1/j^{2}$.

Example 4: $G=L(\chi_{-4},2)$, Catalan’s constant

Here, we could take the trivial continued fraction for $G$, directly coming
from the series $G=\sum_{n\geq 1}(-1)^{n-1}/(2n-1)^{2}$, and apply iteratively
Bauer–Muir, giving

$\displaystyle G$
$\displaystyle=[[0,1,8(n-1)],[1,(2n-1)^{4}]]=[[1/6,7/3,24(n-1)],[16/9,(2n-1)^{4}]]$
$\displaystyle=[[19/82,145/41,40(n-1)],[4096/1681,(2n-1)^{4}]]\;,$

and so on, but this is not pretty, first because $b(0)$ changes, and second
because one needs to specify both $a(0)$ and $a(1)$ since $n-1$ vanishes for
$n=1$.

A nicer continued fraction taken from [2], which in fact we are going to
prove, is $G=[[1,8n^{2}-8n+7],[-1/2,-16n^{4}]]$. We thus obtain

$\displaystyle G$ $\displaystyle=[[0,8n^{2}-8n+3],[1/2,-16n^{4}]]$
$\displaystyle=[[1,8n^{2}-8n+7],[-1/2,-16n^{4}]]=[[8/9,8n^{2}-8n+19],[1/2,-16n^{4}]]$
$\displaystyle=[[209/225,8n^{2}-8n+39],[-1/2,-16n^{4}]]$
$\displaystyle=[[10016/11025,8n^{2}-8n+67],[1/2,-16n^{4}]]\;,$

and so on, the general formula being

$G=[[\sum_{1\leq j\leq
k}(-1)^{j-1}/(2j-1)^{2},8n^{2}-8n+4k^{2}+3],[(-1)^{k}/2,-16n^{4}]]\;,$

and the continued fraction for $k=0$ being obtained by _reverse_ Bauer–Muir,
with extremely slow convergence in $1/\log(n)$.

But in turn these formulas _prove_ that the initial continued fraction
converges to $G$, since if we set $S_{k}=\sum_{1\leq j\leq
k}(-1)^{j-1}/(2j-1)^{2}$, which is the $k$th partial sum of the series
defining $G$, the $k$th continued fraction is
$S_{k}+(-1)^{k}/2/(4k^{2}+3-16/(4k^{2}+19-\cdots))$, and this clearly tends to
$\lim_{k\to\infty}S_{k}=G$ as $k\to\infty$.

Example 5: $\zeta(3)$

The trivial continued fraction for $\zeta(3)$, directly coming from the series
$\zeta(3)=\sum_{n\geq 1}1/n^{3}$, is
$\zeta(3)=[[0,(2n-1)(n^{2}-n+1)],[1,-n^{6}]]$. Applying Bauer–Muir
acceleration iteratively, we immediately obtain

$\displaystyle\zeta(3)$
$\displaystyle=[[0,(2n-1)(n^{2}-n+1)],[1,-n^{6}]]=[[1,(2n-1)(n^{2}-n+5)],[1,-n^{6}]]$
$\displaystyle=[[9/8,(2n-1)(n^{2}-n+13)],[1,-n^{6}]]$
$\displaystyle=[[251/216,(2n-1)(n^{2}-n+25)],[1,-n^{6}]]\;,$

and so on, the general formula being

$\zeta(3)=[[\sum_{1\leq j\leq
k}1/j^{3},(2n-1)(n^{2}-n+2k^{2}+2k+1)],[1,-n^{6}]]\;.$

The reader can check that unfortunately, the method does not work (i.e., the
formulas become extremely complicated) for the alternating sum giving
$3\zeta(3)/4$, nor for $\zeta(k)$ for $k\geq 4$, explaining in large part why
Apéry’s method has not been extended to $\zeta(k)$ for $k\geq 5$. Note that,
on the contrary, Apéry’s method does work for a large number of other series,
and will be the object of a future paper.

##  6 Conclusion

We have given three rather different methods to obtain infinitely many
continued fractions for certain linear combinations of zeta and $L$ values.
Note, however, that they are all polynomially convergent (i.e., in $C/n^{k}$
for some $k\geq 1$), while really interesting continued fractions are
exponentially or at least sub-exponentially convergent. As already mentioned,
this will be the subject of a future paper [1].

## References

  * [1] [Coh] H. Cohen, Continued fractions of polynomial type, 182p., in preparation.
  * [2] [Cuyt] A. Cuyt, V. Petersen, B. Verdonk, H. Waadeland, and W. Jones, Handbook of Continued Fractions for Special Functions, Springer Netherlands (2008).
  * [3] [Kon-Zag] M. Kontsevitch and D. Zagier, Periods, in Mathematics unlimited 2001 and Beyond, Springer (2000), 771–808.
  * [4] [Ram] The Ramanujan machine, www.ramanujanmachine.org