Curry and Howard Meet Borel

Melissa Antonelli
University of BolognaItaly

Ugo Dal Lago

University of BolognaItaly

Paolo Pistone
University of BolognaItaly

We show that an intuitionistic version of counting propositional logic
corresponds, in the sense of Curry and Howard, to an expressive type system
for the probabilistic event $\lambda$-calculus, a vehicle calculus
in which both call-by-name and call-by-value evaluation of discrete
randomized functional programs can be simulated.
Remarkably, proofs (respectively, types) do not only guarantee that validity (respectively, termination) holds, but also reveal the underlying probability. We finally show that by endowing the type system with an intersection operator, one obtains a system precisely capturing the probabilistic behavior of $\lambda$-terms.

§ INTRODUCTION

Among the many ways in which mathematical logic influenced programming language
theory, the so-called Curry-Howard correspondence is certainly among the most
intriguing and meaningful ones.
Traditionally, the correspondence identified by
Curry [13] and formalized by Howard [32] (CHC in the following) relates
propositional intuitionistic logic and the simply-typed
$\lambda$-calculus. As is well-known, though, this correspondence holds in
other contexts, too. Indeed, in the last fifty years more sophisticated type
systems have been put in relation with logical formalisms: from
polymorphism [25, 26] to various forms of session typing [52, 11], from control
operators [45] to dependent types [38, 50].

Nevertheless, there is a class of programming languages and type systems for
which a correspondence in the style of
the CHC has not yet been found. We are talking about languages with probabilistic effects, for which
type-theoretic accounts have recently been put forward in various ways, e.g. type
systems based on sized types [15], intersection types [9]
or type systems in the style
of so-called amortized analysis [56].
In all the aforementioned cases,
a type system was built by modifying well-known type systems for deterministic
languages without being guided by logic, and instead incepting
inherently quantitative
concepts directly from
probability theory.
So, one could naturally wonder if there is any logical
system behind all this, or
what kind of logic could possibly play the role of
propositional logic in suggesting meaningful and expressive type systems for a
$\lambda$-calculus endowed with probabilistic choice effects.

A tempting answer is to start from modal logic,
which is known to correspond in the Curry-Howard sense
to staged computation
and to algebraic effects [18, 60, 12].
Nevertheless, there is one aspect of randomized
computation that modal logic fails to capture[With a few notable exceptions,
e.g. [23].], namely the probability of
certain notable events, typically termination.
Indeed, several other properties like reachability and safety can be reduced to the termination property (see, e.g., the discussion in [35]).
In many of the probabilistic
type systems mentioned above, for example, a term $t$ receives a type that
captures the fact that $t$ has a certain probability $q$, perhaps strictly smaller
than $1$, of reducing to a value. This probability is an essential part of what we want to observe about the dynamics of $t$ and, as such, has to be captured by its
type, at least if one wants the type system to be expressive.

Recently, the authors have proposed to use counting quantifiers [3, 2] as a means to express probabilities within a logical language.
These quantifiers,
unlike standard ones, determine not only the
existence of an assignment of values to variables with certain
characteristics, but rather count how many of those assignments exist.
Recent works show that classical propositional logic
enriched with counting quantifiers
corresponds to Wagner's hierarchy of counting complexity classes [55] (itself intimately linked to
probabilistic complexity),
and that Peano Arithmetics enriched with similar quantitative quantifiers
yields a system capable of speaking of randomized computation in the same
sense in which standard PA models deterministic computation [3].
One may now wonder whether all this scale
to something like a proper CHC.

The aim of this work is precisely to give a positive answer to the aforementioned
question, at the same time highlighting a few
remarkable consequences of our study of probabilistic computation through the lens of logic.
More specifically,
the contributions of this paper are threefold:

First of all, we introduce an intuitionistic version of

Antonelli et al.'s counting propositional
logic [2], together with a Kripke-style semantics based on the Borel $\sigma$-algebra
of the Cantor space and a sound and complete proof-theory.
Then, we identify a “computational fragment” of this logic and we
design for it a natural deduction system in which proof normalization simulates
well-known evaluation strategies for probabilistic programs.
This is in
Section <ref>.

* We then show that derivations can be decorated with terms of the
probabilistic event $\lambda$-calculus, a
$\lambda$-calculus for randomized computation
introduced by Dal Lago et al. in [16]. This gives rise to a type-system called
$\LCPL$. Remarkably, the correspondence scales to the underlying dynamics,
i.e. proof normalization relates to reduction in the probabilistic event
$\lambda$-calculus. This is in Section <ref> and
Section <ref>.

* We complete the picture by giving an intersection type assignment system,
derived from $\LCPL$, and proving that it precisely captures the normalization
probability of terms of the quoted $\lambda$-calculus. This is in Section <ref>.

Space limits prevent us from being comprehensive, meaning that many technical
details will be unfortunately confined to the Appendix.

§ FROM LOGIC TO COUNTING AND PROBABILITY: A ROADMAP

In this section we provide a first overview of our probabilistic CHC,
at the same time sketching the route we will follow in the rest of
the paper.

§.§ Randomized Programs and Counting Quantifiers

The first question we should ask ourselves concerns the kind of programs we
are dealing with.
What is a probabilistic functional program?
Actually, it is a functional program with the additional ability of sampling from some
distributions, or to proceed by performing some form of discrete probabilistic
choice.[Here we are not at all concerned with sampling from continuous
distributions, nor with capturing any form of conditioning.]
This has a couple of crucial consequences: program evaluation becomes an
essentially stochastic process, and programs satisfy a given specification
up to a certain probability. As an example, consider the $\lambda$-term,

\Xi_{\mathsf{half}} :=\lambda x.\lambda y. x\oplus y

where $\oplus$ is a binary infix operator for fair probabilistic choice.
When applied to two arguments $t$ and $u$,
the evaluation on $\Xi_{\mathsf{half}}$
results in either $t$, with probability one half, or in $u$, again with
probability one half.

But now, if we try to take $\Xi_{\mathsf{half}}$ as a proof of some logical formula, we see that standard propositional logic is simply not
rich enough to capture the behavior above. Indeed, given that
$\Xi_{\mathsf{half}}$ is a function of two arguments, it is natural to see it
as a proof of an implication $A\to B\to C$, namely (following the BHK
interpretation) as a function turning a proof of
$A$ and a proof of $B$ into a proof of $C$. What is $C$, then? Should it be $A$
or should it be $B$? Actually, it could be both, with some degree of
uncertainty, but propositional logic is not able to express all this.
At this point, the recent work on counting quantifiers in propositional
logic [2]
comes to the rescue.

Another way to look at discrete probabilistic programs is
as programs which are allowed to sample an element $\omega$ from the
Cantor space $2^{\BB N}$. For example, a probabilistic Turing machine
$M$ can be described as a 2-tape machine where the second tape is read-only and
sampled from the Cantor space at each run.
Similarly, the execution of $\Xi_{\mathsf{half}}$ applied to programs $t$ and $u$ can be described as the result of sampling $\omega$ and returning either $t$ or $u$ depending on some read value, e.g. $\omega(0)$.
Crucially, for each input $x$ and each possible output $y$ of a probabilistic
program $f$, the set $S_{x,y}$ of elements in $2^{\BB N}$, making
$f(x)$ produce $y$, is a Borel set, so it makes sense to say that the
probability that $f(x)$ yields $y$ coincides with the measure of $S_{x,y}$
(more on Borel sets and measures below).

Yet, what has all this to do with logic and counting? The fundamental
observation is that formulas of classical propositional logic
provide ways of
denoting Borel sets.
Let $\bvar_{0},\bvar_{1},\dots$ indicate a countable set of propositional variables
(which can be seen as i.i.d. and uniformly distributed random variables $\bvar_{i}\in \{0,1\}$);
each variable $\bvar_{i}$ can be associated with the cylinder set (indeed, a Borel set of measure $\frac{1}{2}$)
formed by all $\omega\in 2^{\BB N}$ such that $\omega(i)=1$
(i.e., in logical terms, such that $\omega \vDash \bvar_{i}$).
Then, any propositional formula $\bone, \btwo,\dots$ formed by way of $\lnot,\land,\lor$ can be associated
with the Borel sets $\{\omega \in 2^{\BB N}\mid \omega \vDash\bone\}$ which can be constructed starting from cylinder sets
by means of complementation, finite intersection and finite unions.

In this way, for any Boolean formula $\bone$, it makes sense to define
new formulas like the formula $\B C^{\frac{1}{2}}\bone$, which is true when the Borel set associated with $\bone$ has measure greater than $\frac{1}{2}$ (i.e. when $\bone$ is satisfied by at least
$\frac{1}{2}$ of its models).
For instance, for any two distinct indexes $i,j\in \BB N$ (so that the variables $\bvar_{i},\bvar_{j}$ correspond to two independent events), the formula $\B C^{\frac{1}{2}}(\bvar_{i} \lor \bvar_{j})$ is
true, since the Borel set formed by the $\omega\in 2^{\BB N}$ such that either $\omega(i)=1$ or $\omega(j)=1$ has measure greater than $\frac{1}{2}$
$\bvar_{i} \lor \bvar_{j}$ is satisfied by at least $\frac{1}{2}$ of its models).

Instead, $\B C^{\frac{1}{2}}(\bvar_{i} \land \bvar_{j})$ is false, since, $\bvar_{i}$ and $\bvar_{j}$ being independent,
the Borel set associated with $\bvar_{i}\land \bvar_{j}$ has only measure $\frac{1}{4}$.

Counting propositional logic (from now on $\CPL$) is defined by enriching classical propositional logic with counting
quantifiers $\B C^{q}$,
where $q\in (0,1]\cap\BB Q$. Following our sketch, $\CPL$ admits a natural semantics in the
Borel $\sigma$-algebra of the Cantor space, together with a sound and complete
sequent calculus [2].
Notice that measuring a Boolean formula actually amounts at counting its models,
that is, to a purely recursive operation,
albeit one which needs not be doable in polynomial time
(indeed, $\CPL$ is deeply related to Wagner's counting hierarchy [2]).

Going back to the term $\Xi_{\mathsf{half}}$, what seems to be lacking in
intuitionistic logic is precisely a way
to express that $C$ could be $\B C^{\frac{1}{2}}A$, that is, that it could be
$A$ with probability at least $\frac{1}{2}$, and, similarly, that it could be
by $\B C^{\frac{1}{2}}B$.

In Section <ref> we introduce an intuitionistic version of $\CPL$, called $\ICPL$, which enriches
intuitionistic logic with Boolean variables

as well as the counting quantifier $\B C^{q}$.
Intuitively, if a proof
of a formula $A$ can be seen as a deterministic program satisfying the
specification $A$, a proof of $\B C^{q}A$
will correspond
to a probabilistic program that satisfies the specification $A$ with
probability $q$.
Our main result consists in showing that proofs in $\ICPL$
correspond to functional probabilistic programs and, most importantly, that
normalization in this logic describes probabilistic evaluation.

§.§ Can CbN and CbV Evaluation Coexist?

When studying probabilistic extensions of the $\lambda$-calculus, two different evaluation strategies are generally considered:
the call-by-name (CbN) strategy, which (possibly) duplicates choices before evaluating
them, and the call-by-value (CbV) strategy, which instead evaluates choices before (possibly) duplicating their outcomes.
Importantly, the probability of termination of a program might differ depending on the chosen strategy.
For example, consider the application of the term $\B 2:=\lambda y x.y(yx)$ (i.e. the second Church numeral)
$I\oplus \Omega$,

where $I=\lambda x.x$ and $\Omega$ is the diverging term $(\lambda x.xx)\lambda x.xx$.
Under CbN, the redex $\B 2(I\oplus\Omega)$ first produces $\lambda x.( I\oplus \Omega)(( I\oplus \Omega)x)$,
then reduces to any of the terms $\lambda x. u(vx)$, with $u,v$
chosen from $\{I,\Omega\}$, each with probability $\frac{1}{4}$.
Since $\lambda x. u(vx)$ converges only when $u=v=I$,
the probability of convergence is thus $\frac{1}{4}$.
Under CbV,  in $\B 2(I\oplus\Omega)$ one first has to evaluate $I\oplus\Omega$,
and then passes the result to $\B 2$, hence  returning
either the converging term $I(Ix)$ or the diverging term $\Omega(\Omega x)$,
each with probability $\frac{1}{2}$.

If we now try to think of the Church numeral $\B 2$ as a proof of some counting quantified formula, we see that, depending on the reduction strategy we have in mind, it must prove a different formula. Indeed,

given that $I\oplus\Omega$ proves $\B C^{\frac{1}{2}}(A\to A)$, in the CbN case, $\B 2$ proves
$\B C^{\frac{1}{2}}(A\to A) \to A\to  \B C^{\frac{1}{4}}A$, since only in one over four cases it yields a proof of $A$, while in the CbV case, $\B 2 $ proves the formula
$\B C^{\frac{1}{2}}(A\to A) \to  A\to \B C^{\frac{1}{2}}A$, as it yields a proof of $A$ in one case over two.

In the literature on probabilistic $\lambda$-calculi, the apparent
incompatibility of CbN and CbV evaluation is usually resolved by
restricting to calculi with one or the other strategy.
However, the observation above suggests that, if functional programs are typed using counting quantifiers, it should become possible
to make the two evaluation strategies coexist, by assigning them different

Actually,  a few
recent approaches [14, 19, 21, 16] already suggest ways to make CbN and CbV evaluation live together. In particular, in the
probabilistic event $\lambda$-calculus [16] the choice operator $\oplus$ is decomposed into two different operators, yielding a confluent calculus: a
choice operator $t\oplus_{a}u$, depending on some
probabilistic event $a\in\{0,1\}$,
and a probabilistic event generator $\nu a.t$, which
actually “flips the coin”.

In this language, the CbN and CbV applications of $\B 2$ to $I\oplus
\Omega$ are encoded by two distinct terms
$\B 2(\nu a.I\oplus_{a}\Omega)$ and
$\nu a. \B 2 ( I\oplus_{a}\Omega)$,

crucially distinguishing between generating a probabilistic choice before or after a duplication takes place.

This calculus constitutes then an ideal candidate for our CHC. Indeed, as we'll see, the logical rules for the counting quantifier $\B C^{q}$ naturally give rise to typing rules for the event generator $\nu a.$
In Section <ref> we introduce a variant $\EVLL$ of the calculus from [16],
with the underlying probability space $\{0,1\}$  replaced by
the Cantor space, and in

Section <ref> we introduce a type system $\LCPL$ for simple types with counting quantifiers, showing that natural deduction derivations translate into typing derivations in $\LCPL$, with
normalization precisely corresponding to reduction in $\EVLL$.

§.§ Capturing Probability of Normalization via Types

As observed in the Introduction, a fundamental quantitative property we would like to observe using types is the probability of termination.
Nevertheless, given that the reduction of $\EVLL$ is purely deterministic, what notions of probabilistic termination should we actually observe?

Rather than evaluating programs by implementing probabilistic choices,
reduction in the probabilistic event $\lambda$-calculus has the effect of progressively generating the full tree of outcomes of (sequences of) probabilistic choices, giving rise to a distribution of values.

Therefore, given a term $t$, rather than asking whether
some or all reductions of $t$ terminate, it makes sense to ask with what probability a normal form is found by generating all probabilistic outcomes of $t$.

In Section <ref> we will first show that when the type $\B C^{q}\sigma$ is assigned to a program $t$,
the value $q\in \mathbb{Q}\cap (0,1]$ provides a lower bound for the actual probability of finding a (head) normal form in the development of $t$.
Then we show that, by extending the type system with an intersection operator, one can attain an upper bound and thus fully characterize the distribution of values associated with a term.

§.§ Preliminaries on the Cantor Space

Throughout the paper, we exploit some basic facts about the Cantor space,
its Borel $\sigma$-algebra, and their connections with Boolean logic, that we briefly recall here.

We consider a countably infinite set $\CC A$ of names, noted $a,b,c,\dots$. For any finite subset $X\subseteq \CC A$, we let $\Borel_{X}$ (resp. $\Borel_{\CC A}$) indicate the Borel $\sigma$-algebra on the $X$-th product of the Cantor space $(2^{\BB N})^{X}$ (resp. on the $\CC A$-th product $(2^{\BB N})^{\CC A}$), that is, the smallest $\sigma$-algebra containing all open sets under the product topology.

There exists a unique measure $\mu$ of $\Borel_{\CC A}$ such that $\mu(C_{a,i})=\frac{1}{2}$ for all cylinders $C_{a,i}=\{\omega \mid \omega(a)(i)=1\}$. The measure $\mu$ restricts to a measure $\mu_{X}$ on $\Borel_{X}$ by
letting $\mu_{X}(S)=\mu(S\times (2^{\BB N})^{\CC A-X})$.

Boolean formulas with names in $\CC A$ are defined by:

\bone::= \TOP\mid\BOT \mid \bvar_{a}^{i}\mid\lnot \bone \mid  \bone \land \bone \mid \bone \lor \bone

where $a\in \CC A$ and $i\in \BB N$. We let $\FN(\bone)\subseteq \CC A$ be the set of names occurring in $\bone$.

For all Boolean formula $\bone$ and $X\supseteq\FN(\bone)$,
we let $\model{\bone}_{X}$ indicate the Borel set $\{\omega\in (2^{\BB  N})^{X}\mid \omega \vDash \bone\}$
(in particular, $\model{\bvar^i_a}_{\{a\}}=\{\omega \ | \ \omega(a)(i)=1\}$.
The value  $\mu_{X}(\model{\bone}_{X})\in [0,1]\cap\BB Q$ is independent from the choice of $X\supseteq \FN(\bone)$, and we will note it simply as $\mu(\bone)$.

§ INTUITIONISTIC COUNTING PROPOSITIONAL LOGIC

In this section we introduce a constructive version of $\CPL$, that we call $\ICPL$, which extends standard intuitionistic logic with Boolean variables and counting quantifiers.
The logic $\ICPL$ combines constructive reasoning (corresponding, under CHC, to functional programming) with  semantic reasoning on Boolean formulas and their models (corresponding, as we have seen, to discrete probabilistic reasoning). The formulas of $\ICPL$ are hybrid, that is, comprise both a countable set $\CC P=\{\CC p, \CC q, \dots\}$ of intuitionistic propositional variables, and named Boolean propositional variables $\bvar_{a}^{i}$.
For example, consider the formula below:

A:= \CC p \to \CC q \to (\bvar_{a}^{0}\land \CC p)\lor (\lnot \bvar_{a}^{0}\land \CC q).

Intuitively, proving $A$ amounts to showing that,
whenever $\CC p$ and $\CC q$ hold,
given that either $\bvar_{a}^{0}$ or $\lnot\bvar_{a}^{0}$ holds,
in the first case $\CC p$ holds, and in the second case $\CC q$ holds.

Suppose we test $A$ against some element $\omega$ from the Cantor space.
A way of proving $A$, in the “environment” $\omega$, could then be as follows:
given assumptions $\CC p$ and $\CC q$, conclude $\CC p$ and $\bvar_{a}^{0}$ if $\omega(0)=1$ (i.e. if $\omega$ satisfies $\bvar_{a}^{0}$),
and conclude $\CC q$ and $\lnot \bvar_{a}^{0}$ if $\omega(0)=0$ (i.e. if $\omega$ does not satisfy $\lnot\bvar_{a}^{i}$). In other words, a proof of $A$ under $\omega$ could be something like $\lambda xy. x\oplus_{a}y$.

Assuming that $\omega$ is uniformly sampled, what are the chances that our strategy will actually yield a proof of $A$?
Well, there are two possible cases, and in both cases we get a proof of one of the disjuncts
$\bvar_{a}^{0}\land\CC p$
and $\lnot\bvar_{a}^{0}\land \CC q$, thus a proof of $A$.
We thus obtain a proof of $A$ with probability 1 or, in other words,

a proof of $\B C^{1}_{a}A$ (no more depending on any “environment”). As a term, this proof looks then precisely as the closed term $\nu a.\lambda xy.x\oplus_{a}y$.

Consider now another formula:

B:= \CC p \to \CC q \to \bvar_{a}^{0}\land \CC p.

Given some $\omega$, a proof $B$ should conclude, from assumptions $\CC p$ and $\CC q$, both $\CC p$ and $\bvar_{a}^{0}$ when $\omega(0)=1$, but when $\omega(0)=0$, it needs not conclude anything, since we have nothing to prove in this case. A proof of $B$ should then be something like $\lambda xy.x\oplus_{a}?$, where $?$ can be any program. By uniformly sampling $\omega$, we get then a proof of $B$ only in one half of the cases, i.e. we get a proof of $\B C^{\frac{1}{2}}_{a}B$.

§.§ The Semantics and Proof-Theory of $\ICPL$.

The formulas of the logic just sketched are defined by:

A::= \TOP\mid \BOT\mid \bvar_{a}^{i}\mid \CC p\mid A\land A\mid A\lor A\mid A\to A\mid \B C^{q}_{a}A

where $\CC p\in \CC P$ and $q\in (0,1]\cap \BB Q$.
A natural semantics for $\ICPL$-formulas can be given in terms of Kripke-like structures:

An $\ICPL$-structure is a triple $\CC M=(W, \preceq , \B i)$ where $W$ is a countable set, $\preceq$ is a preorder on $W$,
and $\B i: \CC P\to W^{\uparrow}$, where $W^{\uparrow}$ is the set of upper subsets of $W$.

The interpretation of formulas in
$\ICPL$-structures combines a set $W$ of worlds (for the interpretation of intuitionistic propositional variables) with the choice of  an element of the Cantor space (for the interpretation of Boolean variables):
for any $\ICPL$-structure $\CC M=(W,\preceq,  \B i)$ and finite set $X$, we define the relation $w,\omega \Vdash^{X}_{\CC M}A$ (where $w\in W$, $\omega \in (2^{\BB N})^{X}$ and $\FN(A)\subseteq X$) by induction as follows:

* $w, \omega \not\Vdash_{\CC M}^{X} \BOT$ and $w, \omega \Vdash_{\CC M}^{X} \TOP$;

* $w, \omega \Vdash^{X}_{\CC M}   \bvar_{a}^{i}$ iff $\omega(a)(i)=1$;

* $w, \omega \Vdash^{X}_{\CC M}   \CC p$ iff  $w\in \B i(\CC p)$;

* $w,\omega \Vdash^{X}_{\CC M}   A\land B$ iff $w,\omega \Vdash^{X}_{\CC M}   A$ and $w,\omega \Vdash^{X}_{\CC M}    B$;

* $w,\omega \Vdash^{X}_{\CC M}   A\lor B$ iff $w,\omega \Vdash^{X}_{\CC M}   A$ or $w,\omega \Vdash^{X}_{\CC M}    B$;

* $w,\omega \Vdash^{X}_{\CC M}   A\to B$ iff for all $w'\succeq w$,
$w', \omega \Vdash^{X}_{\CC M}  A$ implies $w',\omega \Vdash^{X}_{\CC M}   B$;

* $w,\omega \Vdash^{X}_{\CC M}  \B C^{q}_{a}A$ iff
$\mu\left (\left \{ \omega'\in 2^{\BB N} \mid w, \omega+ \omega'\Vdash^{X\cup\{a\}}_{\CC M}A\right\}\right)\geq q
$, where $\omega+\omega'\in (2^{\BB N})^{X\cup\{a\}}$ is given by $
(\omega+\omega')(b)(n)=\omega(b)(n)$, for $b\in X$, and

Using properties of the Borel $\sigma$-algebra $\Borel_{X}$, it can be shown that for any $w\in W$ and formula $A$, the set $\{\omega\in (2^{\BB N})^{X}\mid w,\omega \Vdash^{X}_{\CC M}A\}$ is a Borel set, and thus measurable.

We write $\Gamma \Vdash^{X}_{\CC M}  A$ when for all $w\in W$ and $\omega \in (2^{\BB N})^{X}$,
whenever $w,\omega \Vdash^{X}_{\CC M}  \Gamma$ holds, also
$w,\omega \Vdash^{X}_{\CC M}  A$ holds.

We write $\Gamma \vDash A$ when for any $\ICPL$-structure $\CC M$ and $X\supseteq\FN(A)$, $\Gamma \Vdash^{X}_{\CC M}  A$ holds.

A sound and complete proof system for $\ICPL$ can be defined.
Indeed, starting from usual natural deduction for intuitionistic logic, one obtains a calculus $\NDCPL$ for $\ICPL$
by adding the excluded middle $\bvar_{a}^{i}\vee \lnot \bvar_{a}^{i}$ as an axiom for Boolean variables,
as well as suitable rules and axioms for counting quantifiers (details can be found in App. <ref>).

$\Gamma \vDash A$ iff $\Gamma\vdash_{\NDCPL}A$.

For example, $\B C^{q}$ admits an introduction rule as below

\begin{align}\label{rule0}
\AXC{$\Gamma, \bthree \vdash A$}
\AXC{$\mu(\bthree)\geq q$}
\BIC{$\Gamma \vdash \B C^{q}_{a}A$}
\DP
\tag{$\B C$I}
\end{align}

with the proviso that $a$ does not occur in $\Gamma$, and is the only name occurring in $\bthree$. Intuitively, this rule says that if we can prove $A$ under assumptions $\Gamma$ and $\bthree$, and if a randomly chosen valuation of $a$ has chance $q$ of being a model of $\bthree$, then we can build a proof of $\B C^{q}_{a}A$ from $\Gamma$.
Observe that the rule ($\B C$I) has a semantic premise $\mu(\bthree)\geq q$: we ask to an oracle to count the models of $\bthree$ for us (this is similar to what happens in sequent calculi for $\CPL$, see [2]).

§.§ The Computational Fragment of $\ICPL$.

From the perspective of the CHC, however, the natural deduction system just sketched is not what we are looking for. As $\ICPL$ contains Boolean logic, in order to relate proofs and programs, one should first choose among the several existing constructive interpretations of classical logic.
Yet, in our previous examples Boolean formulas were never those to be proved; rather, they were used as semantic constraints that programs may or may not satisfy (for example, when saying that a program, depending on some event $\omega$, yields a proof of $A$ when $\omega$ satisfies $\bone$, or that
a program has $q$ chances of yielding a proof of $A$ when $\bone$ has measure at least $q$).

Would it be possible, then, to somehow separate purely constructive reasoning from Boolean semantic reasoning within formulas and proofs of $\ICPL$? The following lemma suggests that this is indeed possible.

For any formula $A$ of $\ICPL$ there exist Boolean formulas $\bone_{v}$ and purely intuitionistic formulas $A_{v}$ (i.e. formulas containing no Boolean variables), where $v$ varies over all possible  valuations of the Boolean variables in $A$,
such that

$$\vDash A \leftrightarrow \bigvee_{v} \bone_{v}\land A_{v}$$

The idea is to let
$\bone_{v}$ be the formula characterizing $v$, i.e. the
conjunction of all variables true in $v$ and of all negations of variables false in $v$, and let  $A_{v}$ be obtained from $A$ by replacing each Boolean variable by either $\TOP$ or $\BOT$, depending on its value under $v$.

By Lemma <ref>, any sequent $\Gamma\vdash A$ of $\ICPL$ can be associated with a family of intuitionistic sequents of the form
$\Gamma_{v}, \bone_{v}\vdash A_{v}$ where $v$ ranges over all valuations of the Boolean variables of $\Gamma$ and $A$, and $\Gamma_{v},\bone_{v},A_{v}$ are as in Lemma <ref>.
We will note such special sequents as $\Gamma_{v}\vdash \bone_{v}\Pto A_{v}$, in order to highlight the special role played by the Boolean formula $\bone_{v}$.

The sequents $\Gamma \vdash \bone\Pto A$ have a natural computational interpretation: they express program specifications of the form “$\Pi$ yields a proof of $A$ from $\Gamma$ whenever its sampled function satisfies $\bone$”.

By the way, Lemma <ref>,
ensures that, modulo Boolean reasoning,
logical arguments in $\ICPL$ can be reduced to (families of) arguments of this kind.

Let then $\ICPLL$ be the fragment formed by the purely intuitionistic formulas of $\ICPL$, which are defined by:

A::= \CC p\midd A\to A \midd \BOX^{q}A

where $q\in (0,1]\cap \BB Q$.
For simplicity, and since this is enough for the CHC, we take here implication as the only connective,
yet all other propositional connectives could be added.
As formulas do not contain Boolean variables, counting quantifiers in $\ICPLL$ are not named.
We use $\B C^{q_{1}* \dots * q_{n}}A$ (or even $\B C^{\vec q}$, for simplicity) as an abbreviation for $\B C^{q_{1}}\dots \B C^{q_{n}}A$.

The natural deduction system $\NDCPLL$ for $\ICPLL$ is defined by the rules illustrated in Fig. <ref>
(where in ($\B C$I) it is assumed that $\FN(\bone)\cap \FN(\bthree)=\emptyset$).
A few rules involve semantic premises of the forms $\bone \vDash \btwo$ and $\mu(\bone)\geq q$.

Beyond standard intuitionistic rules, $\NDCPLL$ comprises structural rules to manipulate Boolean formulas, and introduction and elimination rules for the counting quantifier.
The rule ($\BOT$) yields dummy proofs of any formula, i.e. proofs which are correct for no possible event; the rule ($\mathsf m$)
combines two proofs $\Pi_{1},\Pi_{2}$ of the same formula into one single proof $\Pi'$,
with the choice depending on the value of some Boolean variable $\bvar_{a}^{i}$ ($\Pi'$ is thus something like $\Pi_{1}\oplus_{a}\Pi_{2}$).
The introduction rule for $\B C^{q}$ is similar to rule (<ref>). It is explained as follows: if $\Pi$, in the “environment” $\omega+\omega'\in(2^{\BB N})^{X\cup\{a\}}\simeq(2^{\BB N})^{X} \times 2^{\BB N}$, yields a proof of $A$ whenever $\omega+\omega'$
satisfies the two independent constraints $\bone$ and $\bthree$ (i.e. $\omega\vDash \bone$ and $\omega'\vDash \bthree$), then by randomly choosing $\omega'\in 2^{\BB N}$, we have at least $q\geq \mu(\bthree)$ chances of getting a proof of $A$
($\Pi'$  is thus something like $\nu a.\Pi$).
Finally, the elimination rule ($\B C$E) essentially turns a proof of $A\to B$ into a proof of $\B C^{q}A\to \B C^{qs}B$. As we'll see, this rule captures CbV function application.

Identity Rule

\AXC{}
\RL{(id)}
\UIC{$ \Gamma,A \vdash \bone \Pto A$}
\DP
%\UIC{$ \ ; \Gamma, A \vdash \bone \Pto A$}

Structural Rules

%\AXC{$\Gamma \vdash \btwo\Pto A$}
%\AXC{$\bone \vDash \btwo$}
%\BIC{$\Gamma \vdash \bone \Pto A$}
\AXC{$\bone \vDash \BOT$}
\RL{($\BOT$)}
\UIC{$\Gamma \vdash \bone \Pto A$}
\DP

\AXC{$\Gamma \vdash \btwo \Pto A$}
\AXC{$\Gamma \vdash \bthree \Pto A$}
\AXC{$\bone \vDash (\btwo \land \bvar_{a}^{i})\lor (\bthree \land \lnot \bvar_{a}^{i})$}
\RL{($\mathsf m$)}
\TIC{$\Gamma \vdash \bone \Pto A$}
\DP

Logical Rules

\AXC{$ \Gamma, A \vdash \bone \Pto B$}
\RL{($\to$I)}
\UIC{$\Gamma \vdash \bone \Pto (A\to B)$}
\DP

\AXC{$ \Gamma \vdash \bone \Pto (A\to B)$}
\AXC{$ \Gamma \vdash \bone \Pto A$}
\RL{($\to$E)}
\BIC{$\Gamma \vdash \bone \Pto B$}
\DP

Counting Rules

\AXC{$\Gamma \vdash \bone \land \bthree\Pto A$}
\AXC{$\mu(\bthree)\geq q$}
\RL{($\BOX$I)}
\BIC{$\Gamma \vdash \bone \Pto \BOX^{q}A$}
\DP

\AXC{$\Gamma \vdash \bone \Pto \BOX^{q}A$}
\AXC{$ \Gamma, A \vdash \bone \Pto B$}
\RL{($\BOX$E)}
\BIC{$\Gamma \vdash \bone \Pto \BOX^{qs}B$}
\DP

Rules of $\NDCPLL$.

Fig. <ref> illustrates a proof $\Pi_{\frac{1}{2}\mathsf{id}}$ of $\B C^{\frac{1}{2}}(A\to A)$ obtained by first “mixing” an exact proof of $A\to A$ with a dummy one, and then introducing the counting quantifier.
Fig. <ref> illustrates a derivation of
$ \B C^{q}(A\to A) \to A \to \B C^{q*q}B$.

\Pi_{\frac{1}{2}\mathsf{id}}\quad  =   \quad
\AXC{$A\vdash \bvar_{a}^{i}\Pto A$}
\RL{($\to$I)}
\UIC{$\vdash \bvar_{a}^{i}\Pto (A\to A)$}
\AXC{}
\RL{($\BOT$)}
\UIC{$\vdash \BOT \Pto (A\to A)$}
\AXC{$\bvar_{a}^{i}\vDash (\bvar_{a}^{i}\land \bvar_{a}^{i})\lor (\lnot\bvar_{a}^{i}\land \BOT)$}
\RL{($\mathsf m$)}
\TIC{$\vdash \bvar_{a}^{i}\Pto (A\to A)$}
\AXC{$\mu(\bvar_{a}^{i})\geq \frac{1}{2}$}
\RL{($\B C$I)}
\BIC{$\vdash \B C^{\frac{1}{2}}(A\to A)$}
\DP

$     $=$     $
\AXC{$\B C^{q}(A\to A), A \vdash \B C^{q}(A\to A)$}
\AXC{$A\to A, A \vdash A\to A$}
\AXC{$A\to A, A \vdash A$}
\RL{($\to$E)}
\BIC{$A\to A, A \vdash A$}
\RL{($\B C$E)}
\BIC{$\B C^{q}(A\to A), A \vdash \B C^{q}A$}
\AXC{$\B C^{q}(A\to A), A,A \vdash \B C^{q}(A\to A)$}
\AXC{$A\to A, A,A \vdash A\to A$}
\AXC{$A\to A, A,A \vdash A$}
\RL{($\to$E)}
\BIC{$A\to A,A, A \vdash A$}
\RL{($\B C$E)}
\BIC{$\B C^{q}(A\to A), A,A \vdash \B C^{q}A$}
\RL{($\B C$E)}
\BIC{$\B C^{q}(A\to A),A \vdash \B C^{q*q}A$}
%\RL{($\B C_{\times}$)}
%\UIC{$\B C^{q}(A\to A), A \vdash \B C^{q^{2}}A$}
\doubleLine
\RL{($\to$I)}
\UIC{$\vdash \B C^{q}(A\to A)\to  A\to \B C^{q*q}A$}
\DP
%\AXC{$\alpha, B, \B C^{q}B\vdash \B C^{q}B$}
%\AXC{$\alpha, B, \B C^{q}B\vdash \alpha$}
%\AXC{$\alpha, B, \B C^{q}B\vdash B$}
%\BIC{$\alpha, B, \B C^{q}B \vdash B\to B$}
%\AXC{$\alpha, B, \B C^{q}B\vdash B$}
%\BIC{$\alpha, B, \B C^{q}B \vdash B $}
%\RL{($\B C$E)}
%\BIC{$\alpha, \B C^{q}B \vdash \B C^{q}B$}
%\UIC{$ \vdash \B C^{q}(A\to A)\to  A \to \B C^{q^{2}}A$}

Examples of derivations in $\NDCPLL$.

A precise connection between the proof systems for
$\ICPL$ and $\ICPLL$ is discussed in Appendix <ref>.

§.§ Normalization in $\ICPLL$

From the CHC perspective, natural deduction proofs correspond to programs, and normalization corresponds to execution. Let us look at normalization in $\ICPLL$, then.

The two main normalization steps are ($\to$I/$\to$E) and ($\B C$I/$\B C$E).

The cuts ($\to$I/$\to$E) are eliminated, as usual,
by means of the admissible substitution rule

\AXC{$\Gamma \vdash\bone\Pto A$}
\AXC{$\Gamma , A\vdash \bone\Pto B$}
\RL{(subst)}
\BIC{$\Gamma \vdash \bone\Pto B$}
\DP

The normalization step ($\B C$I/$\B C$E), illustrated in Fig. <ref>,
also applies the rule (subst) to the premiss of ($\B C$I) and the minor premiss of ($\B C$E), and permutes the rule ($\B C$I) downwards.

For example, if we cut the proof $\Pi$ from Fig. <ref> with $\Pi_{\frac{1}{2}\mathsf{id}}$ from Fig. <ref> (by letting $q=\frac{1}{2}$), normalization duplicates $\Pi$, that is, it duplicates the choice between the correct and the dummy proof of $A\to A$, yielding a normal proof of $A\to \B C^{\frac{1}{2}*\frac{1}{2}}A$.

The other normalization steps (illustrated in App. <ref>) permute ($\mathsf m$) with other rules, and  correspond to the permuting reductions for the probabilistic $\lambda$-calculus introduced in the next section.

To make the study of normalization as simple as possible, we did not consider a “multiplication rule” to pass from $\B C^{q}\B C^{s}A$ to $\B C^{qs}A$, as this would introduce other normalization steps. Nevertheless, in App. <ref> we study an alternative  “CbN” proof-system $\NDCPLL$ also comprising this rule.

As a by-product of the CHC developed in the following sections, we will obtain a strong normalization theorem for $\ICPLL$ (Corollary <ref>).

In Section <ref> it will be shown (Prop. <ref>) that, once proofs in $\NDCPLL$ are seen as probabilistic programs, the two normalization steps ($\to$I/$\to$E) and
($\B C$I/$\B C$E) simulate CbN and CbV evaluation, respectively.

$\Gamma \vdash \bone \land \bthree  \Pto A$
$\mu(\bthree  )\geq q$
($\B C$I)
$\Gamma \vdash \bone \Pto \B C^{q}A$
$\Gamma,A \vdash \bone \Pto B$
($\B C$E)
$\Gamma \vdash \bone \Pto \B C^{qs}B$

$\Gamma \vdash \bone \land \bthree  \Pto A$
$\Pi$$[\bone\mapsto \bone\land \bthree]$
$\Gamma,A \vdash \bone  \land \bthree\Pto B$

$\Gamma \vdash \bone \land \bthree  \Pto B$
$\mu(\bthree)\geq qs$
($\B C$I)
$\Gamma \vdash \bone\Pto \B C^{qs}B$

Normalization step ($\B C$I)/($\B C$E) of $\NDCPLL$.

§ THE PROBABILISTIC EVENT LAMBDA CALCULUS

In this section we introduce the computational side of the CHC, that is, a variant of the probabilistic event $\lambda$-calculus $\EVL$ from [16], with choices depending on events from the Cantor space. We will then discuss how terms of $\EVL$ yield distributions of values, and we define two notions of probabilistic normalization for such distributions. We finally introduce a further variant $\EVLL$ of $\EVL$ which provides a smoother representation of CbV functions.

§.§ A $\lambda$-Calculus Sampling from the Cantor Space

The terms of $\EVL$ are defined by the grammar below:

t::= x\midd \lambda x.t\midd tt\midd t\oplus_{a}^{i}u \midd \nu a.t

with $a\in \CC A$, and $i\in \mathbb N$. The intuition is that
$\nu a.$ samples some function $\omega$ from the Cantor space, and
$t\oplus_{a}^{i}u$ yields either $t$ or $u$ depending on the value $\omega(a)(i)\in\{0,1\}$.
In the following we let $t\oplus^{i} u$ be an abbreviation for $\nu a.t\oplus_{a}^{i}u$ (supposing $a$ does not occur free in either $t$ or $u$).

For any term $t$, finite set $X$ and $\omega \in (2^{\BB N})^{X}$, let
$\pi^{\omega}_{X}(t)$, the “application of $\omega$ to $t$ through $X$”, be defined as:

\begin{align*}
\pi^{\omega}_{X}(x)& =x \\
\pi^{\omega}_{X}(\lambda x.t)& =\lambda x.\pi^{\omega}_{X}(t) \\
\pi^{\omega}_{X}(tu)& =\pi^{\omega}_{X}(t)\pi^{\omega}_{X}(u) \\
\pi^{\omega}_{X}(t\oplus_{a}^{i}u) &= \begin{cases}
\pi^{\omega}_{X}(t) & \text{ if }a\in X \text{ and } \omega(a)(i)=1 \\
\pi^{\omega}_{X}(u) & \text{ if }a\in X \text{ and } \omega(a)(i)=0 \\
\pi^{\omega}_{X}(t) \oplus_{a}^{i}\pi^{\omega}_{X}(u)& \text{ otherwise}
\end{cases}\\
\pi^{\omega}_{X}(\nu b.t) & = \nu b. \pi^{\omega}_{X}(t)
\end{align*}

In usual randomized $\lambda$-calculi, program execution is defined so as to be inherently probabilistic: for example a term $t\oplus u$ can reduce to either $t$ or $u$, with probability $\frac{1}{2}$. In this way, chains of reduction can be described as stochastic Markovian sequences [47], leading to formalize the idea of normalization with probability $r\in[0,1]$ (see [8]).

By contrast, reduction in $\EVL$ is fully deterministic: beyond the usual (and un-resticted) $\beta$-rule $(\lambda x.t)u \redbeta t[u/x]$, it comprises a permutative reduction $t\redperm u$ defined by the rules in Fig. <ref> (where $(a,i)<(b,j)$ if either $\nu b$ occurs in the scope of $\nu a$, or $a=b$ and $i<j$).
Intuitively, permutative reductions implement probabilistic choices by computing the full tree of possible choices.
For example, given terms $t_{1},t_{2}, u_{1},u_{2}$, one can see that the term
$\nu a.(t_{1}\oplus_{a}^{0}t_{2})(u_{1}\oplus_{a}^{1}u_{2})$ reduces to $
\nu a.  (t_{1}u_{1}\oplus_{a}^{1} t_{1}u_{2}) \oplus_{a}^{0}( t_{2}u_{1}\oplus_{a}^{1} t_{2}u_{2})
$, hence displaying all possible alternatives.

\begin{align*}
%(\lambda x.t)u &\to_{\beta} t[u/x] \\
% & \\
t\oplus_{a}^{i}t & \redperm t  \tag{$\mathsf{i}$} \\
(t\oplus_{a}^{i}u)\oplus_{a}^{i} v & \redperm t\oplus_{a}^{i}v \tag{$\mathsf{c}_{1}$}\label{eq:c1} \\
t\oplus_{a}^{i}(u\oplus_{a}^{i}v) & \redperm t\oplus_{a}^{i}v  \tag{$\mathsf{c}_{2}$} \\
\lambda x.(t\oplus_{a}^{i}u) & \redperm (\lambda x.t)\oplus_{a}^{i} (\lambda x.u)  \tag{$\oplus\lambda$} \\
(t\oplus_{a}^{i}u)v & \redperm (tu)\oplus_{a}^{i}(uv)  \tag{$\oplus\mathsf{f}$} \\
t(u\oplus_{a}^{i}v) & \redperm (tu)\oplus_{a}^{i}(tv)  \tag{$\oplus\mathsf{a}$}\label{eq:oa} \\
(t\oplus_{a}^{i}u)\oplus_{b}^{j} v & \redperm (t\oplus_{b}^{j}v)\oplus_{a}^{i}(u\oplus_{b}^{j}v) & ((a,i)< (b,j)) \tag{$\oplus\oplus_{1}$}  \\
t\oplus_{b}^{j}(u\oplus_{a}^{i} v) & \redperm (t\oplus_{b}^{j}u)
\oplus_{a}^{i}(t\oplus_{b}^{j} v) & ((a,i)<(b,j))
\tag{$\oplus\oplus_{2}$}
\\
\nu b. (t\oplus_{a}^{i} u) & \redperm (\nu b.t)\oplus_{a}^{i}(\nu b.u) &  (a\neq b)
\tag{$\oplus\nu$}\label{eq:cnu} \\
\nu a.t & \redperm t &  (a\notin \FN(t))
\tag{$\lnot\nu$}\label{eq:notnu}\\
\lambda x.\nu a.t & \redperm \nu a. \lambda x.t
\tag{$\nu\lambda$}\label{eq:nulambda}\\
(\nu a.t)u  & \redperm  \nu a.(tu)\tag{$\nu\mathsf{f}$}\label{eq:nuapp}
\end{align*}

Permutative reductions.

The fundamental properties of $\EVL$ are the following:

$\redperm$ is confluent and strongly normalizing.
Full reduction  $\redall\ := \ \redbeta\cup \redperm$ is confluent.

The existence and unicity of normal forms for $\redperm$ (that we call permutative normal forms, PNFs for short) naturally raises the question of what these normal forms represent.

Let $\CC T$ indicate the set of PNFs containing no free name occurrence.
For any $t\in \CC T$, the PNF of $t$ can be of two forms:
either $t$ starts with a generator, i.e. $t=\nu a.t'$, and $t'$ is a tree of $a$-labeled choices $\oplus_{a}^{i}$ whose leaves form a finite set of $\CC T$ (the support of $t'$, $\mathrm{supp}(t)$).
Otherwise, $t$ is of the form
$\lambda x_{1}.\dots.\lambda x_{n}.t't_{1}\dots t_{p}$, where $t'$ is either a variable or a $\lambda$. We call these last terms pseudo-values, and we let $\CC V\subseteq \CC T$ indicate the set formed by them.

Using this decomposition, any $t\in \CC T$ can be associated in a unique way with a (sub-)distribution of pseudo-values $\CC D_{t}: \CC V\to [0,1]$ by letting $\CC D_{t}(v)=\delta_{t}$ when $t\in \CC V$, and

\CC D_{t}(v) =  \sum_{u\in \mathrm{supp}(t')}\CC D_{u}(v) \cdot \mu(\{\omega\in 2^{\BB N}\mid \pi^{\omega}_{\{a\}}(t')=u\})

if $t=\nu a.t'$. Intuitively, $\CC D_{t}(v)$ measures the probability of finding $v$ by iteratively applying to $t$ random choices of events from the Cantor space any time a $\nu$ is found.

§.§ Probabilistic (Head) Normalization.

Given a term $t\in \CC T$, the questions “is $t$ in normal form?” and “does $t$ reduce to a normal form?” have univocal yes/no answers, because $\redall$ is deterministic. However, if we think of $t$ rather as $\CC D_{t}$, the relevant questions become “with what probability is $t$ in normal form?” and “with what probability does $t$ reduce to normal form?”.

To answer this kind of questions we will introduce functions $\NHNF(t)$, $\NNF(t)$ measuring the probability that $t$ reduces to a normal form.

Let us consider head-normal forms, first.
A head-reduction $t\redall_{\mathsf h} u$ is either a $\redperm$-reduction or a $\redbeta$-reduction
of the form
$\TT R[\lambda \vec x.(\lambda y.t)uu_{1}\dots u_{n}]\redbeta \TT R[\lambda \vec x.t[u/x]u_{1}\dots u_{n}]$,
where $\TT R$ is a randomized context, defined by the grammar

\TT R[\ ]::= [\ ]\mid \TT R[\ ]\oplus_{a}^{i}u \mid t\oplus_{a}^{i}\TT R[\ ]\mid  \nu a. \TT R[\ ].

A head normal value (in short, HNV) is a $\redall_{\mathsf h}$-normal term which is also a pseudo-value, i.e. it is of the form $\lambda \vec x.yu_{1}\dots u_{n}$. We let $\HNF$ indicate the set of such terms.

For any $t\in \CC T$,
$\HNF(t) :=\sum_{v\in \HNF}\CC D_{t}(v)$ and
$\NHNF(t):= \sup\{ \HNF(u)\mid t\redall_{\mathsf h}^{*} u\}$.
When $\NHNF(t)\geq q$, we say that $t$ yields a HNV with probability at least $q$.

For example, if $t= \nu a. (\lambda x\lambda y.(y\oplus_{a}^{i}I )x)u$, where $u= I \oplus^{j}\Omega$, then $\NHNF(t)= \frac{3}{4}$. Indeed,  we have

$$t\redall^{*}_{\mathsf h} \nu a.( \lambda y. y(\nu b.I\oplus_{b}^{j}\Omega)) \oplus_{a}^{i} (\nu b'.I\oplus_{b'}^{j} \Omega)$$

three over the four possible choices (corresponding to choosing between either left or right for both $\nu a$ and $\nu b'$) yield a HNV. Observe that the choice about $\nu b$ does not matter, since $\lambda y.yu$ is already a HNV.

Let us now consider normal forms. The first idea might be to define a similar function $\NF(t)=\sum_{v \text{ normal form}}\CC D_{t}(v)$.
However, with this definition a term like $t=\lambda x.x(\nu a. I \oplus_{a}^{0}\Omega)$ would have probability 0 of yielding a normal form. Instead, our guiding intuition here is that $t$ should yield a normal form with probability $\frac{1}{2}$, i.e. depending on a choice for $a$.
This leads to the following definition:

For any $t\in \CC T$, $\NF(t)$ is defined by:

* if $t=\lambda \vec x.yu_{1}\dots u_{n}\in \HNF$, then $\NF(t):= \prod_{i=1}^{n}\NF(u_{i})$;

* otherwise $\NF(t):= \sum_{u\in \HNF}\NF(u)\cdot \CC D_{t}(u)$.

We let $\NNF(t)=\sup\{\NF(u)\mid t\redall^{*}u\}$ and, if $\NNF(t)\geq q$, we say that $t$ yields a normal form with probability at least $q$.

For example, for the term $t$ considered above, $\NNF(t)=\frac{4}{8}=
\frac{1}{2}$: four over the eight possible choices for $\nu a$, $\nu b$ and $\nu b'$ yield a normal form (i.e. either choose left for $\nu a$ and $\nu b$ and choose anything for $\nu b'$, or
choose right for $\nu a$, left for $\nu b'$, and choose anything for $\nu b$).

§.§ Extending $\EVL$ with CbV Functions

$\EVL$ makes it possible to encode a CbV redex like $\nu a. \B 2 (I\oplus_{a}^{0}\Omega)$, as we have seen. However,
in view of the functional interpretation of $\ICPLL$, it would be convenient also to be able to represent the CbV functions mapping $\nu a. (u\oplus_{a}v) $ onto $\nu a.\B 2 (u\oplus_{a}^{0}v)$.

A simple way to do this is by enriching the language of $\EVL$ with a “CbV application” operator $\{t\}u$, with suitable permutative rules. Let $\EVLL$ indicate this extension of terms of $\EVL$ with $\{\}$. While $\beta$-reduction for $\EVLL$ is the same as for $\EVL$, permutative reduction $\redpermm$ is defined by all rules in Fig. <ref> except for (<ref>), together with the three permutations below

\begin{align*}
\{t\} \nu a. u & \ \redpermm \ \nu a. tu \tag{$\{\}\nu$} \label{eq:e0}\\
\{t\oplus_{a}^{i}u\} v & \ \redpermm \ \{t\}v \oplus_{a}^{i}\{t\} v \tag{$\{\}\oplus_{1}$}\label{eq:e1} \\
\{t\} (u \oplus_{a}^{i}v) & \ \redpermm \ \{t\}u \oplus_{a}^{i}\{t\} v\tag{$\{\}\oplus_{2}$}\label{eq:e2}
\end{align*}

For instance, a CbV Church numeral can be encoded in $\EVLL$ as $ {\B 2}^{\mathrm{CbV}}:=\lambda f. \{\B 2 \}f
$, since one has ${\B 2}^{\mathrm{CbV}}(\nu a.u\oplus_{a}^{i}v) \redbeta
\{\B 2\} \nu a.u\oplus_{a}^{i}v \redpermm
\nu a. \B 2 (u\oplus_{a}^{i}v)$.

The fundamental properties of $\EVL$ extend to $\EVLL$:

$\redpermm$ is confluent and strongly normalizing.
Full reduction  $\redalll\ := \ \redbeta\cup \redpermm$ is confluent.

In the Appendix <ref> it is shown how the definitions of $\CC D_{t}$ and $\NHNF(t)$ extend to terms of $\EVLL$.

§ THE CORRESPONDENCE, STATICALLY AND DYNAMICALLY

In this section we present the core of the CHC. First, we introduce two type systems $\TCI$ and $\LCPL$ for $\EVL$ and $\EVLL$, respectively, which extend the simply typed $\lambda$-calculus with counting quantifiers. Then, we show that each proof $\Pi$ in $\ICPLL$ can be  associated with a typing derivation in $\LCPL$ of some probabilistic term $t^{\Pi}$, in such a way that normalization of $\Pi$ corresponds to reduction of $t^{\Pi}$.
Observe that translating the rule ($\B C$E) requires the CbV application operator $\{\}$. In the Appendix <ref> we show that an alternative “CbN” proof-system for $\ICPLL$ can be translated without $\{\}$, and thus into $\TCI$.

§.§ Two Type Systems with Counting Quantifiers

Both type systems $\TCI$ and $\LCPL$ extend the simply typed $\lambda$-calculus with counting quantifiers, but in a slightly different way: in $\TCI$ types are of the form $\B C^{q}\FF s$, i.e. prefixed by exactly one counting quantifier, while in $\LCPL$ types are of the form $\B C^{\vec q}\FF s$, i.e. prefixed by a (possibly empty) list of counting quantifiers.

More precisely, the types (denoted $\FF s, \FF t$) of $\TCI$ and $\LCPL$ are generated by the grammars below:

\begin{align*}
\FF s &  :: = \B C^{ q}\sigma  &  \sigma &::=o\midd \FF s\To \sigma
\tag{$\TCI$}\\
\FF s &  :: = \B C^{\vec q}\sigma  &  \sigma &::=o\midd \FF s\To \sigma
\tag{$\LCPL$}
\end{align*}

where, in both cases, the $q$s are chosen in $(0,1]\cap \BB Q$.

Judgements in both systems are of the form $\Gamma \vdash^{X} t: \bone \Pto \FF s$, where $\Gamma$ is a set of type declarations $x_{i}: \FF s_{i}$ of pairwise distinct variables, $t$ is a term of $\EVL$ (resp. of $\EVLL$), $\bone$ a Boolean formula, and $X$ a finite set of names with $\FN(t), \FN(\bone)\subseteq X$.

The intuitive reading of $\Gamma \vdash^{X} t: \bone \Pto \FF s$ is that, whenever $\omega\in (2^{\BB N})^{X}$ satisfies $\bone$, then $\pi^{\omega}_{X}(t)$ is a program from $\Gamma$ to $\FF s$.

The typing rules of $\LCPL$, which are essentially derived from those of $\ICPLL$, are illustrated in Fig. <ref>, where in the rule ($\mu$) it is assumed that $\FN(\bone)\subseteq X$, $\FN(\bthree)\subseteq \{a\}$ and $a\notin X$.
The rule ($\vee$) allows one to merge $n$ typing derivations for the same term; in particular, with $n=0$, one has that $\Gamma \vdash^{X}t: \BOT \Pto \FF s$ holds for any term $t$.
The rule ($\oplus$) is reminiscent of the rule ($\mathsf m$) of $\ICPLL$,
the rule ($\mu$) is reminiscent of the rule ($\B C$I) of $\ICPLL$, while the rule ($\{\}$) for CbV application is reminiscent of the rule ($\B C$E).

The typing rules of $\TCI$ coincide with those of $\LCPL$ (with $\B C^{\vec q}$ replaced everywhere by $\B C^{q}$), except for the rule ($\{\}$), which is obviously absent, and for the rule ($\mu$), which is adapted as follows to the presence of exactly one counting quantifier:

\AXC{$\Gamma \vdash^{X\cup\{a\}}t:\bone\land \bthree \Pto \B C^{q}\sigma$}
\AXC{$\mu(\bthree)\geq s$}
\RL{($\mu'$)}
\BIC{$\Gamma \vdash^{X}\nu a.t:\bone \Pto \B C^{qs}\sigma$}
\DP

Identity rule:

\AXC{$\mathrm{FN}(\bone)\subseteq X$}
\RL{(id)}
\UIC{$\Gamma, x:\FF s \vdash^{X} x: \bone \Pto \FF s $}
\DP

Structural rule:

\AXC{$
\Big\{ \Gamma \vdash^{X}t: \bone_{i}\Pto \FF s\Big\}_{i=1,\dots,n}$}
\AXC{$\bone \vDash^{X}\bigvee_{i}\bone_{i}$}
\RL{$(\lor)$}
\BIC{$\Gamma \vdash^{X}t: \bone\Pto \FF s$}
\DP

Plus rule:

\AXC{$ \Gamma \vdash^{X\cup\{a\}}t: \btwo\Pto \FF s$}
\AXC{$ \Gamma \vdash^{X\cup\{a\}}u: \bthree\Pto \FF s$}
\AXC{$\bone \vDash (\bvar_{a}^{i}\land \btwo)\lor(\lnot \bvar_{a}^{i}\land \bthree)$}
\RL{$(\oplus)$}
\TIC{$\Gamma \vdash^{X\cup\{a\}} t\oplus^{i}_{a}u :  \bone\Pto \FF s$}
\DP

Arrow rules:

\AXC{$\Gamma, x:\FF s \vdash^{X} t: \bone\Pto \B C^{\vec q}\tau$}
\RL{$(\lambda)$}
\UIC{$\Gamma \vdash^{X} \lambda x.t : \bone\Pto \B C^{\vec q}(\FF s\To \tau)$}
\DP

$$\AXC{$\Gamma \vdash^{X}t:\btwo\Pto  \B C^{\vec q}(\FF s \To \tau)$}
\AXC{$ \Gamma \vdash^{X} u: \bthree\Pto \FF s$}
\AXC{$\bone\vDash^{X}\btwo\land \bthree$}
\RL{$(@)$}
\TIC{$\Gamma \vdash^{X} tu: \bone\Pto \B C^{\vec q}\tau$}
\DP

$$\AXC{$\Gamma \vdash^{X}t:\btwo\Pto \B C^{\vec q}(\FF s \To \tau)$}
\AXC{$ \Gamma \vdash^{X} u: \bthree\Pto \B C^{r}\FF s$}
\AXC{$\bone\vDash^{X}\btwo\land \bthree$}
\RL{$(\{ \})$}
\TIC{$\Gamma \vdash^{X} \{t\}u: \bone\Pto \B C^{rs}\B C^{\vec q} \tau$}
\DP

Counting rule:

\AXC{$\Gamma \vdash^{X\cup \{a\}} t: \bone\land \bthree\Pto \FF s$}
\AXC{$\mu(\bthree)\geq q$}
%\AXC{$\bthree_{i}\land \bthree_{j}\vDash \BOT\quad (i\neq j)$}
%\AXC{$\bone \vDash \btwo$}
\RL{$(\mu)$}
\BIC{$\Gamma \vdash^{X} \nu a.t: \bone\Pto \B C^{q}\FF s$}
\DP

Typing rules of $\LCPL$.

Both systems enjoy the subject reduction property:

[Subject Reduction]propositionsubje
If $\Gamma \vdash^{X}t: \bone \Pto \FF s$ in $\TCI$ (resp. in $\LCPL$) and $t \redall u$ (resp. $t\redalll u$), then
$\Gamma \vdash^{X}u: \bone \Pto \FF s$.

The choice of considering arrow types of the form $\B C^{\vec q}(\FF s\To \sigma)$ (hence of never having a counting quantifier to the right of $\To$, as in e.g.  $\FF s\To \B C^{q}\sigma$) was made to let the rule ($\lambda$) be permutable over ($\mu$), as required by the permuting rule (<ref>).

Fig. <ref> illustrates typing derivations in $\LCPL$ for a version of the CbN Church numeral $\B 2^{\mathrm{CbN}}= \lambda y.\lambda x.\{y\}(yx)$, with type
$\B C^{q*q}(\B C^{q}(o\To o)\To (o\To o))$, and for the CbV numeral
$\B 2^{\mathrm{CbV}}$ with type $\B C^{q}(\B C^{q}(o\To o)\To (o\To o))$.

Both $\TCI$ and $\LCPL$ can type non-normalizable terms. For example, one can type all terms of the form
$I\oplus^{i}\Omega$ with  $\B C^{\frac{1}{2}}(o\To o)$ in $\LCPL$ and with
$\B C^{\frac{1}{2}}(\B C^{1}o\To o)$ in $\TCI$.

Actually, the failure of normalization for typable programs can be ascribed to the rule ($\vee$), as shown by the result below, proved in App. <ref> (where we let

$\Gamma \vdash_{\lnot \vee}t:\bone \Pto \FF s$ indicate that
$\Gamma \vdash t:\bone \Pto \FF s$ is deduced without using the rule ($\vee$)).

[Deterministic Normalization]theoremdetnormalization
In both $\TCI$ and $\LCPL$, if $\Gamma \vdash_{\lnot \vee} t: \bone \Pto \FF s$, then $t$ is strongly normalizable.

As observed in the previous section, restricting to terms of $\EVL$ having a normal form
the most interesting part of the calculus, which is made of terms for which normalization is inherently probabilistic. Similarly, restricting to type derivations without ($\vee$) trivializes the most interesting features of $\TCI$ and $\LCPL$,
that is, their ability to estimate probabilities of termination. We will explore the expressiveness of these systems in this sense
in the next section.

\AXC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash y:\TOP \Pto \B C^{q}(o\To o)$}
\AXC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash y:\TOP \Pto \B C^{q}(o\To o)$}
\AXC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash x:\TOP \Pto o$}
\RL{($@$)}
\BIC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash yx:\TOP\Pto \B C^{q}o$}
\RL{($\{\}$)}
\BIC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash \{y\}(yx): \TOP\Pto \B C^{q*q}o$}
\doubleLine
\RL{($\lambda$)}
\UIC{$\vdash \B 2^{\mathrm{CbN}}: \TOP \Pto \B C^{q*q}(\B C^{q}(o\To o)\To (o\To o))$}
\DP

\AXC{$\vdots$}
\noLine
\UIC{$y: \B C^{q}(o\To o) \vdash \B 2:\TOP \Pto (o\To o)\To (o\To o)$}
\AXC{$y: \B C^{q}(o\To o) \vdash y:\TOP \Pto \B C^{q}(o\to o)$}
\RL{($\{\}$)}
\BIC{$y: \B C^{q}(o\To o) \vdash \{\B 2\}y: \TOP\Pto \B C^{q}(o\To o)$}
% \AXC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash y:\TOP \Pto \B C^{q}(o\to o)$}
%  \AXC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash x:\TOP \Pto o$}
%  \RL{($@$)}
% \BIC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash yx:\TOP\Pto \B C^{q}o$}
% \RL{($\{\}$)}
% \BIC{$y: \B C^{q}(o\To o), x: \B C^{q}o \vdash \{y\}(yx): \TOP\Pto \B C^{q}\B C^{q}o$}
\RL{($\lambda$)}
\UIC{$\vdash \B 2^{\mathrm{CbV}}: \TOP \Pto \B  C^{q}(\B C^{q}(o\To o)\To (o\To o))$}
\DP

Typing of CbN and CbV Church numerals in $\LCPL$.

§.§ Translating $\ICPLL$ into $\LCPL$.

We now show how derivations in $\ICPLL$ translate into typing derivations in $\LCPL$.
In the Appendix <ref> a similar translation of a “CbN” proof-system for $\ICPLL$ into $\TCI$ is shown.

For any formula $A$ of $\ICPLL$, let us define a corresponding type $\FF s_{A}$ by letting
$\FF s_{\CC p}:= o$, $\FF s_{A\to \B C^{\vec q}B}:=\B C^{\vec q}(\FF s_{A}\To \FF s_{B})$ and $\FF s_{\B C^{q}A}:= \B C^{q}\FF s_{A}$.
Fig. <ref> shows how a derivation $\Pi$ of $\Gamma \vdash \bone \Pto A$ in $\ICPL$ translates into a typing derivation $D^{\Pi}$ of $\FF s_{\Gamma} \vdash t^{\Pi}: \bone \Pto \FF s_{A}$ in $\LCPL$, with $\FN(t^{\Pi})\subseteq \FN(\bone)$, by induction on $\Pi$.
Notice that we exploit a special constant $\B c$ to translate the rule ($\BOT$).

\AXC{$ \Gamma \vdash^{X} t: \btwo \Pto \FF s$}
\AXC{$\bone \vDash \btwo$}
\RL{($\vDash$)}
\BIC{$\Gamma \vdash^{X} t: \bone \Pto \FF s$}
\DP

Moreover, the rule ($\to$E) translates as CbN application $tu$, while the rule ($\B C$E) translates as CbV application $\{t\}u$.

As required by the CHC, normalization steps of $\ICPLL$ are simulated by $\redalll$-reductions:

If $\Pi \leadsto\Pi'$, then $t^{\Pi} \redalll^{*}t^{\Pi'}$.

The normalization steps in Fig. <ref> translate into the following reductions:

\begin{align*}
(\lambda x^{\B C^{q}\FF s_{A}}.t^{\Pi}) \nu a. t^{\Sigma} &  \ \redbeta \
t^{\Pi}[ \nu a.t^{\Sigma} /x ]  \\
%The normalization step in Fig.~\ref{fig:cutelim2} translates into the CbV reduction:
\{\lambda x^{\FF s_{A}}.t^{\Pi}\} \nu a. t^{\Sigma} &  \ \redpermm \
\nu a.(\lambda x^{\FF s_{A}}.t^{\Pi}) t^{\Sigma} \ \redbeta \
\nu a. t^{\Pi}[ t^{\Sigma}/x ]
\end{align*}

All other normalization steps translate into $\redpermm$-reductions.

Notice that the normalization step ($\to$I/$\to$E) translates into CbN reduction (i.e. plain $\beta$-reduction): the “choice” $\nu a.t^{\Sigma}$ is directly substituted, and thus possibly duplicated; instead the
($\B C$I/$\B C$E) translates into CbV reduction (i.e. (<ref>) followed by $\beta$-reduction): the generator $\nu a$ is first permuted down and only $t^{\Sigma}$ is substituted.

By observing that the only use of ($\vee$) coming from the translation introduces a constant $\B c$, from Theorem <ref> we deduce, as promised, the following:

$\ICPLL$ is strongly normalizing.

\AXC{}
\RL{(id)}
\UIC{$\Gamma, A \vdash \bone\Pto A$}
\DP$

\AXC{}
\RL{(id)}
\UIC{$\FF s_{\Gamma}, x: \FF s_{A} \vdash x:\bone\Pto \FF s_{A}$}
\DP

\AXC{$\bone \vDash \BOT$}
\RL{($\BOT$)}
\UIC{$\Gamma \vdash \bone\Pto A$}
\DP$

\AXC{$\bone \vDash \BOT$}
\RL{($\vee$)}
\UIC{$\FF s_{\Gamma} \vdash \B c:\bone\Pto \FF s_{A}$}
\DP

$\Gamma \vdash \btwo \Pto A$
$\Gamma \vdash \bthree \Pto A$
$\bone \vDash (\btwo \land \bvar_{a}^{i})\lor (\bthree \land \lnot \bvar_{a}^{i})$
($\mathsf m$)
$ \Gamma \vdash \bone \Pto A$

$\mapsto $

$ \FF s_{\Gamma}\vdash t^{\Pi}: \btwo \Pto A$
$\FF s_{\Gamma}\vdash t^{\Pi'}: \bthree \Pto A$
$\bone \vDash (\btwo \land \bvar_{a}^{i})\lor (\bthree \land \lnot \bvar_{a}^{i})$
$ \FF s_{\Gamma}\vdash t^{\Pi}\oplus_{a}^{i}t^{\Pi'}: \bone \Pto \FF s_{A}$

$\Gamma,A \vdash \bone \Pto B$
$ \Gamma \vdash \bone \Pto (A\to B)$

$\mapsto $

$ \FF s_{\Gamma},x:\FF s_{A}\vdash t^{\Pi}: \bone \Pto \FF s_{B}$
$ \FF s_{\Gamma}\vdash \lambda x.t^{\Pi}: \bone \Pto (\FF s_{A\to B})$

$\Gamma\vdash \bone \Pto (A\to \B C^{\vec q}B)$
$\Gamma\vdash \bone \Pto A$
$ \Gamma \vdash \bone \Pto  \B C^{\vec q}B$

$\mapsto $

$\FF s_{\Gamma}\vdash t^{\Pi}: \bone \Pto\B C^{\vec q} (\FF s_{A}\to \FF s_{B})$
$\FF s_{\Gamma}\vdash t^{\Sigma}: \bone \Pto \FF s_{A}$
$ \FF s_{\Gamma}\vdash t^{\Pi}t^{\Sigma}: \bone \Pto \B C^{\vec q} \FF s_{B}$

$\Gamma\vdash \bone\land \bthree \Pto A$
$\mu(\bthree)\geq q$
($\B C$I)
$\Gamma \vdash \bone \Pto \B C^{q}A$

$\mapsto $

$ \FF s_{\Gamma}\vdash t^{\Pi}: \bone \land \bthree \Pto \FF s_{A}$
$\mu(\bthree)\geq q$

$\FF s_{\Gamma}\vdash \nu a.t^{\Pi}: \bone \Pto \FF s_{\B C^{q}A}$

$\Gamma\vdash \bone \Pto \B C^{q}A$
$\Gamma,A\vdash \bone \Pto \B C^{\vec s}B$
($\B C$E)
$\Gamma \vdash \bone \Pto  \B C^{qs}\B C^{\vec s}B$

$\mapsto $

$ \FF s_{\Gamma}\vdash t^{\Pi}: \bone \Pto \B C^{q}\FF s_{A}$
$\FF s_{\Gamma},x:\FF s_{A}\vdash t^{\Sigma}: \bone \Pto \B C^{\vec s} \FF s_{B}$
$\FF s_{\Gamma } \vdash \lambda x.t^{\Sigma}: \bone \Pto \B C^{\vec s}(\FF s_{A}\To \FF s_{B})$
($\{ \}$)
$ \FF s_{\Gamma}\vdash \{\lambda x.t^{\Sigma}\}t^{\Pi}: \bone \Pto   \FF s_{\B C^{qs}\B C^{\vec s}B}$

Translation $\Pi\mapsto D^{\Pi}$ from $\NDCPLL$ to $\LCPL$.

§ FROM TYPE SOUNDNESS TO TYPE COMPLETENESS: INTERSECTION TYPES

In this section we first show that derivations in $\TCI$ and $\LCPL$ provide sound approximations of $\HNF(t)$ and $\NF(t)$.
In order to achieve completeness, we then introduce an extension $\TCINT$ of $\TCI$ with intersection types and show that this system fully captures both deterministic and probabilistic notions of termination for $\EVL$.

§.§ From Types to Probability

We already observed, through examples, that if a term $t$ has a type like, e.g. $\B C^{\frac{1}{2}}(o\To o)$, then $t$ has one chance over two of yielding a “correct” program for $o\To o$.
The result below makes this intuition precise, by showing that the probabilities derived in $\TCI$ and $\LCPL$ are lower bounds for the function $\NHNF(t)$, that is, for the actual probability of finding a head normalizable term in the distribution $\CC D_{t}$.

If $ \vdash_{\TCI} t: \TOP \Pto \B C^{q}\sigma$, then $\NHNF(t)\geq q$.
If $ \vdash_{\LCPL} t: \TOP \Pto \B C^{q_{1}*\dots *q_{n}}\sigma$, then $\NHNF(t)\geq \prod_{i=1}^{n}q_{i}$.

What about reduction to normal form, i.e. the function $\NNF(t)$?
A result like Theorem <ref> cannot hold in this case. Indeed, consider the term $t=\lambda y.y(I\oplus^{i}\Omega)$. While $\NF(t)=\frac{1}{2}$, $\LCPL$ types $t$ with $\FF s=\B C^{1}(\B C^{1}(\B C^{\frac{1}{2}}\sigma\To \sigma)\To \sigma)$, with $\sigma=o\To o$.
The problem in this example is that the type $\FF s$ contains the “unbalanced” assumption
$\B C^{1}(\B C^{\frac{1}{2}}\sigma\To \sigma)$ (in logical terms, $\B C^{\frac{1}{2}}A\to \B C^{1}A$), i.e. it exploits the assumption of the existence of a function turning a $\frac{1}{2}$-correct input into a $1$-correct output.
Notice that such a function $f$ can only be one that erases its input, and these are the only functions such that $tf$ can reduce to a normal form.

Nevertheless, soundness with respect to $\NF(t)$ can be proved, for $\TCI$, by restricting to those types not containing such “unbalanced” assumptions, i.e. to types whose programs cannot increase probabilities.

A type $\B C^{q}(\FF s_{1}\To \dots \To \FF s_{n}\To o)$ of $\TCI$ is balanced if
all $\FF s_{i}$ are balanced and
$q\leq \prod_{i=1}^{n}\srank{\FF s_{i}}$
(where for any type $\FF s=\B C^{q}\sigma$, $\srank{\FF s}=q$).

If $ \vdash_{} t: \TOP \Pto \B C^{q}\sigma$ holds in $\TCI$, where $\sigma$ is balanced, then $\NNF(t)\geq q$.

Theorems <ref> and <ref> are proved by adapting the standard technique of reducibility predicates to the quantitative notion of probabilistic normal form (for further details, see App. <ref>).

§.§ From Probability to (Intersection) Types

To achieve a type-theoretic characterization of $\NHNF(t)$ and $\NNF(t)$, we  introduce an extension of $\TCI$ with intersection types.
Like those of $\TCI$, the types of $\TCINT$ are of the form $\FF s=\B C^{q}\sigma$, but $\sigma$ is now defined as:

\begin{align*}
%\FF s& ::= \B C^{q}\sigma &
\sigma & ::= o\midd \NORM\midd \HNORM \midd \FF M\To \sigma &
\FF M& ::=  [\FF s, \dots, \FF s]
\end{align*}

where $[a_{1},\dots, a_{n}]$ indicates a finite set.
While $\FF M$ intuitively stands for a finite intersection of types, the new ground types $\NORM$ and $\HNORM$ basically correspond to the types of normalizable and head-normalizable programs.

We introduce a preorder $\sigma \preceq \tau$ over types by $\alpha\preceq \alpha$, for $\alpha=o,\NORM, \HNORM$, $\B C^{q}\sigma \preceq \B C^{s}\tau$ if $q\leq s$ and $\sigma \preceq \tau$,  and
$(\FF M\To\sigma) \preceq (\FF N\To \tau)$ if $\sigma\preceq \tau$ and $\FF N\preceq^{*} \FF M$, where
$[\FF s_{1},\dots, \FF s_{n}]\preceq^{*} [ \FF t_{1},\dots, \FF t_{m}]$ holds is there exists an injective function $f: \{1,\dots, m\}\to \{1,\dots, n\}$ such that $ \FF s_{f(i)}\preceq \FF t_{i}$.

A type judgment of $\TCINT$ is of the form $\Gamma \vdash^{X}t:\bone \Pto \FF s$, where $\Gamma$ is made of declarations of the form $x_{i}:\FF M_{i}$.
The typing rules of $\TCINT$ are illustrated in Fig. <ref>. We omit the ($\vee$)- and ($\oplus$)-rules, which are as in $\TCI$.
In the rule ($\mu_{\Sigma}$) it is assumed that $a$ does not occur in $\bone$, is the only name in the $\bthree_{i}$, and that for $i\neq j$, $\bthree_{i}\land \bthree_{j}\vDash \BOT$.

The two rules ($\HNORM$) and ($\NORM$) are justified by Proposition <ref> and Theorem <ref> below. As rule ($\NORM$) must warrant a bound on normal forms, following Theorem <ref>, $\sigma$ has to be

safe, i.e. balanced[Definition <ref> extends to the types of $\TCINT$ by letting
$\srank{\HNORM}=\srank{[]}=0$, $\srank{\NORM}=1$ and $\srank{[\FF s_{1},\dots, \FF s_{n+1}]}=\max\{\srank{\FF s_{i}}\}$.] and $\{[],\HNORM\}$-free.
The rule ($@_{\cap}$) is a standard extension of rule ($@$) of $\TCI$ to finite intersections.

The counting rule ($\mu_{\Sigma}$) requires some discussion. The rule admits $n+1$ major premisses expressing typings for $t$ which depend on pairwise disjoint events (the Boolean formulas $\bthree_{i}$).
This is needed to cope with situations as follows: let

\begin{align*}
t[a,b] & =\Big ((I \oplus_{b}^{1}\Omega)\oplus_{b}^{0}\Omega\Big ) \oplus_{a}^{0}\Big (\Omega \oplus_{b}^{0} I\Big)
\end{align*}

$t[a,b]$ can be given type $\sigma=(\B C^{1}o)\To o$ under either of the two disjoint Boolean constraints
$\bthree_{1}:= \bvar_{a}^{0}\land (\bvar_{b}^{0}\land \bvar_{b}^{1})$ and $ \bthree_{2}:=\lnot\bvar_{a}^{0}\land \lnot\bvar_{b}^{0}$.
In $\TCI$, the best we can achieve to measure the probability that $\nu a.\nu b.t[a,b]$ has type $\sigma$ is $\frac{1}{4}$. Indeed, the rule ($\mu'$) forces us
to approximate $\mu(\bvar_{b}^{0}\land \bvar_{b}^{1})$ and $\mu(\lnot \bvar_{b}^{1})$ to a common lower bound, i.e. $\frac{1}{4}$, in order to apply a ($\vee$)-rule as illustrated in Fig. <ref>. Instead, using ($\mu_{\Sigma}$) we can compute (again, see Fig. <ref>), the actual probability $
\mu(\bvar_{a}^{0})\mu(\bvar_{b}^{0}\land \bvar_{b}^{1})+ \mu(\lnot \bvar_{a}^{0})\mu(\lnot\bvar_{b}^{0})=
\frac{1}{2}\cdot \frac{1}{4} + \frac{1}{2}\cdot \frac{1}{2} = \frac{3}{8}$.

Thanks to the rule ($\mu_{\Sigma}$), the generalized counting rule ($\mu^{*}$) below becomes admissible in $\TCINT$:

\AXC{$\Gamma\vdash^{\{a_{1},\dots, a_{n}\}}t: \bone \Pto  \B C^{q}\sigma$}
\RL{($\mu^{*}$)}
\UIC{$\Gamma \vdash^{\emptyset}\nu a_{1}.\dots. \nu a_{n}.t: \TOP \Pto \B C^{ q\cdot \mu(\bone)} \sigma$}
\DP

This rule plays an essential role in the completeness results below, together with the standard result that both subject reduction and subject expansion hold for intersection types.

Identity rule:

\AXC{$\FF s_{i}\preceq \FF t$}
\AXC{$\mathrm{FN}(\bone)\subseteq X$}
\RL{(id$_{\preceq}$)}
\BIC{$\Gamma, x:[\FF s_{1},\dots, \FF s_{n}] \vdash^{X} x: \bone \Pto \FF t  $}
\DP

Ground types rules:

\AXC{$\Gamma \vdash^{X}t: \bone \Pto \B C^{q}\sigma$}
\RL{($\HNORM$)}
\UIC{$\Gamma \vdash^{X}t: \bone \Pto \B C^{q}\HNORM$}
\DP
\qquad
\AXC{$\Gamma \vdash^{X}t: \bone \Pto \B C^{q}\sigma$}
\AXC{$\sigma$ safe}%$\{[],\HNORM\}$-free}
\RL{($\NORM$)}
\BIC{$\Gamma \vdash^{X}t: \bone \Pto \B C^{q}\NORM$}
\DP

Arrow rules:

\AXC{$\Gamma, x:\FF M \vdash^{X} t: \bone\Pto \B C^{q}\tau$}
\RL{$(\lambda)$}
\UIC{$\Gamma \vdash^{X} \lambda x.t : \bone\Pto \B C^{q} (\FF M\To \tau)$}
\DP

$$\AXC{$\Gamma \vdash^{X}t:\bone\Pto  \B C^{q}([\FF s_{1},\dots, \FF s_{n}] \To \tau)$}
\AXC{$ \Big\{\Gamma \vdash^{X} u: \bone\Pto \FF s_{i}\Big\}_{i=1,\dots,n}$}
%\AXC{$\bone\vDash^{X}\btwo\land \bthree$}
\RL{$(@_{\cap})$}
\BIC{$\Gamma \vdash^{X} tu: \bone\Pto \B C^{q} \tau$}
\DP

Counting rule:

\AXC{$\Big\{\Gamma \vdash^{X\cup \{a\}} t: \bone\land \bthree_{i}\Pto\B C^{q_{i}} \sigma\Big\}_{i=1,\dots,n+1}$}
\AXC{$\mu(\bthree_{i})\geq s_{i}$}
%\AXC{$\bthree_{i}\land \bthree_{j}\vDash \BOT\quad (i\neq j)$}
%\AXC{$\bone \vDash \btwo$}
\RL{$(\mu_{\Sigma})$}
\BIC{$\Gamma \vdash^{X} \nu a.t: \bone\Pto\B C^{\sum_{i}q_{i}s_{i}} \sigma$}
\DP

Typing rules of $\TCINT$.

\AXC{$\Gamma\vdash^{\{a,b\}} t[a,b]:  \bvar_{a}^{0}\land (\bvar_{b}^{0}\land \bvar_{b}^{1})\Pto\B C^{1}\sigma$}
\AXC{$\mu(\bvar_{b}^{0}\land \bvar_{b}^{1})\geq 1/4$}
\RL{$(\mu')$}
\BIC{$\Gamma \vdash^{\{a\}}\nu b.t[a,b]: \bvar_{a}^{0}\Pto \B C^{\frac{1}{4}}\sigma$}
\AXC{$\Gamma\vdash^{\{a,b\}} t[a,b]: \lnot \bvar_{a}^{0}\land \lnot\bvar_{b}^{0}\Pto\B C^{1} \sigma$}
\AXC{$\mu(\lnot\bvar_{b}^{0})\geq 1/4$}
\RL{$(\mu')$}
\BIC{$\Gamma \vdash^{\{a\}}\nu b.t[a,b]: \lnot\bvar_{a}^{0}\Pto \B C{\frac{1}{4}}\sigma$}
\RL{($\vee$)}
\BIC{$\Gamma \vdash^{\{a\}}\nu b.t[a,b]: \bvar_{a}^{0}\lor\lnot\bvar_{a}^{0}\Pto \B C{\frac{1}{4}}\sigma$}
\AXC{$\mu( \bvar_{a}^{0}\lor \lnot \bvar_{a}^{0})\geq 1$}
\RL{$(\mu')$}
\BIC{$\Gamma \vdash^{\emptyset}\nu a.\nu b.t[a,b]:\TOP \Pto \B C^{ \frac{1}{4}} \sigma$}
\DP

\AXC{$\Gamma\vdash^{\{a,b\}} t[a,b]:  \bvar_{a}^{0}\land (\bvar_{b}^{0}\land \bvar_{b}^{1})\Pto\B C^{1}\sigma$}
\AXC{$\mu(\bvar_{b}^{0}\land \bvar_{b}^{1})\geq 1/4$}
\RL{$(\mu_{\Sigma})$}
\BIC{$\Gamma \vdash^{\{a\}}\nu b.t[a,b]: \bvar_{a}^{0}\Pto \B C^{\frac{1}{4}}\sigma$}
\AXC{$\Gamma\vdash^{\{a,b\}} t[a,b]: \lnot \bvar_{a}^{0}\land \lnot\bvar_{b}^{0}\Pto\B C^{1} \sigma$}
\AXC{$\mu(\lnot\bvar_{b}^{0})\geq 1/2$}
\RL{$(\mu_{\Sigma})$}
\BIC{$\Gamma \vdash^{\{a\}}\nu b.t[a,b]: \lnot\bvar_{a}^{0}\Pto \B C{\frac{1}{2}}\sigma$}
\AXC{$\mu( \bvar_{a}^{0}), \mu( \lnot \bvar_{a}^{0})\geq 1/2$}
\RL{$(\mu_{\Sigma})$}
\TIC{$\Gamma \vdash^{\emptyset}\nu a.\nu b.t[a,b]:\TOP \Pto \B C^{ \frac{1}{4}\cdot \frac{1}{2}+ \frac{1}{2} \cdot \frac{1}{2}} \sigma$}
\DP

Comparing probabilities derived with the rules ($\mu'$) and ($\mu_{\Sigma}$).

If $\Gamma \vdash^{X}t: \bone \Pto \FF s$ and either $t\redall u$ or $u\redall t$, then
$\Gamma \vdash^{X}t: \bone \Pto \FF s$.

We will now discuss how typings in $\TCINT$ capture both deterministic and probabilistic properties of terms.
First we have the following facts, which show that the types $\HNORM$ and $\NORM$ capture deterministic termination.

[Deterministic Completeness]propositiondetcomple
For any closed term $t$,

(i.) $t$ is head-normalizable iff $\vdash_{\lnot \vee} t: \TOP \Pto \B C^{1}\HNORM$;

(ii.) $t$ is normalizable iff $\vdash_{\lnot \vee} t: \TOP \Pto \B C^{1}\NORM$.

(iii.) $t$ is strongly normalizable iff $\vdash_{\lnot \vee} t: \TOP \Pto \B C^{1}\NORM$ and all types in the derivation are safe.

Using standard intersection types arguments, it is shown that $\vdash_{\lnot \vee} t: \TOP \Pto \B C^{1}\HNORM$ holds for any head-normal $t$. The first half of (i.) is deduced then using Proposition <ref>.
The second half follows from a normalization argument similar to that of Theorem <ref>.
Cases (ii.) and (iii.) are similar.

The probabilistic normalization theorems <ref> and <ref> (which extend smoothly to $\TCINT$) ensure that if $t$ has type $\B C^{q}\HNORM$ (resp. $\B C^{q}\NORM$), then $\NHNF(t)\geq q$ (resp. $\NNF(t)\geq q$).

Conversely, $\NHNF(t)$ and $\NNF(t)$ can be bounded by means of derivations in $\TCINT$, in the following sense:

[Probabilistic Completeness]theoremcompletenessa
For any closed term $t$,

\begin{align*}
\NHNF(t) & = \sup \{ q\mid\  \vdash t: \TOP \Pto \B C^{q}\HNORM\} \\
\NNF(t) & = \sup \{ q\midd \  \vdash t: \TOP \Pto\B C^{q} \NORM\}
\end{align*}

Suppose w.l.o.g. that $t=\nu a_{1}.\dots.\nu a_{k}.t'$.
For any $u\in \HNF$ such that $\CC D_{t}(u)>0$, we can deduce $\vdash u:\TOP\Pto \HNORM$. The sequence of probabilistic choices leading to $u$ is finite, and thus captured by a Boolean formula $\bone_{t\mapsto u}$.
Using subject reduction/expansion we thus deduce $\vdash t': \bone_{t\mapsto u}\Pto \HNORM$.
Hence, for any finite number of head normal forms $u_{1},\dots, u_{n}$, we deduce $\vdash t': \bone_{t\mapsto u_{i}}\Pto \HNORM$. Using ($\vee$) and the generalized counting rule ($\mu^{*}$) we deduce then $\vdash t: \TOP \Pto \B C^{s}\HNORM$, where $s= \sum_{i=1}^{n}\mu(\bone_{t\mapsto u_{i}})=\mu(\bigvee_{i=1}^{n}\bone_{t\mapsto u_{i}})$.

The argument for $\NF(t)$ is similar.

§ RELATED WORK

As discussed in the introduction, our results provide the first clear correspondence between a proof system and a probabilistic extension of the $\lambda$-calculus. This is not to say that our logic and calculi come from nowhere.

Different kinds of measure-theoretic quantifiers have been investigated in the literature, with the intuitive meaning of “$A$ is true for almost all $x$”,
see [41, 51] and more recently [39, 40], or
“$A$ is true for the majority of $x$” [44, 59, 58].
Our use of the term “counting quantifier” comes from [2], where an extension of classical propositional logic with such quantifiers is studied and related to Wagner's counting operator on classes of languages [53, 55, 54].
To our knowledge, the present work is the first to apply some form of measure quantifier to typed probabilistic functional programs.

Despite the extensive literature on logical systems enabling
(in various ways and for different purposes) some forms of probabilistic
reasoning, there is not much about logics tied to computational aspects,
as $\ICPL$ is.
Most of the recent logical formalisms have been
developed in the realm of modal logic, like e.g. [42, 43, 6, 4, 5, 22, 29, 30].

Another class of probabilistic modal logics have been designed to model Markov chains and similar structures [36, 31, 37].
With the sole exception of Riesz modal logic [23], we are
not aware of sequent calculi for probability logic.

Intuitionistic modal logic has been related in the Curry-Howard sense to monadic extensions of the $\lambda$-calculus [18, 7, 1, 60, 12].
Nevertheless, in these correspondences
modal operators are related to qualitative properties of programs (typically, tracing algebraic effects), as opposed to the quantitative properties expressed by counting quantifiers.
Our Kripke structures for $\ICPL$ can be related to standard Kripke structures for intuitionistic modal logic [46, 49]. These are based on a set $W$ with two pre-order relations $\leq$ and $R$ enjoying a suitable “diamond” property $R; \leq  \ \subseteq\  \leq ; R$. We obtain a similar structure by taking worlds to be pairs $w,\omega$ made of a world and an outcome from the Cantor space,
with $(w,\omega)\preceq (w',\omega)$ whenever $w\leq w'$, and $(w,\omega)R(w,\omega+\omega')$. The clause for $\B C^{q}A$ can then be seen as a quantitative variant of the corresponding clause for $\Diamond A$. This is not very surprising, given the similarity between the introduction and elimination rules for $\B C^{q}$ and those for $\Diamond$, see e.g. [7, 1].

On the other hand, quantitative semantics arising from linear logic have been largely used in the study of probabilistic $\lambda$-calculi,
e.g. [14, 19, 21].
Notably, probabilistic coherence spaces [27, 19, 20] have been shown to provide a fully abstract model of probabilistic PCF.
While we are not aware of correspondences relating probabilistic programs with proofs in linear logic, it seems that the proof-theory of counting quantifiers could be somehow related to that of bounded exponentials [28, 17] and, more generally, to the theory of graded monads and comonads [33, 10, 24, 34].

The calculus $\EVL$ derives from [16], which also introduces a simple type system ensuring strong normalization, although the typings do not provide any quantitative information.
Beyond this, several type systems for probabilistic $\lambda$-calculi have been introduced in the recent literature.
Among these, systems based on type distributions [15], i.e. where a single derivation assigns several types to a term, each with some probability, and systems based on oracle intersection types [9], where type derivations capture single evaluations as determined by an oracle.
Our type systems sit in between these two approaches: like the first (and unlike the second), typing derivations can capture a finite number of different evaluations, although without using distributions of types; like the second, typings reflect the dependency of evaluation on oracles, although the latter are manipulated in a collective way by means of Boolean constraints.

Finally, in
[57] dependent type theory is enriched with a probabilistic choice operator, yielding a calculus with both term and type distributions. Interestingly, a fragment of this system enjoys a sort of CHC with
so-called Markov Logic Networks [48], a class of probabilistic graphical models specified by means of first-order logic formulas.

§ CONCLUSIONS

The main contribution of this work consists in defining a Curry-Howard
correspondence between a logic with counting quantifiers and a
type system that expresses probability of
termination. Moreover, in analogy with what happens in the
deterministic case, extending
the type system with an intersection operator leads to a full characterization of probability of termination.

Even though intersection types do not have a clear logical
counterpart, the existence of this extension convinces us that the
correspondence introduced is meaningful. The possibility of defining a Curry-Howard correspondence
relating algebraic effects, on the program side, with a modal operator, on the logic
side, is certainly not surprising.
Instead, it seems to us that the new and surprising contribution of this work is showing that
the peculiar
features of probabilistic effects can be managed in an elegant way

using ideas coming from logic.

Among the many avenues of research that this work opens, the study of the
problem of type inference must certainly be mentioned, as well as the extension
of the correspondence to polymorphic types or to control operators. Particularly
intriguing, then, is the possibility of studying the system of intersection
types introduced to support the synthesis, always in analogy with what is
already known in deterministic calculations.

[1]
N. Alechina, M. Mendler, V. de Paiva, and E. Ritter.
Categorical and Kripke semantics for constructive S4 modal logic.
In L. Fribourg, editor, Proc. CSL'21, volume 2142, pages
292–307. Springer, 2001.

[2]
M. Antonelli, U. Dal Lago, and P. Pistone.
On Counting Propositional Logic and Wagner's Hierarchy.
In Proc. ICTCS '21, volume 3072, pages 107–121. CEUR
Workshop Proceedings, 2021.

[3]
M. Antonelli, U. Dal Lago, and P. Pistone.
On Measure Quantifiers in First-Order Arithmetic.
In 17th Conference on Computability in Europe Connecting with
Computability, 17th Conference on Computability in Europe, CiE 2021, volume
12813 of Lecture Notes in Computer Science, pages 12–24. Springer,

[4]
F. Bacchus.
Lp, a logic for representing and reasoning with statistical
Comput. Intell., 6(4):209–231, 1990.

[5]
F. Bacchus.
On probability distributions over possible worlds.
Machine Intelligence and Pattern Recognition, 9:217–226, 1990.

[6]
F. Bacchus.
Representing and Reasoning with Probabilistic Knowledge.
MIT Press, 1990.

[7]
N. P. Benton, G. M. Bierman, and V. C. V De Paiva.
Computational types from a logical perspective.
Journal of Functional Programming, 8(2):177–193, 1998.

[8]
Olivier Bournez and Claude Kirchner.
Probabilistic rewrite strategies. applications to elan.
In Sophie Tison, editor, Rewriting Techniques and Applications,
pages 252–266, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.

[9]
F. Breuvart and U. Dal Lago.
On Intersection Types and Probabilistic Lambda Calculi.
In Proc. PPDP '18, New York, NY, USA, 2018. Association for
Computing Machinery.

[10]
A. Brunel, M. Gaboardi, D. Mazza, and S. Zdancewic.
A core quantitative coeffect calculus.
In Proceedings of the 23rd European Symposium on Programming
Languages and Systems - Volume 8410, pages 351–370, Berlin, Heidelberg,
2014. Springer-Verlag.

[11]
L. Caires, F. Pfenning, and B. Toninho.
Linear logic propositions as session types.
Math. Struct. in Comput. Sci., 26(3):367–423, 2016.

[12]
P.-L. Curien, M. Fiore, and G. Munch-Maccagnoni.
A Theory of Effects and Resources: Adjunction Models and Polarised
In Proc. POPL'16, pages 44–56. Association for Computing
Machinery, 2016.

[13]
H. B. Curry and R. Feys.
Combinatory logic. Vol. I.
North-Holland, 1958.

[14]
U. Dal Lago, C. Faggian, B. Valiron, and A. Yoshimizu.
The Geometry of Parallelism: Classical, Probabilistic, and Quantum
In Proc. POPL '17, pages 833–845. Association for Computing
Machinery, 2017.

[15]
U. Dal Lago and C. Grellois.
Probabilistic Termination by Monadic Affine Sized Typing.
ACM TOPLAS, 41(2):10–65, 2019.

[16]
U. Dal Lago, G. Guerrieri, and W. Heijltjes.
Decomposing Probabilistic Lambda-Calculi.
In FoSSaCS '20, pages 136–156. Springer, 2020.

[17]
U. Dal Lago and M. Hofmann.
Bounded linear logic, revisited.
In Pierre-Louis Curien, editor, Typed Lambda Calculi and
Applications, pages 80–94, Berlin, Heidelberg, 2009. Springer Berlin

[18]
R. Davies and F. Pfenning.
A Modal Analysis of Staged Computation.
J. ACM, 48(3):555–604, 2001.

[19]
T. Ehrhard and C. Tasson.
Probabilistic call by push value.
LMCS, 15(1):1–46, 2018.

[20]
T. Ehrhard, C. Tasson, and M. Pagani.
Probabilistic coherence spaces are fully abstract for probabilistic
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, pages 309–320, New York, NY,
USA, 2014. Association for Computing Machinery.

[21]
C. Faggian and S. Ronchi della Rocca.
Lambda-calculus and probabilistic computation.
In Proc. LICS '19, pages 1–13, 2019.

[22]
R. Fagin and J.Y. Halpern.
Reasoning about Knowledge and Probability.
J. ACM, 41(2):340–367, 1994.

[23]
R. Furber, R. Mardare, and M. Mio.
Probabilistic logics based on Riesz spaces.
LMCS, 16, 2020.

[24]
D. R. Ghica and A. I. Smith.
Bounded linear types in a resource semiring.
In Proceedings of the 23rd European Symposium on Programming
Languages and Systems - Volume 8410, pages 331–350, Berlin, Heidelberg,
2014. Springer-Verlag.

[25]
J.-Y. Girard.
Interprétation fonctionnelle et élimination des coupures
de l'arithmetique d'ordre supérieur.
PhD thesis, Université Paris VII, 1972.

[26]
J.-Y. Girard, Y. Lafont, and P. Taylor.
Proofs and Types, volume 7 of Cambridge Tracts in
Theoretical Computer Science.
Cambridge University Press, 1989.

[27]
J.-Y. Girard, P. Ruet, P. Scott, and T. Ehrhard.
Between Logic and Quantic: a Tract, pages 346–381.
London Mathematical Society Lecture Note Series. Cambridge University
Press, Cambridge, 2004.

[28]
Jean-Yves Girard, Andre Scedrov, and Philip J. Scott.
Bounded linear logic: a modular approach to polynomial-time
Theoretical Computer Science, 97(1):1–66, 1992.

[29]
J.Y. Halpern.
An Analysis of First-Order Logics for Probability.
Artif. Intell., 46(3):311–350, 1990.

[30]
J.Y. Halpern.
Reasoning About Uncertainty.
MIT Press, 2003.

[31]
H. Hansson and B. Jonsson.
A logic for reasoning about time and reliability.
Form. Asp. Comput., 6(5):512–535, 1994.

[32]
W.A. Howard.
The formula-as-types notion of construction (1969).
In To H.B. Curry. Essays on Combinatory Logic,
Lambda Calculus and Formalism. Academic Press, 1980.

[33]
S. Katsumata.
Parametric effect monads and semantics of effect systems.
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, pages 633–645, New York, NY,
USA, 2014. Association for Computing Machinery.

[34]
S. Katsumata.
A double category theoretic analysis of graded linear exponential
In Christel Baier and Ugo Dal Lago, editors, Foundations of
Software Science and Computation Structures, pages 110–127, Cham, 2018.
Springer International Publishing.

[35]
Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois.
On the Termination Problem for Probabilistic Higher-Order Recursive
In LICS 2019 - 34th Annual ACM/IEEE Symposium on Logic in
Computer Science, pages 1–14, Vancouver, France, 2019. IEEE.

[36]
D. Kozen.
Semantics of probabilistic programs.
JCSS, 22(3):328 – 350, 1981.

[37]
D. Lehmann and S. Shelah.
Reasoning with time and chance.
Inf. Control., 53(3):165 – 198, 1982.

[38]
P. Martin-Löf.
An intuitionistic theory of types: predicative part.
In Proc. Logic Colloquium '73, volume 80 of Studies in
logic and the foundations of mathematics, pages 73–118. North-Holland,

[39]
H. Michalewski and M. Mio.
Measure quantifiers in monadic second order logic.
LFCS, pages 267–282, 2016.

[40]
M. Mio, M. Skrzypczak, and H. Michalewski.
Monadic Second Order Logic with Measure and Category Quantifiers.
LMCS, 8(2):1–29, 2012.

[41]
C.F. Morgenstern.
The Measure Quantifier.
J. Symb. Log., 44(1):103–108, 1979.

[42]
N. J. Nilsson.
Probabilistic logic.
Artif. Intell., 28(1):71–87, 1986.

[43]
N. J. Nilsson.
Probabilistic logic revisited.
Artif. Intell., 59(1/2):39–42, 1993.

[44]
C.H. Papadimitriou.
Games against nature.
JCSS, 31(2):288–301, 1985.

[45]
M. Parigot.
$\lambda$$\mu$-Calculus: An Algorithmic Interpretation of Classical
Natural Deduction.
In A. Voronkov, editor, Logic Programming and Automated
Reasoning, pages 190–201. Springer Berlin Heidelberg, 1992.

[46]
G. Plotkin and C. Stirling.
A framework for intuitionistic modal logics: Extended abstract.
In Proc. TARK '86, pages 399–406. Morgan Kaufmann Publishers
Inc., 1986.

[47]
M. L. Puterman.
Markov Decision Processes: Discrete Stochastic Dynamic
John Wiley & Sons, Inc., USA, 1st edition, 1994.

[48]
M. Richardson and P. Domingos.
Markov logic networks.
Machine Learning, 62(1):107–136, 2006.

[49]
A.K. Simpson.
The Proof Theory and Semantics of Intuitionistic Modal Logic.
PhD thesis, University of Edinburgh, 1994.

[50]
M.H. Sorensen and P. Urzyczyn.
Lectures on the Curry-Howard isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics.
Elsevier, 2006.

[51]
C.I. Steinhorn.
Borel Structures and Measure and Category Logics, volume 8,
pages 579–596.
Springer-Verlag, 1985.

[52]
P. Wadler.
Propositions as Sessions.
In Proc. ICFP '12, pages 273–286. Association for Computing
Machinery, 2012.

[53]
K.W. Wagner.
Compact descriptions and the counting polynomial-time hierarchy.
In Frege Conference 1984: Proceedings of the International
Conference held at Schwerin, pages 383–392, 1984.

[54]
K.W. Wagner.
Some Observations on the Connection Between Counting and Recursion.
TCS, 47:131–147, 1986.

[55]
K.W. Wagner.
The Complexity of Combinatorial Problems with Succinct Input
Acta Informatica, 23:325–356, 1986.

[56]
D. Wang, D. M. Kahn, and J. Hoffmann.
Raising expectations: Automating expected cost analysis with types.
Proc. ACM Program. Lang., 4(ICFP), aug 2020.

[57]
J. Warrell and M. B. Gerstein.
Dependent type networks: a probabilistic logic via the
Curry-Howard correspondence in a system of probabilistic dependent types.
Uncertainty in Artificial Intelligence, Workshop on Uncertainty in
Deep Learning, 2018.

[58]
S. Zachos.
Probabilistic Quantifiers and Games.
JCSS, 36(3):433–451, 1988.

[59]
S. Zachos and H. Heller.
A decisive characterization of BPP.
Inf. Control., pages 125–135, 69.

[60]
N. Zyuzin and A. Nanevski.
Contextual modal types for algebraic effects and handlers.
Proc. ICFP '21, 5(ICFP):1–29, 2021.

§ DETAILS ABOUT INTUITIONISTIC COUNTING PROPOSITIONAL LOGIC

In this section we introduce a proof-system $\NDCPL$ for $\ICPL$ and describe the correspondence between proofs in $\ICPL$ and families of proofs $\ICPLL$; then, we establish the soundness and completeness of $\NDCPL$ with respect to $\ICPL$-structures.
Finally, we provide some more details about normalization in the “computational fragment” $\ICPLL$, and we describe an alternative “CbN” proof-system for $\ICPLL$, whose derivations can be decorated with terms of $\EVL$, yielding a CHC with the type system $\TCI$.

§.§ The Proof-Theory of $\ICPL$.

The natural deduction system $\NDCPL$  for $\ICPL$ is formed by the rules illustrated in Fig. <ref>, with the following proviso:

* it is everywhere assumed that in a sequent $\Gamma \vdash  A$, $\FN(\Gamma),  \FN(A)
\subseteq X$;

* in the rule ($\B C$I) and ($\B C$E$_{3}$) it is assumed that $ \FN(\bthree)\subseteq \{a\}$.

together with all instances of the two axiom schema below:

\begin{align}
\B C^{q}_{a}(A\lor B) & \to A \lor (\B C^{q}_{a}A) & (a\notin \FN(A)) \tag{$\B C\vee$} \label{ax1}\\
&  \lnot\B C^{q}_{a}\bone & (\FN(\bone)\subseteq\{a\}, \mu(\bone)<q) \tag{$\B C\BOT$}\label{ax2}
\end{align}

As usual, we take $\lnot A$ as an abbreviation for $A\supset \BOT$.

We let $\NDCPL^{-}$ indicate $\NDCPL$ without (<ref>) and (<ref>).

The reason for distinguishing between the systems $\NDCPL$ and $\NDCPL^{-}$ is somehow analogous to what happens in intuitionistic modal logic (IML). Indeed, standard axiomatizations of IML include two axioms

\begin{align}
\Diamond(A\lor B) & \to\Diamond A \lor \Diamond B \tag{$\Diamond\vee$}\\
&\lnot \Diamond\BOT \tag{$\Diamond\BOT$}
\end{align}

which do not have a clear computational interpretation. Instead, a Curry-Howard correspondence can be defined for an axiomatization of IML (usually referred to as constructive modal logic) which does not include these two axioms.

In a similar way, we will show that provability in $\NDCPL^{-}$ corresponds, under the decomposition provided by Lemma <ref> to provability in the Curry-Howard proof-system $\NDCPLL$, while axioms (<ref>) and (<ref>) cannot be similarly interpreted.

Classical Identity

\AXC{}
\RL{(Cid)}
\UIC{$\Gamma\vdash \bvar_{a}^{i}\lor \lnot \bvar_{a}^{i}$}
\DP

Intuitionistic Identity

\AXC{}
\RL{(Iid)}%$\mathsf{FN}(\bone), \mathsf{FN}(A), \mathsf{FN}(\Gamma)\subseteq X$}
\UIC{$\Gamma, A \vdash  A$}
\DP

Logical Rules

\AXC{}
\RL{($\TOP$I)}
\UIC{$\Gamma \vdash   \TOP$}
\DP
\AXC{$\Gamma\vdash  \BOT$}
\RL{($\BOT$E)}
\UIC{$\Gamma \vdash  A$}
\DP

\AXC{$\Gamma \vdash  A$}
\AXC{$\Gamma \vdash  A$}
\RL{($\land$)I}
\BIC{$\Gamma \vdash  A\land B$}
\DP
\AXC{$\Gamma \vdash  A\land B$}
\RL{($\land$E$_{1}$)}
%\AXC{$\bone\vdash \btwo$}
\UIC{$\Gamma \vdash  A$}
\DP
\qquad
\AXC{$\Gamma \vdash A\land B$}
\RL{($\land$E$_{2}$)}
%\AXC{$\bone\vdash \btwo$}
\UIC{$\Gamma \vdash  B$}
\DP

\AXC{$\Gamma \vdash  A$}
\RL{($\lor$I$_{1}$)}
%\AXC{$\bone\vdash \btwo$}
\UIC{$\Gamma \vdash  A\lor B$}
\DP
\qquad
\AXC{$\Gamma \vdash  A$}
\RL{($\lor$I$_{2}$)}
%\AXC{$\bone\vdash \btwo$}
\UIC{$\Gamma \vdash  A\lor B$}
\DP
\AXC{$\Gamma \vdash  A\lor B$}
\AXC{$\Gamma, A \vdash  C$}
\AXC{$\Gamma,B \vdash  C$}
\RL{($\lor$E)}
%\AXC{$\bone\vdash \btwo\land \bthree\land \bfour$}
\TIC{$\Gamma \vdash  C$}
\DP

\AXC{$\Gamma, A \vdash  B$}
\RL{($\to$I)}
\UIC{$\Gamma \vdash  A\to B$}
\DP
$        $
\AXC{$\Gamma \vdash A\to B$}
\AXC{$\Gamma \vdash  A$}
\RL{($\to$E)}
%\AXC{$\bone\vdash \btwo\land \bthree$}
\BIC{$\Gamma \vdash  B$}
\DP

Counting Rules

\AXC{$ \Gamma, \bthree \vdash  A$}
\AXC{$\mu(\bthree)\geq q$}
\RL{($\B C$I) {\small$a\notin \Gamma$}}
\BIC{$\Gamma \vdash\B C^{q}_{a}A$}
\DP
%\qquad \qquad
%\AXC{$\Gamma, A \vdash \bthree$}
%\AXC{$\mu(\bthree)< q$}
%\RL{($\B D$I)  {\small$a\notin \Gamma$}}
%\BIC{$\Gamma \vdash \B D^{q}_{a}A$}

\AXC{$\Gamma \vdash\B C^{q}_{a}A$}
%\RL{$a\notin A$}
%\AXC{$\Gamma, A \vdash C$}
%%\AXC{$\bone\vdash  \btwo\land \bthree$}
\RL{($\B C$E$_{1}$)  {\small$a\notin A$}}
\UIC{$\Gamma \vdash A$}
\DP
\qquad\qquad
\AXC{$\Gamma \vdash\B C^{q}_{a}A$}
\AXC{$\Gamma, A \vdash C$}
%\AXC{$\bone\vdash  \btwo\land \bthree$}
\RL{($\B C$E$_{2}$)  {\small$a\notin \Gamma$}}
\BIC{$\Gamma \vdash \B C^{qs}_{a}C$}
\DP

Rules of $\NDCPL$.

A formula $A$ of $\ICPL$ is purely classical if $A$ contains no intuitionistic propositional variable, and
purely intuitionistic if $A$ contains no classical propositional variable.

Let us list a few properties of $\ICPL$.

For any purely Boolean formula $\bone$, $\vdash \bone$ is derivable in $\NDCPL$ iff $\bone$ is a tautology.

The following are theorems of $\ICPL$:

(i.) $\B C^{q}_{a}\BOT \leftrightarrow \BOT$ and $\B C^{q}_{a}\TOP \leftrightarrow \TOP$;

(ii.) if $a\notin \FN(A)$, $\B C^{q}_{a}(A\to B) \to (A\to \B C^{q}_{a}B)$.

(iii.) if $a\notin \FN(A)$, $\B C^{q}_{a}(A\land B) \leftrightarrow A\land \B C^{q}_{a}B$.

iv. if $a\notin\FN(A)$, then $\B C^{q}_{a}A\leftrightarrow A$.

For any Boolean formula $\bone$ with $\FN(\bone)\subseteq \{a\}$,  $\B C^{q}_{a}\bone \lor (\lnot \B C^{q}_{a}\bone)$ is provable.

Two possibilities arise:
if $\mu(\bone)\geq q$, then from $\bone \vdash \bone$ we deduce, by ($\B C$I), $\vdash\B C^{q}_{a}\bone$ as well as
$\vdash \B C^{q}_{a}\bone \lor (\lnot \B C^{q}_{a}\bone)$.
if $\mu(\bone)> q$, then we deduce, using axiom <ref>,
$\vdash \lnot \B C^{q}_{a} \bone$, as well as
$\vdash \B C^{q}_{a}\bone \lor (\lnot \B C^{q}_{a}\bone)$.

§.§ Relating $\ICPL$ and $\ICPLL$.

Let us first provide a complete proof of the decomposition lemma (Lemma <ref>).

For any formula $C$ and $b\in\{0,1\}$, let $\lnot^{b}C$ indicate the formula $C$ if $b=0$ and $\lnot C$ if $b=1$.
For any $\omega \in (2^{\mathbb N})^{\CC A}$, let the theory of $\omega$ be the following set of Boolean formulas:

$$\TTH(\omega)=\{\lnot^{(1-\omega(a)(i))}\bvar_{a}^{i} \mid a,i\in \mathbb N\}$$

Moreover, for all $K\in \mathbb N$ and finite set $X$, let
$\TTH^{K}_{X}(\omega)$ be the Boolean formula below

\TTH^{K}_{X}(\omega)=\bigwedge_{a\in A,i\leq K}
\lnot^{(1-\omega(a)(i))}\bvar_{a}^{i}
% \left( \bigwedge_{i\leq K,\omega(a)(i)=1}\bvar_{a}^{i}\right) \land \left(\bigwedge_{i\leq K, \omega(a)(i)=0}\lnot \bvar_{a}^{i}\right)

Observe that the formula $\TTH^{K}_{X}(\omega)$ only depends on a finite amount of information of $\omega$, namely, on the unique $v\in (2^{\{1,\dots,K\}})^{X}$ such that $v(a)(i)=\omega(a)(i)$.
When $v$ is clear from the context, we will indicate $\TTH^{K}_{X}(\omega)$ simply as $\TTH(v)$.

The decomposition lemma can be reformulated then as follows:

For any formula $A$ of $\ICPL$ there exist intuitionistic formulas $A_{v}$, where $v$ varies over all possible  valuations of the Boolean variables in $A$,
such that
$\vdash A \leftrightarrow \bigvee_{v}\TTH(v) \land A_{v}$.

The formula $A_{v}$ is defined by induction on $A$ as follows:

* if $A=\TOP$, $A=\BOT$, or $A=\CC p$, then $A_{v}=A$;

* if $A=\bvar_{a}^{i}$, then $A_{v}=\TOP$ if $v(a)(i)=1$, and $A_{v}=\BOT$ if $v(a)(i)=0$;

* if $A=B c C$, where $c=\land, \lor, \to$, then $A_{v}= B_{v} c C_{v}$;

* if $A=\B C^{q}_{a}B $, then we consider two cases:

* if $a$ does not occur in $B$, then we let $A_{v}:=B_{v}$;

* if $a$ does occur in $B$, then for all valuation $w$ of the variables of name $a$ in $B$, we can suppose that the formulas $B_{v+w}$ are well-defined. We let then
A_{v}= \B C^{q}_{a} \bigvee_{w}B_{v+w}

Let us show that for any formula $A$ and valuation $v$ of its Boolean variables,
$\TTH (v)\vdash_{ \ICPL}A\leftrightarrow A_{v}$.
We argue by induction on $A$. Indeed, the only non-trivial case is that of $A=\B C^{q}_{a}B$.
If $a$ does not occur in $B$, then we can conclude by the IH.
Otherwise, by the IH we have that for any valuation $w$ of the Boolean variables of $B$ of name $a$,
$\TTH (v+w)\vdash B\leftrightarrow B_{v+w}$. Using the fact that $\bigvee_{w}\TTH(w)$ is provable and that
$\TTH(v+w)\leftrightarrow (\TTH(v)\land \TTH(w))$, we deduce then
$ \TTH(v) \vdash B\leftrightarrow \bigvee_{w}B_{v+w}$, from which we can deduce
$\TTH(v)\vdash A  \leftrightarrow A_{v}$.

Using $\TTH(v)\vdash A\leftrightarrow A_{v}$ and $\vdash \bigvee_{v}\TTH(v)$, we can conclude
$\vdash A \leftrightarrow \bigvee_{v}\TTH(v)\land A_{v}$.

If $A$ is a formula of $\ICPL$ containing no Boolean variable, we let $|A|$ indicate the corresponding formula of $\ICPLL$ obtained by deleting names from counting quantifiers, i.e. replacing $\B C^{q}_{a}$ by $\B C^{q}$.

In the following, we consider as $\NDCPLL$ the proof-system obtained by enriching the rules from Section <ref> with all standard rules for intuitionistic connectives (straightforwardly adapted to the sequents of $\NDCPLL$ by adding everywhere a fixed Boolean formula $\dots\vdash\bone \Pto \dots$).

In $\NDCPLL$, if $\Gamma \vdash \bone \land \btwo \Pto A$, where $\bone \land \btwo$ is satisfiable, then
$\Gamma \vdash \bone \Pto A$.

By induction on the rules of $\NDCPLL$.

The following result describes the correspondence between the proof-theories of $\ICPL$ and $\ICPLL$.

$\Gamma \vdash_{\NDCPL^{-}} A$ iff for all valuations $v$, $|\Gamma_{v}| \vdash_{\NDCPLL}\TTH(v)\Pto | A_{v}|$.

The if part follows from the decomposition lemma (Lemma <ref>) and from the fact that
$|\Gamma| \vdash_{\NDCPLL} \bone \Pto |A|$ implies $\Gamma, \bone \vdash_{\NDCPL^{-}}A$ (easily checked by induction on the rules of $\NDCPLL$).

For the only-if part we argue by induction on the rules of $\NDCPL$. All propositional cases are straightforward, so we only focus here on the rules for counting quantifiers.

($\B C$I)

\begingroup\makeatletter\def\f@size{10}
\begin{lrbox}{\mypti}% Store prooftree in \mypti
\begin{varwidth}{\linewidth}
\AXC{$|\Gamma_{v}|\vdash\TTH(v)\land \TTH(w)\Pto| A_{v+w}|$}
\doubleLine
\RL{($\vee$I)}
\UIC{$|\Gamma_{v}|\vdash\TTH(v)\land \TTH(w)\Pto\bigvee_{w} |A_{v+w}|$}
\DP$
\end{varwidth}
\end{lrbox}
\AXC{$\Gamma, \bthree \vdash A$}
\AXC{$\mu(\bthree)\geq q$}
\BIC{$\Gamma \vdash  \B C^{q}_{a}A$}
\DP
\qquad\mapsto \qquad
\AXC{$\left\{ \usebox{\mypti}\right\}_{w\vDash \bthree}$}
\doubleLine
\RL{($\mathsf m$)}
\UIC{$|\Gamma_{v}|\vdash\TTH(v)\land \bthree \Pto \bigvee_{w}|A_{v+w}|$}
\AXC{$\mu(\bthree)\geq q$}
\RL{($\B C$I)}
\BIC{$| \Gamma_{v}|\vdash\TTH(v)\Pto |(\B C^{q}_{a}A)_{v}|$}
\DP
\endgroup

($\B C$E)$_{1}$
Since $a\notin \FN(A)$, it follows that $(\B C^{q}_{a}A)_{v}=A_{v}$, so we can conclude by the IH.

($\B C$E)$_{2}$

\begingroup\makeatletter\def\f@size{10}
\begin{lrbox}{\mypti}% Store prooftree in \mypti
\begin{varwidth}{\linewidth}
\AXC{$|\Gamma_{v}| ,|A_{v+w}|\vdash\TTH(v)\land \TTH(w)\Pto |B_{v+w}|$}
\RL{[Lemma \ref{lemma:nothv}]}
\UIC{$|\Gamma_{v}| ,|A_{v+w}|\vdash\TTH(v)\Pto |B_{v+w}|$}
\doubleLine
\RL{($\vee$I)}
\UIC{$|\Gamma_{v} |,|A_{v+w}|\vdash\TTH(v)\Pto (\bigvee_{w}|B_{v+w}|)$}
\DP$
\end{varwidth}
\end{lrbox}
\AXC{$\Gamma \vdash \B C^{q}_{a}$}
\AXC{$\Gamma, A \vdash B$}
\BIC{$\Gamma \vdash \B C^{qs}_{a}B$}
\DP
\qquad \mapsto \qquad
\AXC{$|\Gamma_{v}| \vdash\TTH(v)\Pto |(\B C_{a}^{q}A)_{v}|$}
\AXC{$\left\{ \usebox{\mypti}\right\}_{w}$}
\doubleLine
\RL{($\vee$E)}
\UIC{$|\Gamma_{v} |,\bigvee_{w}|A_{v+w}|\vdash \TTH (v)\Pto (\bigvee_{w}|B_{v+w}|)$}
\RL{($\B C$E)}
\BIC{$|\Gamma_{v} |\vdash
\TTH(v)\Pto
|(\B C^{qs}_{a}B)_{v}|$}
\DP
\endgroup

§.§ Normalization in $\NDCPL^{-}$.

It is possible to define a normalization procedure for $\NDCPL^{-}$. Cuts formed by propositional intro-elim rules are reduced as in standard intuitionistic logic. The cuts formed by counting rules are reduced as follows:

($\B C$I/$\B C$E$_{1}$)

\AXC{$\Pi$}
\noLine
\UIC{$\Gamma,\bthree \vdash A$}
\AXC{$\mu(\bthree)\geq q$}
\RL{$(\B C$I)}
\BIC{$\Gamma \vdash \B C^{q}_{a}A$}
\RL{($\B C$E)$_{1}$}
\UIC{$\Gamma \vdash A$}
\DP
\qquad \leadsto \qquad
\AXC{$\Pi^{*}$}
\noLine
\UIC{$\Gamma \vdash A$}
\DP

where the derivation $\Pi^{*}$ is obtained from Lemma <ref> below, easily established by induction.

If $\Gamma, \bone \vdash A$ is derivable in $\NDCPL^{-}$, where $\FN(\bone)\subseteq \{a\}$, and $a$ does not occur in either $\Gamma$ nor $A$, then $\Gamma \vdash A$ is derivable with a derivation of same length and using the same rules.

($\B C$I/$\B C$E$_{2}$)

\AXC{$\Pi$}
\noLine
\UIC{$\Gamma,\bthree \vdash A$}
\AXC{$\mu(\bthree)\geq q$}
\RL{$(\B C$I)}
\BIC{$\Gamma \vdash \B C^{q}_{a}A$}
\AXC{$\Sigma$}
\noLine
\UIC{$\Gamma, A \vdash B$}
\RL{($\B C$E)$_{2}$}
\BIC{$\Gamma \vdash \B C^{qs}_{a}B$}
\DP
\qquad \leadsto \qquad
\AXC{$\Pi$}
\noLine
\UIC{$\Gamma,\bthree \vdash A$}
\AXC{$\Sigma$}
\noLine
\UIC{$\Gamma, A \vdash B$}
\RL{(subst)}
\BIC{$\Gamma, \bthree \vdash B$}
\AXC{$\mu(\bthree)\geq qs$}
\RL{$(\B C$I)}
\BIC{$\Gamma \vdash \B C^{qs}_{a}B$}
\DP

where the admissibility of the rule (subst) is easily checked by induction.

The proof of
Theorem <ref> yields a way to associate each proof $\Pi$ of $\Gamma \vdash A$ in $\NDCPL^{-}$ with a family of proofs $\Pi_{v}$ of $|\Gamma_{v}|\vdash \TTH(v)\Pto |A_{v}|$ in $\NDCPLL^{-}$.
This association preserves normalization in the following sense:

For any two proofs $\Pi, \Sigma$ of $\Gamma \vdash A$ in $\NDCPL^{-}$ and any valuation $v$ of the Boolean variables in $\Gamma$ and $A$, if $\Pi \leadsto^{*}\Sigma$, then $\Pi_{v}\leadsto^{*}\Sigma_{v}$.

The lemma above, easily checked, can be used to deduce the strong normalization of $\NDCPL^{-}$ from that of $\NDCPLL$:

$\NDCPL^{-}$ is strongly normalizing.

§.§ Soundness and Completeness of $\NDCPL$.

Let us first establish a few properties of Kripke Semantics.
For this we first need to recall a fundamental property of Borel sets.

For any Borel set $S\in \Borel_{X\cup Y}$ and $\omega\in (2^{\mathbb N})^{X}$, let

\Pi^{\omega}(S)=\{\omega'\in (2^{\mathbb N})^{Y}\mid \omega+\omega'\in S\}\subseteq (2^{\mathbb N})^{X}

Notice that $\Pi^{\omega}(S)$ is an analytic set and needs not be Borel. However, since the Lebesgue measure is defined on all analytic sets, the values $\mu(\Pi^{\omega}(S))$, for $S$ Borel (or more generally, analytic), are always defined. Moreover the following holds:

[<cit.>, Theorem 14.11 + Theorem 29.26]
For any $S\in \Borel_{X\cup Y}$, with $X\cap Y=\emptyset$, and $r\in [0,1]$,
\{ \omega\in (2^{\mathbb N})^{X}\mid \mu(\Pi^{f}(S))\geq r\}\in \Borel_{X}

For any $S\subseteq \Borel_{X}$ and $Y\supseteq X$, let $S^{\uparrow Y}:= S\times (2^{\BB N})^{Y-X}$.

Using Lemma <ref> we can show that for any $\ICPL$-structure $\CC M=(W,\preceq, \B i)$ and world $w\in W$, the set of functions $\omega\in (2^{\mathbb N})^{X}$ such that $w,\omega \Vdash^{X}_{\CC M}A$ is a Borel set.

Given a $\ICPL$-structure $\CC M=(W,\preceq,  \B i)$, for any finite set $X$, $w\in W$ and formula $A$ with $\mathrm{FN}(A)\subseteq X$, the set

\mathrm{mod}_{\CC M}(A,X,w)=\{\omega \in (2^{\mathbb N})^{X}\mid w,\omega \Vdash^{X}_{\CC M}  A\}

is Borel.

We argue by induction on $A$:

* if $A=\BOT$, then $\mathrm{mod}_{\CC M}(A,X,w)=\emptyset$ is Borel;
similarly, if $A=\TOP$, then $\mathrm{mod}_{\CC M}(A,X,w)=(2^{\mathbb N})^{X}$ is Borel;

* if $A=\bvar_{a}^{i}$, then $\mathrm{mod}_{\CC M}(A,X,w)$ is the cylinder $\{f\mid f(a)(i)=1\}$, so it is Borel;

* if $A=\CC p$, then $\mathrm{mod}_{\CC M}(A,X,w)$ is either $(2^{\mathbb N})^{X}$ or the empty set, which are both Borel;

* if $A=B\land C$, then $\mathrm{mod}_{\CC M}(A,X,w)=\mathrm{mod}_{\CC M}(B,X,w)\cap \mathrm{mod}_{\CC M}(C,X,w)$, so we conclude by the I.H.;

* if $A=B\lor C$, then $\mathrm{mod}_{\CC M}(A,X,w)=\mathrm{mod}_{\CC M}(B,X,w)\cup \mathrm{mod}_{\CC M}(C,X,w)$, so we conclude by the I.H.;

* if $A=B\to C$, then $\mathrm{mod}_{\CC M}(A,X,w)=
\bigcap_{w'\succeq w} \overline{\mathrm{mod}_{\CC M}(B,X,w')}\cup \mathrm{mod}_{\CC M}(C,X,w')
$ is, by the I.H., a countable intersection of Borel sets, so it is Borel;

* if $A=\B C^{q}_{a}B$, then by the I.H. , for all $w'\in W$,
$\mathrm{mod}_{\CC M}(B, X\cup\{a\}, w')$ is Borel; using Lemma <ref> we then have that the set

$$\mathrm{mod}_{\CC M}(A,X,w)=\bigcap_{w'\succeq w}
\left\{\omega\in (2^{\mathbb N})^{X}\mid
\mu\left( \Pi^{\omega}\left( \mathrm{mod}_{\CC M}(B, X\cup\{a\}, w') \right)\right) \geq q\right\}$$

is Borel.

If $w,\omega \Vdash^{X}_{\CC M}  A$ and $w\preceq w'$, then $w',\omega \Vdash^{X}_{\CC M}  A$.

We argue by induction on $A$.

If $A=\CC p$ the claim follows from the fact that $\B i(\CC p)$ is an upper set;

If $A=\bvar_{a}^{i}$ the claim is immediate.

If $A=B\land C$, the claim follows from the I.H.

If $A=B\to C$ and
$w,\omega \Vdash^{X}_{\CC M}  A$, then for all $w''\succeq w$,
$w'', \omega \Vdash^{X}_{\CC M}  B$ implies $w'',\omega \Vdash^{X}_{\CC M}  C$. Hence, in particular, for all $w''\succeq w'\succeq w$, $w'', \omega \Vdash^{X}_{\CC M}  B$ implies $w'',\omega \Vdash^{X}_{\CC M}  C$, and thus
$w', \omega \Vdash^{X}_{\CC M}  A$.

If $A=\B C^{q}_{a}B$ then by the I.H. for all $\omega'\in 2^{\mathbb N}$, $w,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}B $ implies that for all $w'\succeq w$, $w',\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}B $; we deduce then that for for all $w'\succeq w$,
for all $w''\succeq w'\succeq w$, the set $
\left \{ \omega'\in 2^{\mathbb N}\mid   w'',\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}B \right \}
% \supseteq
%  \left \{ f\in 2^{\mathbb N}\mid   w,\omega+f\Vdash^{X\cup\{a\}}_{\CC M}B \right \}
$ has measure $\geq q$, which implies  $w',\omega\Vdash^{X}_{\CC M}  A$.

Let $\CC M=\langle W,\preceq, \alpha\rangle$ be a $\ICPL$-structure.
For any finite set $X$ and $a\notin X$, for all
$u\in W$ and $\bone\in \Borel_{X}$, and for any formula $A\in\mathrm{Formulae}_{X}$,
if $u,\omega \Vdash^{X}_{\CC M}  A$ holds, then $u, \omega'\Vdash^{X\cup\{a\}}_{\CC M}A$ holds for any $\omega'\in\{\omega\}^{\uparrow_{X\cup\{a\}}}$.

By induction on the rules.

Let $\CC M=\langle W,\preceq, \B i\rangle$ be a $\ICPL$-structure.
For any finite set $X$, $a\notin X$, formula $A\in\mathrm{Formulae}_{X}$, $q\in(0,1]$ and $\omega \in \Borel_{X}$,

w, \omega \Vdash^{X}_{\CC M}   \B C^{q}_{a}A \quad \To \quad
w, \omega \Vdash^{X}_{\CC M}  A

$w', \omega \Vdash^{X}_{\CC M}   \B C^{q}_{a}A $ implies that
$\mu(\{\omega'\in 2^{\mathbb N}\mid u, \omega+\omega' \Vdash^{X\cup\{a\}}_{\CC M} A\}) \geq q>0$. From $u,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}A$ one can deduce by induction on $A$ that $u,\omega\Vdash^{X}_{\CC M}  A$. Since there exists at least one such $f$, we conclude that $u,\omega\Vdash^{X}_{\CC M}  A$ holds.

We are now in a position to establish, by induction on the rules, the soundness of $\NDCPL$.

If $\Gamma \vdash_{\NDCPL} A$, then $\Gamma \vDash A$.

Let $\CC M=\langle W, \preceq, \B i\rangle$ be a $\ICPL$-structure.
We argue by induction on the rules of $\NDCPL$ (selected rules):

* if the last rule is $\AXC{}\UIC{$\Gamma, A\vdash A$}\DP$, then for all $w\in W$ and $\omega \in \Borel_{X}$, if $w, \omega \Vdash^{X}_{\CC M}  \Gamma,A$, then
$w, \omega \Vdash^{X}_{\CC M}  A$.

* if the last rule is

\AXC{$\Gamma, \bthree \vdash^{X\cup\{a\}} A$}
\AXC{$\mu(\bthree)\geq q$}
\BIC{$\Gamma \vdash \B C^{q}_{a}A$}
\DP

then by the I.H. together with Lemma <ref>, for all $w\in W$, for all $\omega\in \Borel_{X}$ and $\omega'\in 2^{\mathbb N}$, if $w,\omega \Vdash^{X}_{\CC M}  \Gamma$ and $w,\omega'\Vdash^{\{a\}} \bthree$ (where the latter condition only depends on $\omega'$), then for all $w'\succeq w$, we have
$w',\omega+\omega' \Vdash^{X\cup\{a\}}_{\CC M}A$.

Since $\mu(\bthree)\geq q$, we deduce that for all $w'\succeq w$,

\left \{ \omega'\mid w',\omega+\omega' \Vdash^{X\cup\{a\}}_{\CC M}A\right \}

has measure greater than $q$, and we conclude then that $w,\omega \Vdash^{X}_{\CC M}  \B C^{q}_{a}A$.

* if the last rule is

\AXC{$\Gamma \vdash \B C^{q}_{a}A$}
\AXC{$\Gamma, A\vdash^{X\cup\{a\}} C$}
\RL{($\B C$E$_{1}$) \ $a\notin \mathrm{FN}(\Gamma,C)$}
\BIC{$\Gamma \vdash  C$}
\DP

let $w\in W$, $\omega\in (2^{\mathbb N})^{X}$ and $w,\omega \Vdash^{X}_{\CC M}  \Gamma$.
By I.H. we deduce that the set

S:=\left \{ \omega'\mid
%\exists w'\sqsupseteq^{X\cup\{a\}}_{X} w \text{ s.t. }
%f\in \B m(w') \text{ and } w',
w, \omega+\omega' \Vdash^{X\cup\{a\}}_{\CC M}A\right \}

has measure greater than $q>0$, and it is thus non-empty.
Let $\omega'$ be an element of $S$; again, by the I.H. we deduce that $w,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}C$;
since $a\notin \FN(C)$, by Lemma <ref>, we conclude then that $w,\omega\Vdash^{X}_{\CC M}  C$.

* if the last rule is

\AXC{$\Gamma \vdash \B C^{q}_{a}A$}
\AXC{$\Gamma, A\vdash^{X\cup\{a\}} C$}
\RL{($\B C$E$_{2}$) \ $a\notin \mathrm{FN}(\Gamma)$}
\BIC{$\Gamma \vdash  \B C^{qs}_{a}C$}
\DP

let $w\in W$, $\omega\in (2^{\mathbb N})^{X}$ and $w,\omega \Vdash^{X}_{\CC M}\Gamma$.
By I.H. we deduce that the set

S:=\left \{ \omega'\mid
%\exists w'\sqsupseteq^{X\cup\{a\}}_{X} w \text{ s.t. }
%f\in \B m(w') \text{ and } w',
w, \omega+\omega' \Vdash^{X\cup\{a\}}_{\CC M}A\right \}

has measure greater than $q\geq qs$ and is contained in the set
S':=\left \{ \omega'\mid
%\exists w'\sqsupseteq^{X\cup\{a\}}_{X} w \text{ s.t. }
%f\in \B m(w') \text{ and } w',
w, \omega+\omega' \Vdash^{X\cup\{a\}}_{\CC M}C\right \}
We can conclude then that $w,\omega\Vdash^{X}_{\CC M}  \B C^{qs}_{a}C$.

* Axiom (<ref>) is valid: suppose $w,\omega \Vdash^{X}_{\CC M}\B C^{q}_{a} (A\lor B)$, where $a\notin \FN(A)$. Then the set $\{\omega'\mid w,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}A\lor B\}$ has measure greater than $q$.
Observe that $w,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}A$ holds iff $w,\omega\Vdash^{X}_{\CC M}A$; so suppose $w,\omega\Vdash^{X}_{\CC M}A$ does not hold; then for any $\omega'$,
$w,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M}A$ does not hold, and thus the set
$\{\omega'\mid w,\omega+\omega'\Vdash^{X\cup\{a\}}_{\CC M} B\}$ must have measure greater than $q$.
We have thus proved that either $w,\omega\Vdash^{X}_{\CC M}A$ holds
or $w, \omega \Vdash^{X}_{\CC M}\B C^{q}_{a}B$ holds, and thus that
$w,\omega \Vdash^{X}A\lor \B C^{q}_{a}B$.

* Axiom (<ref>) is valid:
suppose  $\FN(\bone)\subseteq\{a\}$ and $\mu(\bone)<q$; for any $w\in W$, the set $\{\omega'\mid w,\omega' \vdash^{\{a\}}\bone\}$ coincides with $\model{\bone}$, and has thus measure $<q$ by hypothesis; we deduce that for any $w'\geq w$, $w',*\Vdash^{\emptyset}_{\CC M}\B C^{q}_{a}\bone$ does not hold, and we conclude that $w,*\Vdash^{\emptyset}_{\CC M} \lnot \B C^{q}_{a}\bone$.

To prove the completeness theorem we first need to study provability in $\ICPL$ a bit further.

For any formula $A$ and finite set $X$, $|A|_{X}:=\max\{i\mid \exists a\in X\cap \FN(A) \text{ s.t. }\bvar_{a}^{i} \text{ occurs in }A\}$. We use $|A|$ as a shorthand for $|A|_{\FN(A)}$.
For any $\omega\in (2^{\mathbb N})^{\CC A}$,
$A^{\omega}:=\TTH^{|A|}_{\FN(A)}(\omega) \to A$.

We will exploit the following relativized version of the decomposition lemma (Lemma <ref>), which is proved in a similar way:

Let $A$ be a formula with $\FN(A)\subseteq X\cup Y$, where $X\cap Y=\emptyset$. Then there exist formulas $A^{X}_{w}$, with $\FN(A^{X}_{w})\subseteq X$, where $w$ ranges over the valuations of the variables of name in $Y$ in $A$,

such that
$\vdash A \leftrightarrow ( \bigvee_{w}\TTH(w)\land A^{X}_{w} )$.

For each formula $A$, with $\FN(A)\subseteq \{a\}$, let $\bone_{A}:=\bigvee_{v}\{\TTH(v)\mid A_{v}\not\vdash_{\NDCPL}\BOT\}$.

From $A\vdash \bigvee_{v}\TTH(v) \land A_{v}$ and $A\vdash\lnot \TTH(w)$ for all $\TTH (w)$ not occurring in $\bone_{A}$, we can deduce $A\vdash \bone_{A}$.
The following result shows that measuring the formula $\bone_{A}$ provides a test to know if $\B C^{q}_{a}A$ is consistent:

Let $A$ be a formula with $\FN(A)\subseteq \{a\}$. Then for all $q\in (0,1]$,

\mu (\bone_{A})< q \quad \To \quad \B C^{q}_{a}A \vdash \BOT

The claim follows from the observation that $A\vdash \bone_{A}$ by applying Axiom (<ref>) and the rule ($\B C$E$_{2}$).

Suppose $A$ is a formula with $\FN(A)\subseteq X\cup\{a\}$ (with $a\notin X$). Then for each $\omega \in (2^{\mathbb N})^{\CC A}$, let $A^{X}_{\omega}$ be $A^{X}_{w}$, where $w$ is the restriction of $\omega$ to $(2^{|A|})^{X}$.
Then, by applying the construction from Lemma <ref> to $A^{X}_{\omega}$ we can define a Boolean formula $\bone_{A}^{\omega}$ with $\FN(\bone_{A}^{\omega})\subseteq\{a\}$ such that $\TTH^{|A|}_{X}(\omega)\vdash A\to \bone_{A}^{\omega}$ and such that
$\mu(\bone_{A}^{\omega})< q \To  \TTH^{|A|}_{X}(\omega)\vdash \lnot \B C^{q}_{a}A$.

The proof of the completeness theorem relies on the construction of a suitable “canonical model” based on sets of formulas. Let us first introduce some terminology.
Let $\Gamma$ be a (possibly infinite) set of formulas. We say that $\Gamma$ is

* $A$-consistent if $\Gamma \not \vdash A$;

* consistent if it is $\BOT$-consistent;

* super-consistent if for all $\omega\in (2^{\mathbb N})^{\CC A}$, $\TTH(\omega)\cup \Gamma$ is consistent;

* closed if $A_{1},\dots, A_{n}\in \Gamma$ and $A_{1},\dots, A_{n}\vdash_{\NDCPL}A$ implies $A\in \Gamma$, and if $(\bthree\to A)^{\omega}\in \Gamma$ and $\mu(\bthree)\geq q$ then $(\B C^{q}_{a}A)^{\omega}\in \Gamma$.

Let $\Theta$ be the set of all super-consistent and closed sets of formulas $\Gamma$ satisfying the following conditions, for all $\omega\in (2^{\mathbb N})^{\CC A}$:

\begin{align*}
(A\lor B)^{\omega} \in \Gamma \quad & \To \quad  A^{\omega}\in \Gamma \text{ or }B^{\omega}\in \Gamma
\tag{$\vee$-closure}\\
%$\Big(\TTH^{K}_{X}(\omega)\to (A\lor B) \Big)\in \Gamma \quad \To \quad
%\Big(\TTH^{K}_{X}(\omega)\to A\Big) \in \Gamma \quad \text{or} \quad
%\Big(\TTH^{K}_{X}(\omega) \to B\Big) \in \Gamma$\\
%where $K=\max\{|A|_{a},|B|_{a}\}$.
(\B C^{q}_{a}A)^{\omega}\in \Gamma \quad & \To \quad
\exists\bthree \text{ s.t. }\mu(\bthree)\geq q \text{ and }
(\bthree \to A)^{\omega}\in \Gamma
% \forall f\in \model{\bthree} \ \  A^{\omega+f}\in \Gamma
\tag{$\B C$-closure}
\end{align*}

The fundamental ingredient for the completeness theorem is the lemma below, which will be used to lift any consistent set of formulas to an element of $\Theta$.

Let $\Gamma$ be a super-consistent set and let $\omega_{0}\in (2^{\mathbb N})^{\CC A}$ be such that
$\TTH(\omega_{0})\cup \Gamma$ is $A$-consistent.
Then there exists a set $\Gamma^{*}\supseteq \Gamma$ such that $\Gamma^{*}\in\Theta$ and
$\TTH_{X}(\omega_{0})\cup \Gamma^{*}$ is $A$-consistent.

Let us fix an enumeration $(a_{i})_{i\in \mathbb N}$ of all names.
For any $p,q\in \mathbb N$, Let $\CC F_{p,q}$ be the set of all formulas $B$ such that $\FN(B)\subseteq \{a_{0},\dots, a_{q-1}\}$ and $|B|\leq p$. Let us fix, for all $p,q\in \mathbb N$ an enumeration $(C_{n}^{p,q})_{n\in \mathbb N}$ of $\CC F_{p,q}$.

For any natural number $N$, let $[N]:=\{0,\dots, N-1\}$. Given $p\leq p'$ and $q\leq q'$, and
finite matrices $s \in (2^{[p+1]})^{[q+1]}$
$s'\in (2^{[p'+1]})^{[q'+1]}$, let $s\sqsubseteq s'$ if for all $i\leq p$ and $j\leq q$ $s(j)(i)=s'(j)(i)$.
We will often indicate as $p_{s}$ and $q_{s}$ the (unique) natural numbers such that $s\in (2^{[p+1]})^{[q+1]}$.

Moreover, for all $\omega\in (2^{\mathbb N})^{X}$, let $s\sqsubseteq \omega$ hold if for all $i\leq p_{s}$ and $j\leq q_{s}$, $s(j)(i)=\omega(a_{j})(i)$.

Observe that if $s\sqsubseteq \omega$, $\TTH(\omega)\vdash \TTH(s)$.

For all $p,q$ and $s\in (2^{[p+1]})^{[q+1]}$, we define a set of formulas $\Gamma^{\langle p,q,s\rangle}\subseteq \CC F_{p,q}$ such that for all $p\leq p'$ and $q\leq q'$, $s \in (2^{[p+1]})^{[q+1]}$ and $s' \in (2^{[p'+1]})^{[q'+1]}$,
$s\sqsubseteq s'$ implies $\Gamma^{\langle p,q,s\rangle}\subseteq \Gamma^{\langle p',q',s'\rangle}$.

We let $\Gamma^{\langle p,q,s\rangle}:=\bigcup_{n}\Gamma^{\langle p,q,s\rangle}_{n}$, where the sets
$\Gamma^{\langle p,q,s\rangle}_{n}$ are defined by a triple induction on $p,q$ and $n$ as follows:

* if $p=q=0$ and $b= \omega_{0}(0)$,

* $\Gamma^{\langle 0,0,b\rangle}_{0}:= \Gamma \cup\{\lnot^{(1-b)}\bvar_{0}^{0}\}$;

* $\Gamma^{\langle 0,0,b\rangle}_{n+1}:= \Gamma_{n} \cup \{C^{0,0}_{n}\}$, if this is $A$-consistent, and
$\Gamma^{\langle 0,0,b\rangle}_{n+1}:= \Gamma_{n}^{\langle 0,0,b\rangle} $ otherwise.

If $b\neq \omega_{0}(0)$, the definition is the same, with $\BOT$ in place of $A$;

* if $p>0$ and $q=0$, $\Gamma^{\langle p,0,s\rangle}= \bigcup_{n}\Gamma^{\langle p,0,s\rangle}_{n}$, where if
$s\sqsubseteq \omega_{0}$,

* $\Gamma^{\langle p,0,s\rangle}_{0}:=
\Gamma^{\langle p-1,0, s|_{p-1,0}\rangle}
\cup
\{\lnot^{(1-s(p)(0))}\bvar_{p}^{0}\}$;

* $\Gamma^{\langle p,0,s\rangle}_{n+1}:=
\Gamma^{\langle p,0, s\rangle}_{n}\cup \{C^{p,0}_{n}\}$ if this is $A$-consistent, and
$\Gamma^{\langle p,0,s\rangle}_{n+1}:=
\Gamma^{\langle p,0, s\rangle}_{n}$ otherwise;

and if $s\not\sqsubseteq \omega_{0}$, the definition is similar, with $\BOT$ in place of $A$;

* if $p=0$ and $q>0$, $\Gamma^{\langle 0,q,s\rangle}= \bigcup_{n}\Gamma^{\langle 0,q,s\rangle}_{n}$, where if
$s\sqsubseteq \omega_{0}$,

* $\Gamma^{\langle0,q,s\rangle}_{0}:=
\Gamma^{\langle 0,q-1, s|_{0,q-1}\rangle}
\cup
\{\lnot^{(1-s(0)(q))}\bvar_{0}^{q}\}$;

* $\Gamma^{\langle 0,q,s\rangle}_{n+1}:=
\Gamma^{\langle 0,q, s\rangle}_{n}\cup \{C^{0,q}_{n}\}$ if this is $A$-consistent, and
$\Gamma^{\langle 0,q,s\rangle}_{n+1}:=
\Gamma^{\langle 0,q, s\rangle}_{n}$ otherwise;

and if $s\not\sqsubseteq \omega_{0}$, the definition is similar, with $\BOT$ in place of $A$;

* if both $p>0$ and $q>0$, $\Gamma^{\langle p,q,s\rangle}= \bigcup_{n}\Gamma^{\langle p,q,s\rangle}_{n}$, where if
$s\sqsubseteq \omega_{0}$,

* $\Gamma^{\langle p,q,s\rangle}_{0}:=
\Gamma^{\langle p-1,q, s|_{p-1,q}\rangle}
\cup 	\Gamma^{\langle p,q-1, s|_{p,q-1}\rangle}
\cup
\{\lnot^{(1-s(p)(q))}\bvar_{p}^{q}\}$;

* $\Gamma^{\langle p,q,s\rangle}_{n+1}:=
\Gamma^{\langle p,q, s\rangle}_{n}\cup \{C^{p,q}_{n}\}$ if this is $A$-consistent, and
$\Gamma^{\langle p,q,s\rangle}_{n+1}:=
\Gamma^{\langle p,q, s\rangle}_{n}$ otherwise;

and if $s\not\sqsubseteq \omega_{0}$, the definition is similar, with $\BOT$ in place of $A$.

In the following, whenever this creates no confusion, we will indicate $\Gamma^{\langle p,q,s\rangle}$ simply as $\Gamma^{s}$.

For all finite matrices $s,s'$, the following hold:

a.  $\TTH(s)\subseteq \Gamma^{s}$;

b. if $s\sqsubseteq \omega_{0}$, $\Gamma^{s}$ is $A$-consistent;

c. if $s\not\sqsubseteq \omega_{0}$, $\Gamma^{s}$ is consistent;

d. if $s\sqsubseteq s'$, $\Gamma^{s}\subseteq \Gamma^{s'}$;

e. if $\Gamma^{s}\vdash B$, then for all $t\sqsupseteq s$ such that $B\in \CC F_{p_{t},q_{t}}$, $B\in \Gamma^{t}$.

Facts a.-d. are verified by construction, so we only prove e.: suppose there exist $B_{1},\dots, B_{n}\in \Gamma^{s}$ such that $B_{1},\dots, B_{n}\vdash_{\NDCPL}B$ and let $t\sqsupseteq s$ be such that $B \in \CC F_{p_{t},q_{t}}$. Suppose $B\notin \Gamma^{t}$: then for some $k\in \mathbb N$, $\Gamma^{t}_{k}\cup\{B\}\vdash \BOT$; yet, from d. it follows that $B_{1},\dots,B_{n}\in \Gamma^{t}$, and thus $\Gamma^{t}\vdash \BOT$, contradicting c.

Given matrices $s_{1},\dots, s_{n}\sqsubseteq \omega$, let $\bigvee^{\omega}\{s_{1},\dots, s_{n}\}$ indicate the smallest sub-matrix of $\omega$ extending all $s_{1},\dots, s_{n}$ (i.e. the restriction of $\omega$ to $p=\max\{p_{s_{1}},\dots, p_{s_{n}}\}$ and $q=\max\{q_{s_{1}},\dots, q_{s_{n}}\}$.

For any matrix $s$, let $\Gamma^{\dag s}=\{A^{s}\mid A\in \Gamma^{s}\}=\{\TTH(s)\to A\mid A\in \Gamma^{s}\}$.
Let $\Gamma^{\dag}=\bigcup_{s}\Gamma^{\dag s}$ and let $\Gamma^{*}$ be the deductive closure of $\Gamma^{\dag}$.

We will establish the following properties of $\Gamma^{*}$:

$\alpha.$ $\Gamma^{*}$ is super-consistent;

$\beta.$ $\TTH(\omega_{0})\cup \Gamma^{*}$ is $A$-consistent;

$\gamma.$ $\Gamma\subseteq\Gamma^{*}$;

$\delta.$ if $B^{\omega} \notin \Gamma^{*}$ and $B^{\omega}=B^{s}$, then
$\TTH(s)\cup\Gamma^{*}\cup\{B\}\vdash \BOT$;
moreover, if $B^{\omega_{0}} \notin \Gamma^{*}$ and $B^{\omega_{0}}=B^{s}$, then
$\TTH(s)\cup\Gamma^{*}\cup\{B\}\vdash A$;

$\epsilon.$ $\Gamma^{*}$ is $\vee$-closed;

$\eta.$ $\Gamma^{*}$ is $\B C$-closed.

This will conclude the proof of the theorem.

Let us preliminarily observe that any formula $B^{\omega}$ can be written as $B^{s}$ for a unique $s\sqsubseteq \omega$ such that $p_{s}=|B|$ and $q_{s}$ is minimum with the property that $\FN(B)\subseteq\{a_{0},\dots, a_{q_{s}-1}\}$.

Let us show that $\Gamma^{\dag}$ is super-consistent. This immediately implies that $\Gamma^{*}$ is super-consistent too.
Suppose $\TTH(\omega)\cup\Gamma^{\dag}\vdash \BOT$; then there exist $s_{1},\dots, s_{n}$ and $B_{1}\in \Gamma^{ s_{1}},\dots, B_{n}\in\Gamma^{ s_{n}}$, such that
$\TTH(\omega) , B_{1}^{s_{1}},\dots, B_{n}^{s_{n}}\vdash \BOT$; we can suppose w.l.o.g. that $s_{1},\dots, s_{n}\sqsubseteq \omega$, since if $s_{i}\not\sqsubseteq \omega$, $\TTH(\omega)\vdash \lnot \TTH(s_{i})$, and thus $\TTH(\omega)\vdash B_{i}^{s_{i}} $.

We have then $B_{i}^{s_{i}}= B_{i}^{\omega}$;
by letting $s=\bigvee^{\omega}\{s_{1},\dots, s_{n}\}$ we thus have
$B_{i}^{s_{i}}=B_{i}^{s}$ and
$\TTH(s),  B_{1}^{s},\dots, B_{n}^{s}\vdash \BOT$,
which implies $\TTH(s),  B_{1},\dots, B_{n}\vdash \BOT$,
and since $\TTH(s)\cup\{ B_{1},\dots, B_{n}\}\subseteq \Gamma^{ s}$, we deduce
$\BOT \in \Gamma^{  s}$, contradicting a.

$\beta.$ The argument is similar to the one for $\alpha$.

Let $B\in \Gamma$ and $s$ be such that $B^{\omega}=B^{s}$, $p_{s}=|B|$ and $\FN(B)\subseteq \{a_{0},\dots, a_{q_{s}-1}\}$.
For any $s'\in (2^{[p_{s}+1]})^{[q_{s}+1]}$, $B^{s'}\in \Gamma^{\dag s'}\subseteq \Gamma^{\dag}$. Hence, using the fact that
$\vdash \bigvee_{s\in (2^{[p_{s}+1]})^{[q_{s}+1]}}\TTH(s)$, we deduce that
$\{ B^{s}\mid s\in (2^{[p_{s}+1]})^{[q_{s}+1]}\} \vdash B$, and thus that $\Gamma^{\dag}\vdash B$, which implies $B\in \Gamma^{*}$.

Let $s$ be such that $B^{\omega}=B^{s}$. We consider the case of $\omega=\omega_{0}$; the case $\omega \neq \omega_{0}$ is proved similarly with $\BOT $ in place of $A$.
We will prove the contrapositive, i.e. that if $\TTH(s)\cup \Gamma^{\dag}\cup \{B\}$ is $A$-consistent, then $B^{\omega_{0}}=B^{s}\in \Gamma^{*}$, from which $\delta$. follows. Suppose that $\TTH(\omega)\cup \Gamma^{\dag}\cup \{B\}$ is $A$-consistent. Suppose $B\notin \Gamma^{s}$: this implies $B\notin \Gamma$ and that for some $k\in \mathbb N$, $\Gamma^{s}_{k}\cup\{B\}\vdash A$. But this forces then $\Gamma^{s}\cup\{B\}\vdash A$;
since for all $F\in \Gamma^{s}$, $F^{s}\in \Gamma^{\dag}$, and $\TTH(s), F^{s} \vdash F$, we deduce then
$\TTH(s)\cup \Gamma^{\dag}\cup \{B\}\vdash A$, which is absurd. We conclude then that $B\in \Gamma^{s}$, and thus $B^{s}=B^{\omega}\in \Gamma^{\dag}\subseteq \Gamma^{*}$.

Again, we consider the case of $\omega=\omega_{0}$; the case $\omega \neq \omega_{0}$ is proved similarly with $\BOT $ in place of $A$.
Let $s\sqsubseteq \omega_{0}$ be such that  $(B\lor C)^{\omega}=(B \lor C)^{s}$ and suppose $(B\lor C)^{s}\in \Gamma^{*}$ but neither $B^{s}\in \Gamma^{*}$ nor $C^{s}\in \Gamma^{*}$; then by $\delta.$, $\TTH(s)\cup \Gamma^{*}\cup\{B\}\vdash A$ and $\TTH(s)\cup \Gamma^{*}\cup\{C\}\vdash A$, hence
$\TTH(s)\cup \Gamma^{*}\cup\{B\lor C\}\vdash A$;
since $(B\lor C)^{s}\in \Gamma^{*}$ we have $\TTH(s)\cup \Gamma^{*}\vdash B\lor C$, so we deduce
$\TTH(s)\cup \Gamma^{*}\vdash A$, and since $\TTH(s)\subseteq \TTH(\omega_{0})$, we have
$\TTH(\omega_{0})\cup \Gamma^{*}\vdash A$, contradicting $\beta$.

Once more, we consider the case of $\omega=\omega_{0}$; the case $\omega \neq \omega_{0}$ is proved similarly with $\BOT $ in place of $A$.

Let $s\sqsubseteq \omega_{0}$ be such that $(\B C^{q}_{a}B)^{\omega_{0}}= (\B C^{q}_{a}B)^{s}$ and suppose $(\B C^{q}_{a}B)^{s}\in \Gamma^{*}$.

We can suppose w.l.o.g. that $a=a_{q}$ with $q> q_{s}$.
Hence we can suppose that the formula $B^{\omega_{0}}$ is of the form $B^{s+s'+s''}$, for some finite matrices $s',s''$, with $s''\in 2^{[|B|+1]}$.

By Lemma <ref> and Remark <ref> we have that $\Gamma^{s}\vdash B\leftrightarrow( \bigvee_{v\in 2^{[|B|+1]} }\TTH(v)\land B_{s+v})$, where $B_{s+v}$ has no free name.
Let $S=\{ v\in 2^{[|B|+1]}\mid B_{s+v}\in \Gamma^{s} \}$ and $\bthree= \bigvee_{v\in S}\TTH(v)$.
Observe that for any $v\in S$, $\Gamma^{s+s'}\vdash \TTH(v)\to B$.
Let $v\in S$ and $\omega_{v}$ be such that $v\subseteq \omega_{v}$. Then

$\Gamma^{s+s'}\vdash \TTH(\omega_{v})\to B$.
Using e. we have then that for all $t\in 2^{[|B|+1]}$,
$\TTH(\omega_{v})\to B\in \Gamma^{s+s'+t}$, so in particular,
$\TTH(\omega_{v})\to B\in \Gamma^{s+s'+s''}$, so
$(\TTH(\omega_{v})\to B)^{\omega_{0}}\in \Gamma^{\dag}\subseteq \Gamma^{*}$.

We thus have that for all $v\in S$, $\Gamma^{*}\vdash (\TTH(v)\to B)^{\omega_{0}}$, which implies
$\Gamma^{*}\vdash (\bthree\to B)^{\omega_{0}}$ and thus $(\bthree\to B)^{\omega_{0}}\in \Gamma^{*}$.

At this point, if $\mu(\bthree)\geq q$ we are done.
Otherwise, suppose $\mu(\bthree)<q$; if $v\notin S$, then $B_{s+v}\notin \Gamma^{s}$, which implies that for some $k$,
$\Gamma^{s}_{k}\cup\{B_{s+v}\}\vdash A$; this implies that $\Gamma^{s}\vdash (\TTH(v)\land B_{s+v}) \to A$; we deduce then that $\Gamma^{s}\vdash B\to ((\bigvee_{v\in S}\TTH(v)\land B_{s+v})\lor A)$, and in particular that $\Gamma^{s}\vdash B\to(\bthree\lor A)$;
this means that there exist formulas $B_{1},\dots, B_{n}\in \Gamma^{s}\subseteq \CC F_{p_{s},q_{s}}$, hence containing no occurrences of the name $a$, such that $B_{1},\dots, B_{n} \vdash B\to  (\bthree\lor A)$;
from this we deduce first $\TTH(s), B_{1}^{s},\dots, B_{n}^{s}\vdash B\to (\bthree\lor A)$, and then, using ($\B C$E$_{2}$), $\TTH(s),\B C^{q}_{a}B, B^{s}_{1},\dots, B^{s}_{n}\vdash \B C^{q}_{a}(\bthree\lor A)$. Now, since $s\subseteq\omega_{0}$, $\B C^{q}_{a}A, B_{1}^{s},\dots, B_{n}^{s}\in \Gamma^{*}$ and
$  \B C^{q}_{a}(\bthree\lor A)\vdash  (\B C^{q}_{a}\bthree)\lor A$ (Axiom (<ref>), since we can suppose w.l.o.g. that $a\notin \FN(A)$), we have
$\TTH(\omega_{0})\cup\Gamma^{*}\vdash (\B C^{q}_{a}\bthree)\lor A$; moreover, from $\mu(\bthree)< q$ we get (by Axiom (<ref>))
$\vdash \lnot \B C^{q}_{a}\bthree$ and thus $(\B C^{q}_{a}\bthree)\lor A\vdash A$, so we can conclude
$\TTH(\omega_{0})\cup\Gamma^{*}\vdash A$, which contradicts $\beta$.

Let $\Gamma$ be an $A$-consistent set of formulas. Then there exists a super-consistent set $\Delta$ and $\omega\in (2^{\mathbb N})^{\CC A}$ such that ${\TTH(\omega)\cup \Delta}$ is $A$-consistent and its closure contains $\Gamma$.

Let us define sets of formulae $\Gamma_{a,i}$ together with $\omega(\langle a,i\rangle)$ as follows:

* let $\omega(\langle 0,0\rangle)=1$ if $\Gamma\cup\{\bvar_{0}^{0}\}$ is $A$-consistent, and $\omega(\langle 0,0\rangle)=0$ otherwise;
moreover, let
$\Gamma_{0,0}= \Gamma$;

* let $\omega(\langle a, i+1\rangle)=1$ if  $\Gamma_{a,i}\cup\{\bvar_{a}^{i+1}\}$ is $A$-consistent, and $\omega(\langle a,i+1\rangle)=0$ otherwise;
moreover, let
$\Gamma_{a,i+1}=\Gamma_{a,i}\cup\{\lnot^{(1-\omega(\langle a,i+1\rangle))}\bvar_{a}^{i+1}\}$;

* let $\omega(\langle a+1, 0\rangle)=1$ if  $\bigcup_{i}\Gamma_{a,i}\cup\{\bvar_{a+1}^{0}\}$ is $A$-consistent, and $\omega(\langle a,i+1\rangle)=0$ otherwise;
moreover, let
$\Gamma_{a+1,0}=\bigcup_{i}\Gamma_{a,i}\cup\{(\lnot^{1-\omega(\langle a+1,0\rangle))}\bvar_{a+1}^{0}\}$.

By construction we then have that $\TTH(\omega)\cup \Gamma=\bigcup_{a,i} \Gamma_{a,i}$;
let us show that
$\bigcup_{a,i} \Gamma_{a,i}$ is $A$-consistent:

* $\Gamma_{0,0}=\Gamma$ is $A$-consistent by hypothesis;

* suppose $\Gamma_{a,i}$ is $A$-consistent; if $\Gamma_{a,i+1}= \Gamma_{a,i}\cup\{\bvar_{a}^{i+1}\}$ then by construction $\Gamma_{a,i+1} $ is $A$-consistent;
if $\Gamma_{a,i+1}= \Gamma_{a,i}\cup\{\lnot\bvar_{a}^{i+1}\}$ then by construction $\Gamma_{a,i} \cup\{\bvar_{a}^{i}\} \vdash A$; if moreover
$\Gamma_{a,i} \cup\{\lnot\bvar_{a}^{i}\} \vdash A$, the
$\Gamma_{a,i}\cup\{\bvar_{a}^{i}\lor\lnot \bvar_{a}^{i}\}\vdash A$ and thus
$\Gamma_{a,i}\vdash A$, which is absurd.
We conclude then that $\Gamma_{a,i+1}$ is $A$-consistent.

* suppose $\Gamma_{a,i}$ is $A$-consistent for all $i\in \mathbb N$; first observe that $\Gamma_{a}:=\bigcup_{i}\Gamma_{a,i}$ is $A$-consistent: if $\Gamma_{a}\vdash A$, then there exist $B_{1}\in \Gamma_{a,i_{1}},\dots, B_{n}\in \Gamma_{a,i_{n}}$ such that $B_{1},\dots, B_{n}\vdash  A$;  since for $j\leq k$,  $\Gamma_{a,j}\subseteq \Gamma_{a,k}$, we deduce that $\Gamma_{a,\max\{i_{1},\dots, i_{n}\}}\vdash A$, which is absurd.

Now, if $\Gamma_{a+1,0}=\Gamma_{a}\cup\{\bvar_{a+1}^{0}\}$ then by construction $\Gamma_{a+1,0}$ is $A$-consistent; if  $\Gamma_{a+1,0}=\Gamma_{a}\cup\{\lnot\bvar_{a+1}^{0}\}$ then
$\Gamma_{a}\cup\{\bvar_{a+1}^{0}\}\vdash A$; hence, if $\Gamma_{a+1,0}\vdash A$, we deduce
$\Gamma_{a}\cup\{\bvar_{a+1}^{0}\lor \lnot \bvar_{a+1}^{0}\} \vdash A$, so we conclude
$\Gamma_{a}\vdash A$, which is absurd.

Now, for each formula $B\in \Gamma$ let us define a formula $B^{*}$ as follows:

B^{*} := B \lor \left ( \bigvee_{a\in \FN(B), i\leq |B|} \lnot^{\omega(\langle a,i\rangle)}\bvar_{a}^{i}   \right)

Observe that $\TTH(\omega)\cup\{B^{*}\}\vdash B$ and that for all $\omega'\in(2^{\mathbb N})^{\CC A}$,
$\TTH(\omega')\cup\{B^{*}\}$ is consistent.

Let then $\Delta=\{B^{*}\mid B\in \Gamma\}$. It is clear that $\TTH(\omega)\cup \Delta \vdash B$ for all $B\in \Gamma$.
Suppose $\TTH(\omega)\cup \Delta\vdash A$, then there exists Boolean formulas $
\bfour_{1},\dots, \bfour_{k}\in \TTH(\omega)$ and formulas $B_{1},\dots, B_{n}\in \Gamma$ such that
$\bfour_{1},\dots, \bfour_{k}, B_{1}^{*},\dots, B_{n}^{*}\vdash A$. Since $B_{i}\vdash B^{*}$, this implies then
$\bfour_{1},\dots, \bfour_{k}, B_{1},\dots, B_{n}\vdash A$, and thus $\TTH(\omega)\cup \Gamma$ is not $A$-consistent, which is absurd.

We now have all elements to proceed to the proof of the completeness theorem.

If $\Gamma \vDash A$, then $\Gamma \vdash _{\NDCPL}A$.

Let $\CC T= \langle \Theta  , \subseteq, \B i\rangle$, where
$\B i( \CC p)=\{\Gamma\mid \CC p\in  \Gamma \}$.

We will prove that for all $\Gamma \in \Theta$ and $\omega\in \Borel_{X}$,
\Gamma, \omega \vdash_{\CC T}^{X} A$ iff $A^{\omega}\in \Gamma
From this claim the theorem is proved as follows: suppose $\Gamma \not\vdash  A$; by Lemma <ref> we obtain a super-consistent set $\Delta$ and $\omega_{0}\in (2^{\mathbb N})^{\CC A}$ such that $\TTH(\omega_{0})\cup \Delta$ is $A$-consistent and its closure contains $\Gamma$.
By Lemma <ref> $\Delta$ extends to $\Gamma^{*}\in \Theta$ such that $\Gamma^{*}\supseteq \Gamma$ and $\TTH(\omega_{0})\cup\Gamma^{*}$ is $A$-consistent.

Then using the claim, from $\Gamma \subseteq \Gamma^{*}$, we deduce that $\Gamma^{*},\omega_{0} \vdash_{\CC T}^{X}\Gamma$, and from $A\notin \Gamma^{*}$ we deduce that
$\Gamma^{*},\omega_{0}\not\vdash_{\CC T}^{X}A$; we can conclude then that $\Gamma \not\vdash_{\CC T}^{X} A$, and thus that $\Gamma \not\vDash A$.

Let us now prove the claim, by arguing by induction on $A$:

* if $A=\BOT$, from the vacuous assumption $\Gamma, \omega \vdash_{\CC T}^{X}\BOT$ we can freely deduce $\BOT^{\omega}\in \Gamma$; conversely,
from the vacuous assumption
$\BOT^{\omega}\in \Gamma$ we can freely deduce
$\Gamma, \omega \vdash_{\CC T}^{X}\BOT$;

* if $A=\TOP$, since $\Gamma, \omega \vdash_{\CC T}^{X}\TOP$ always holds and $\TOP^{\omega}\in \Gamma$ always holds (since $\Gamma$ is closed), we can conclude;

* if $A=\CC p$, $\Gamma, \omega \vdash_{\CC T}^{X}\CC p$ iff $\CC p\in  \Gamma$ holds by definition (since $\CC p\notin \TTH(\omega)$);