2019  OriginalPaper  Buchkapitel Open Access
Towards a Structural Proof Theory of Probabilistic \(\mu \)Calculi
1 Introduction
2 Technical Background
2.1 The Riesz Modal Logic and Its Scalarfree Fragment

\((R, 0, +, r)_{r\in \mathbb {R}}\) is an \(\mathbb {R}\)vector space,

\((R, \sqcup , \sqcap )\) is a lattice,

the lattice order (\(x \le y \Leftrightarrow x\sqcap y = x)\) is compatible with addition, i.e.:(a)\(x\le y\) implies \(x + z \le y +z\) (i.e., \((x \sqcap y) + z = ((x\sqcap y) + z) \sqcap (y + z) \)),(b)\(x\ge 0\) implies \(r x \ge 0\) (i.e., \( 0= 0 \sqcap r(x\sqcup 0) \)) for every \(r\in \mathbb {R}_{\ge 0}\),

\(\Diamond (x + y ) = \Diamond (x) + \Diamond (y)\) and \(\Diamond (r x) = r\Diamond (x)\),

if \(x\ge 0\) then \(\Diamond (x)\ge 0\) (i.e., \(0 = 0 \sqcap \Diamond (x\sqcup 0) \)),

\(\Diamond (1) \le 1\) (i.e., \(\Diamond 1 = \Diamond 1 \sqcap 1\)).

\(\mathcal {R} \vdash \phi = \psi \) iff \(\mathcal {R} \vdash \phi  \psi = 0\),

\(\mathcal {R} \vdash \phi = \psi \) iff \(\big ( \mathcal {R} \vdash \phi \le \psi \,\,\text { and} \,\,\mathcal {R} \vdash \psi \le \phi \big )\).

\(\mathcal {R} \vdash r(x\sqcup y) = rx \sqcup ry\), \(\mathcal {R} \vdash r(x\sqcap y) = rx \sqcap ry\).
2.2 The Hypersequent Calculus GA

Soundness: if \(\vDash _{\text {GA}}G\) then \(\mathbbm {T}_{(1)} \vdash \llbracket G \rrbracket \ge 0\).

Completeness: if \(\mathbbm {T}_{(1)} \vdash A \ge 0\) then \(\vDash _{\text {GA}} (\vdash A)\)
3 The Hypersequent System MGA

For \(n\in \mathbb {N}_{\ge 0}\), we denote with nF the multiset of formulas \(F,F, \dots , F\).So for example we write \(2A,1B\vdash 0C,D\) to denote the sequent \(A,A,B \vdash D \).

Given a multiset of formulas \(\varGamma = F_0, \dots , F_k\) and \(n\in \mathbb {N}_{\ge 0}\) we denote with \(n \varGamma \) the multiset of formulas \(n F_0, \dots , n F_k\). If \(\varGamma =\emptyset \) then also \(n\varGamma =\emptyset \).

Given a multiset of formulas \(\varGamma = F_0,\dots , F_n\) we denote with \(\Diamond \varGamma \) the multiset of formulas \(\Diamond F_0,\dots , \Diamond F_n\). Consistently, if \(\varGamma =\emptyset \) then also \(\Diamond \varGamma =\emptyset \).

Soundness: if \(\vDash _{\text {MGA}}G\) then \(\mathbbm {T}\vdash \llbracket G \rrbracket \ge 0\).

Completeness: if \(\mathbbm {T}\vdash A \ge 0\) then \(\vDash _{\text {MGA}} (\vdash A)\).
4 Overview of the Proof of the CutElimination Theorem
4.1 The CANElimination Theorem for the System GA

If A is a variable, we can conclude with the atomic CANelimination theorem.

Otherwise we use the invertibility of the logical rules and we can conclude with the induction hypothesis. For instance, if \(A=B + C\), then by invertibility of the \(+_L\) and \(+_R\) rules we have a \( GA ^*\)derivation of \( \vDash _{\text {GA}^*}G  \varGamma , B , C \vdash \varDelta , B , C\) and, from it, we can obtain a \( GA ^*\)derivation of \(G  \varGamma \vdash \varDelta \) by using twice the induction hypothesis, first on B then on C.
4.2 Issues in Adapting the Proof for the System MGA

The logical leftrules and rightrules for the connectives \(\{0,,+,\sqcup ,\sqcap \}\) are generalised to deal with scalar coefficients (syntactic sugaring introduced in Sect. 3). For instance, the rules \(+_L\) and \(\sqcup _L\) become:×

The axioms IDax and 1ax are replaced by the rules×

All structural rules (C, W, S, M), the \(\Diamond \)rule and the CAN rule remain exactly as in MGA (see Fig. 2).
4.3 The System MGASR and the MElimination Theorem
4.4 CutElimination Theorem for the System MGA

If A is a variable, we can conclude with Theorem 11.

If \(A=1\), we can conclude with Lemma 1.

If \(A=\Diamond B\), we look at d.

If d finished with the \(\Diamond \)rule, then the end hypersequent is necessarily of the form: \( \left[ \varGamma _i , k_iA \vdash , k_iA ,\varDelta _i \right] _{i=1}^n = \Diamond \varGamma _1 , n_1 \Diamond B \vdash n_1\Diamond B , \Diamond \varDelta _1, k1 \), and is derived from the hypersequent \(\vDash _{\text {MGASR}^{\dag *}}\varGamma _1 , n_1 B \vdash n_1 B, \varDelta _1, k 1\). By induction hypotheses (B has smaller complexity than A), we have that \(\vDash _{\text {MGASR}^{\dag *}}\varGamma _1 \vdash \varDelta _1 , k 1\). Hence we can derive \(\vDash _{\text {MGASR}^{\dag *}}\Diamond \varGamma _1 \vdash \Diamond \varDelta _1, k 1\) by application of the \(\Diamond \)rule.

Otherwise, the hypersequent is derived by application of some other rule (not active on \(A=\Diamond B\)) from some premises. In this case, we simply apply the inductive hypothesis on the premises (the formula A is unchanged but the complexity of the premise derivation has decreased) and use the same rule to construct a derivation of the desired hypersequent.
