# Continuous Learning in a Single-Incremental-Task Scenario with Spike
Features

Ruthvik Vaila<EMAIL_ADDRESS>,  John Chiasson
<EMAIL_ADDRESS>Boise State University 1910 W University
DrBoiseIdahoUSA83706 and  Vishal Saxena<EMAIL_ADDRESS>University of
Delaware140 Evans HallNewarkDEUSA19716

(2020)

###### Abstract.

Deep Neural Networks (DNNs) have two key deficiencies, their dependence on
high precision computing and their inability to perform sequential learning,
that is, when a DNN is trained on a first task and the same DNN is trained on
the next task it forgets the first task. This phenomenon of forgetting
previous tasks is also referred to as catastrophic forgetting. On the other
hand a mammalian brain outperforms DNNs in terms of energy efficiency and the
ability to learn sequentially without catastrophically forgetting. Here, we
use bio-inspired Spike Timing Dependent Plasticity (STDP) in the feature
extraction layers of the network with instantaneous neurons to extract
meaningful features. In the classification sections of the network we use a
modified synaptic intelligence that we refer to as cost per synapse metric as
a regularizer to immunize the network against catastrophic forgetting in a
Single-Incremental-Task scenario (SIT). In this study, we use MNIST
handwritten digits dataset that was divided into five sub-tasks.

neural networks, feature extraction, STDP, catastrophic forgetting, single-
incremental-task, fisher information

††copyright: acmcopyright††journalyear: 2020††conference: International
Conference on Neuromorphic Systems; July 28–30, 2020; Virtual
Conference††booktitle: International Conference on Neuromorphic Systems (ICONS
’20), July 28–30, 2020, Virtual Conference††price: –.00††doi: –.–/——.—-††isbn:
——/–/–††ccs: Computing methodologies††ccs: Computing methodologies Machine
learning††ccs: Computing methodologies Machine learning approaches††ccs:
Computing methodologies Bio-inspired approaches

##  1\. Introduction

Typically, Spiking Neural Networks (SNNs) are trained using an unsupervised
algorithm called Spike Timing Dependant Plasticity (STDP) (Kheradpisheh et
al., 2018). Spike features extracted from latency encoded convolutional
variants of SNNs have been used with an SVM (Kheradpisheh et al., 2018) and a
linear neural network classifier (Vaila et al., 2019) to achieve
classification accuracies in excess of $98.5\%$. However, SNNs tend to achieve
lower classification accuracies when compared to Artificial Neural Networks
(ANNs) (Panda et al., 2019). ANNs are trained using Stochastic Gradient
Descent (SGD). The main assumption of SGD is that the mini-batches of the
training data contain approximately equal number of data points with the same
labels (i.e., the data is uniformly randomly distributed). This assumption
does not hold for many of the machine learning systems that learn online
continuously. Different kinds of continuous learning schemes have been
proposed to mitigate the problem of catastrophic forgetting. Two main
scenarios of continuous learning are the Multi-Task (MT) and the Single-
Incremental-Task (SIT) scenarios (Maltoni and Lomonaco, 2019). In the MT
scenario a neural network with a disjoint set of output neurons is used to
train/test a corresponding set of disjoint tasks. In contrast, a neural
network for the SIT scenario expands the number of neurons in the output layer
to accommodate new classification tasks. The MT scenario is useful when
training different classification tasks on the same network thereby allowing
resource sharing. The SIT scenario is useful for online continuous learning
applications. That is, the SIT scenario is more suitable for online machine
learning systems and is more difficult compared to the MT scenario. This is
because the MT network has to not only mitigate catastrophic forgetting, but
also learn to differentiate classes that are usually not seen together (unless
the system has some kind of short term memory to be replayed later). Self-
Organizing Maps (SOM) with short-term memory were used in (Gepperth and
Karaoguz, 2016) (Parisi et al., 2019) to achieve an accuracy of $85\%$ on the
MNIST dataset using a SIT scenario and replaying the complete dataset. Using
STDP based unsupervised learning and dopaminergic plasticity modulation
controlled forgetting was proposed in (Allred and Roy, 2020). It was shown to
achieve a $~{}95\%$ accuracy on MNIST dataset using the SIT scenario.
Unsupervised spiking networks with predictive coding have been trained with
STDP and shown to achieve an accuracy of $~{}76\%$ on the MNIST dataset using
the MT scenario (Ororbia, 2019). In our work here, our network classifies the
data according to the AR1 method given in (Maltoni and Lomonaco, 2019). This
uses the SIT scenario which was inspired by synaptic intelligence for the MT
scenario in (Zenke et al., 2017). In our previous work (Vaila et al., 2019) we
used the MNIST dataset split into two disjoint tasks to show that features
extracted from a spiking convolutional network (SCN) demonstrated more
immunity to catastrophic forgetting compared to their ANN counterparts. In
(Vaila et al., 2019), using early stopping, the first five output neurons were
trained to classify the digits $\\{0,1,2,3,4\\}$ and then the remaining five
output neurons were trained to classify the digits $\\{5,6,7,8,9\\}$. The
network was then tested on the complete test dataset (digits 0-9) and achieved
a $93\%$ accuracy on this test data. In the work presented here we exclusively
work with spike features extracted from an SCN and study the effect of
continuous learning using the SIT scenario on the MNIST dataset. For this
study the MNIST dataset was split into the five disjoint classification tasks
$\\{\\{0,1\\},\\{2,3\\},\\{4,5\\},\\{6,7\\},\\{8,9\\}\\}$. The feature
classification is done unsupervised in the convolution layer (L2) while the
classification is done in the latter layers using error backpropagation. Here
we modify the synaptic intelligence regularizer calculation of (Zenke et al.,
2017) in order to reduce the computational load.

##  2\. Network

Figure 1. Layers L1-L3 and L3-L5 are feature extraction and feature
classification layers respectively. The output layers expands from $2-10$
output neurons to accommodate the five classification tasks.

The feature extraction part of the network is same as in (Vaila et al., 2019)
(Vaila et al., 2019). Input images are encoded into spikes using ON and OFF
center DoG filters followed by thresholding (Kheradpisheh et al., 2018). The
L2 (convolution) layer consists of 30 maps and the neurons that emerge as
winners after lateral inhibition and STDP competition (Vaila et al., 2020) get
to update their weights according to a simplified STDP (Kheradpisheh et al.,
2018).

(1) ${\small\begin{split}&\text{ \ }\Delta
w_{i}=\begin{cases}-a^{-}w_{i}(1-w_{i}),\ \ \text{if}\ \ t_{out}-t_{in}<0\\\
+a^{+}w_{i}(1-w_{i}),\ \ \text{if}\ \ t_{out}-t_{in}\geq 0\end{cases}\\\
&w_{i}\leftarrow w_{i}+\Delta w_{i}\end{split}}$

$t_{in}$ and $t_{out}$ are the spike times of the pre-synaptic (input) and the
post-synaptic (output) neuron, respectively. If the $i^{th}$ input neuron
spikes before the output neuron spikes, the weight $w_{i}$ is increased;
otherwise the weight is decreased.111The input neuron is assumed to have
spiked _after_ the output neuron spiked. Learning refers to the change $\Delta
w_{i}$ in the (synaptic) weights with $a^{+}$ and $a^{-}$ denoting the
learning rate constants. These rate constants are initialized with low values
$(0.004,0.003)$ and are typically increased for every 1500 input images as
learning progresses (Kheradpisheh et al., 2018). This STDP rule is considered
simplified because the amount of weight change doesn’t depend on the time
duration between pre-synaptic and post-synaptic spikes. In this work,
backpropagation is used only in the classification layers (L3-L4-L5) of the
network with a single hidden layer L4.

##  3\. Continuous Learning

By continuous learning we mean that the network in Figure 1 will start with
two output neurons in L5 and be trained to classify the digits $\\{0,1\\}$.
During this training the error is backpropagated from layer L5 only as far as
L3. After this training is complete two new neurons will be appended to the L5
layer and then trained to classify the digits $\\{2,3\\}$. This is continued
in the same manner for the three remaining classes
$\\{\\{4,5\\},\\{6,7\\},\\{8,9\\}\\}$. We proceed in the rest of this section
to give the details of this training by specifying the cost function along
with the (cost per synapse) weight regularizer. The neural network in this
work has a softmax output layer which is the likelihood of the input image
belonging to a particular class. Let $\textbf{X}\in R^{3630}$ denote the
(flattened) spike features in L3 and ${\theta}\in R^{1500\times 3630}$ denote
the weights from L3 to the hidden layer L4. For task 1 there are two output
neurons and we let $C_{1}$ denote the cross-entropy cost computed with the
softmax outputs of these two neurons. For task 2 there are now four output
neurons and we let $C_{2}$ denote the cross-entropy cost computed with the
softmax outputs of these four neurons. The costs $C_{3},C_{4},C_{5}$ are
defined in a similar manner. The L4 and the L5 weights are updated using SGD
on mini-batches. $C^{(m)}_{1}$ denotes the cost of the $m^{th}$ input mini-
batch for the task $\\{0,1\\}$. $C^{(m)}_{2},...,C^{(m)}_{5}$ are similarly
defined. During training for task 1 the weights ${\theta}\in R^{1500\times
3630}$ are updated as usual according to

(2) $\Delta\theta=-\eta\frac{\partial C_{1}^{(m)}}{\partial\theta}.$

After training is completed for task 1, we need to know the importance of each
of the weights ${\theta}_{rs}$ for $r=1,...,1500$ and $s=1,....,3630$ in terms
of classifying the images of task 1. This is necessary because when we proceed
to train on task 2 these ”important” weights should not be allowed to change
significantly. That is the network must be forced to use the other weights for
the training of task 2. Accordingly, we next define a _cost per synapse_
regularizer during the training of task 2 to help prevent changes to the so
called important weights of the task 1. The change in the cost per each
synapse $\Delta C_{1,{rs}}^{(m)}$ is defined as

(3) $\Delta C_{1,{rs}}^{(m)}\triangleq\frac{\partial
C_{1}^{(m)}}{\partial\theta_{rs}}\Delta\theta_{rs}=-\eta\left(\frac{\partial
C_{1}^{(m)}}{\partial\theta_{rs}}\right)^{2}$

with

(4) $\Delta C_{1}^{(m)}\triangleq\left\\{\Delta
C_{1,rs}^{(m)}\right\\}_{\begin{subarray}{c}r=1,...,1500\\\
s=1,...,3630\end{subarray}}\in\mathbb{R}^{1500\times 3630}$

For each task there are $M$ mini-batches with $P$ images per mini-batch for a
total of $N=MP$ input images for each task. The average change in cost for
$\theta_{rs}$ is given by

(5) $\small{f_{1,{rs}}\triangleq\frac{1}{M}{\sum_{m=1}^{M}\Delta
C_{1,{rs}}^{(m)}}=-\eta\frac{1}{M}{\sum_{m=1}^{M}{\left(\frac{\partial
C_{1}^{(m)}}{\partial\theta_{rs}}\right)}^{2}}}$

with

(6)
$f_{1}\triangleq\left\\{f_{1,rs}\right\\}_{\begin{subarray}{c}r=1,...,1500\\\
s=1,...,3630\end{subarray}}\in\mathbb{R}^{1500\times 3630}$

A softmax output layer with a cross-entropy cost function and one-hot encoded
labels is the same as the log-likelihood cost function (Nielsen, 2015). The
MNIST label $l$ with $l\in\\{0,1,2,...,9\\}$ corresponds to the $k^{th}(=l+1)$
output neuron with $k\in\\{1,2,...,10\\}$, respectively. Let
$\mathbf{X}^{(m)}=\\{(X^{(im)},l_{i}),i=1,...,P\\}$ denote the images and
corresponding labels in the $m^{th}$ mini-batch. In Equation (5) the average
cost $C_{1}^{(m)}$ for mini-batch $m$ is

(7)
${\small\begin{split}C_{1}^{(m)}=\frac{1}{P}\sum_{i=1}^{P}C_{1}(\textbf{X}^{(im)})=-\frac{1}{P}\sum_{i=1}^{P}\sum_{k=1}^{n_{o}=2}y_{k}\ln
a_{k}^{L5}(\textbf{X}^{(im)})\\\
=-\frac{1}{P}\sum_{(\textbf{X}^{(im)},l_{i})\in\textbf{X}^{m}}\ln
a_{l_{i}+1}^{L5}(\textbf{X}^{(im)})\end{split}}$

as $y_{l+1}=1$ and $y_{k}=0$ for $k\neq l+1$. Here L5 indicates the last layer
and $a^{L5}(\textbf{X})$ indicates softmax output activations. Substituting
Equation (7) in to Equation (5), Equation (6) becomes

(8) $f_{1}=-\eta\frac{1}{M}{\sum_{m=1}^{M}{\left({\frac{\partial
C_{1}^{(m)}}{\partial\theta}}\right)}^{2}}\in\mathbb{R}^{1500\times 3630}$

In (Kirkpatrick et al., 2017) the authors state that near a minimum of the
cost the $(r,s)$ component of Equation (8) given by
$-\dfrac{1}{M}\sum\limits_{m=1}^{M}\left(\dfrac{\partial
C_{1}^{(m)}}{\partial\theta_{rs}}\right)^{2}$is the same as

(9)
$I_{rs}(\theta)\triangleq\dfrac{1}{M}\sum\limits_{m=1}^{M}\dfrac{\partial^{2}C_{1}^{(m)}}{\partial\theta_{rs}^{2}},$

with some limitations (Kunstner et al., 2019) and is the Fisher information
(Chiasson, 2013) for the parameter $\theta_{rs}.$ $I_{rs}(\theta)$ is a
measure of the “importance” of the weight $\theta_{rs}.$ A large value of
$I_{rs}(\theta)$ implies that small changes in the value of $\theta_{rs}$ will
lead to a large increase in average cost (classification error). When the
network is to train for task 2, those weights $\theta_{rs}$ with a large
$I_{rs}(\theta)$ computed from task 1 must now be constrained to only small
changes so the network will continue to classify the images of task 1
correctly. That is, when training on task 2, the network must be forced to
(essentially) use only those weights that had a small value of
$I_{rs}(\theta)$ from task 1. So, the cost per synapse for the first task
$f_{1}$ (calculated during the last epoch of training for the first task)
gives the relative importance of the weights for the task1 classification
problem.

Let $\Delta{\theta_{1}}\in\mathbb{R}^{1500\times 3630}$ be the change in
weights during the last epoch of task 1. Further $\hat{\theta}_{1}$ denotes
the value of the weights after training on task 1. The second task is trained
using the regularized cost function given by

(10) $C_{2}^{reg}\triangleq
C_{2}+\frac{\lambda}{2N}({\theta}_{2}-{\hat{\theta}}_{1})\odot
F_{1}\odot({\theta}_{2}-{\hat{\theta}}_{1})$

with

(11) $F_{1}\triangleq
f_{1}\oslash(\Delta{\theta_{1}}\odot\Delta{\theta_{1}}+\xi)$

where $\odot$ and $\oslash$ represent the Hadamard product and division,
respectively. $\xi$ is a small positive number added to each element of the
matrix to prevent division by zero when doing Hadamard division. Similarly,
$f_{t}$ is calculated during the last epoch of training task $t$,
${\Delta\theta}_{t}$ denotes the change in the weights during the last epoch,
and finally $\hat{\theta}_{t}$ denotes the weights at the end of training task
$t$. Task $t$ is trained by adding a weight regularizing term to prevent the
”important” weights from the previous tasks being changed significantly. With
$f_{0}\in\mathbb{R}^{1500\times 3630}$ a matrix of zeros define

(12)
$F_{t}\triangleq\sum_{\tau=0}^{t-1}f_{\tau}\oslash(\Delta{\theta_{\tau}}\odot\Delta{\theta_{\tau}}+\xi).$

then we can write the cost function of the $t^{th}$ as

(13) $C_{t}^{reg}=C_{t}+\frac{\lambda}{2N}\odot
F_{t}\odot({\theta}_{t}-{\hat{\theta}}_{t-1})\odot({\theta}_{t}-{\hat{\theta}}_{t-1}),\hskip
11.38109pt\hskip 5.69054pt\text{t=1,2,3,4,5}$

$\hat{\theta}_{t-1}$ are the weights between L3 and L4 layers at the end of
$(t-1)^{th}$ task and $N=MP$ is the number of input images. Remark Note that
only the weights connecting L3 to L4 are subject to cost per synapse
regularization. The weights connecting L4 to L5 are trained without
regularization and use the AR1 method to train sequentially (Maltoni and
Lomonaco, 2019). The parameter updates for the cost function are

(14) $\small{\frac{\partial C_{t}^{reg}}{\partial{\theta_{t}}}=\frac{\partial
C_{t}}{\partial{\theta_{t}}}+\frac{\lambda}{N}F_{t}\odot({\theta_{t}}-{\hat{\theta}}_{t-1})}$

In (Zenke et al., 2017) the cost per synapse is calculated over all the

Figure 2. Search for $\lambda$.

training epochs (rather than just the last epoch). The parameter $\lambda$ in
Equation (14) was optimized with validation data. Figure 2 shows the effect of
$\lambda$ on accuracy. Results for each $\lambda$ were obtained from $10$
different weight initializations.

###  3.1. Results with Disjoint Tasks

In this section the network was not presented with any

Figure 3. Test accuracy

of the data from the previous tasks. Figure 3 shows the trend of testing
accuracy as the network is trained on disjoint tasks with 10 different weight
initializations. The highest testing accuracy achieved for this disjointly
trained tasks was $84.61\%$. $\lambda$ was set to $2.03\times 10^{7}$. in
Figure 3 ’Max’ in the legend indicates the weight initialization that resulted
in highest test accuracy and ’Min’ indicates the weight initialization that
resulted in lowest test accuracy.

###  3.2. Results by Replaying

Here the data for the new task was expanded with $10\%$ of

Figure 4. Test accuracy.

data from all the previously trained tasks. The accuracy trend as the learning
progresses is shown in the Figure 4 for 10 different weight initializations
with $\lambda$ same as the disjoint case. The highest accuracy achieved by
replaying $10\%$ of the data from the previous tasks was $88.41\%$. For all of
the above reported experiments the hyper-parameter $\eta=1.0\times 10^{-3}$,
the mini-batch size $P=10$ and the number of mini-batches per task $M=1000$.

##  4\. Conclusion

We achieved a final accuracy of $88.4\%$ in sequential training of MNIST
dataset. While we do not claim state-of-the-art classification accuracy we
proposed a hybrid method that combines bio-inspired feature extraction and the
cost per synapse metric that is scalable to more challenging datasets. This is
a work in progress and we are currently working towards extending this work to
a more challenging EMNIST dataset (Cohen et al., 2017) by using surrogate
gradients (Vaila et al., 2020) that can potentially eliminate floating point
matrix-vector multiplications when implemented in a custom hardware.

## References

  * (1)
  * Allred and Roy (2020) Jason M. Allred and Kaushik Roy. 2020.  Controlled Forgetting: Targeted Stimulation and Dopaminergic Plasticity Modulation for Unsupervised Lifelong Learning in Spiking Neural Networks.  _Frontiers in Neuroscience_ 14 (2020), 7.  https://doi.org/10.3389/fnins.2020.00007
  * Chiasson (2013) John Nelson. Chiasson. 2013\.  _Introduction to probability theory and stochastic processes_.  Wiley.
  * Cohen et al. (2017) Gregory Cohen, Saeed Afshar, Jonathan Tapson, and André van Schaik. 2017.  EMNIST: an extension of MNIST to handwritten letters.  _arXiv e-prints_ , Article arXiv:1702.05373 (Feb. 2017), arXiv:1702.05373 pages.  arXiv:cs.CV/1702.05373
  * Gepperth and Karaoguz (2016) Alexander Gepperth and Cem Karaoguz. 2016.  A Bio-Inspired Incremental Learning Architecture for Applied Perceptual Problems.  _Cognitive Computation_ 8, 5 (01 Oct 2016), 924–934.  https://doi.org/10.1007/s12559-016-9389-5
  * Kheradpisheh et al. (2018) Saeed Reza Kheradpisheh, Mohammad Ganjtabesh, Simon J. Thorpe, and Timothée Masquelier. 2018\.  STDP-based spiking deep convolutional neural networks for object recognition.  _Neural Networks_ 99 (2018), 56 – 67.  https://doi.org/10.1016/j.neunet.2017.12.005
  * Kirkpatrick et al. (2017) James Kirkpatrick, Razvan Pascanu, Neil Rabinowitz, Joel Veness, Guillaume Desjardins, Andrei A. Rusu, Kieran Milan, John Quan, Tiago Ramalho, Agnieszka Grabska-Barwinska, Demis Hassabis, Claudia Clopath, Dharshan Kumaran, and Raia Hadsell. 2017.  Overcoming catastrophic forgetting in neural networks.  _Proceedings of the National Academy of Sciences_ 114, 13 (2017), 3521–3526.  https://doi.org/10.1073/pnas.1611835114 arXiv:https://www.pnas.org/content/114/13/3521.full.pdf
  * Kunstner et al. (2019) Frederik Kunstner, Lukas Balles, and Philipp Hennig. 2019\.  Limitations of the Empirical Fisher Approximation for Natural Gradient Descent.  arXiv:cs.LG/1905.12558
  * Maltoni and Lomonaco (2019) Davide Maltoni and Vincenzo Lomonaco. 2019.  Continuous learning in single-incremental-task scenarios.  _Neural Networks_ 116 (2019), 56 – 73.  https://doi.org/10.1016/j.neunet.2019.03.010
  * Nielsen (2015) Michael A Nielsen. 2015\.  _Neural Networks and Deep Learning_.  Determination Press.  http://neuralnetworksanddeeplearning.com/
  * Ororbia (2019) Alexander Ororbia. 2019\.  Spiking Neural Predictive Coding for Continual Learning from Data Streams.  arXiv:cs.NE/1908.08655
  * Panda et al. (2019) Priyadarshini Panda, Aparna Aketi, and Kaushik Roy. 2019\.  Towards Scalable, Efficient and Accurate Deep Spiking Neural Networks with Backward Residual Connections, Stochastic Softmax and Hybridization.  arXiv:cs.CV/1910.13931
  * Parisi et al. (2019) German I. Parisi, Ronald Kemker, Jose L. Part, Christopher Kanan, and Stefan Wermter. 2019.  Continual lifelong learning with neural networks: A review.  _Neural Networks_ 113 (2019), 54 – 71.  https://doi.org/10.1016/j.neunet.2019.01.012
  * Vaila et al. (2019) Ruthvik Vaila, John Chiasson, and Vishal Saxena. 2019\.  Deep Convolutional Spiking Neural Networks for Image Classification.  _arXiv e-prints_ , Article arXiv:1903.12272 (Mar 2019), arXiv:1903.12272 pages.  arXiv:cs.NE/1903.12272
  * Vaila et al. (2019) Ruthvik Vaila, John Chiasson, and Vishal Saxena. 2019\.  Feature Extraction Using Spiking Convolutional Neural Networks. In _Proceedings of the International Conference on Neuromorphic Systems_ _(ICONS ’19)_. Association for Computing Machinery, New York, NY, USA, Article Article 14, 8 pages.  https://doi.org/10.1145/3354265.3354279
  * Vaila et al. (2020) Ruthvik Vaila, John Chiasson, and Vishal Saxena. 2020\.  A Deep Unsupervised Feature Learning Spiking Neural Network with Binarized Classification Layers for EMNIST Classification.  arXiv:cs.NE/2002.11843
  * Zenke et al. (2017) Friedemann Zenke, Ben Poole, and Surya Ganguli. 2017\.  Continual Learning Through Synaptic Intelligence. In _Proceedings of the 34th International Conference on Machine Learning_ _(Proceedings of Machine Learning Research)_ , Doina Precup and Yee Whye Teh (Eds.), Vol. 70. PMLR, International Convention Centre, Sydney, Australia, 3987–3995.  http://proceedings.mlr.press/v70/zenke17a.html


# On Measure Quantifiers in First-Order Arithmetic††thanks: Supported by ERC
CoG “DIAPASoN”, GA 818616.
(Long Version)

Melissa Antonelli  Ugo Dal Lago  Paolo Pistone

###### Abstract

We study the logic obtained by endowing the language of first-order arithmetic
with second-order measure quantifiers. This new kind of quantification allows
us to express that the argument formula is true _in a certain portion_ of all
possible interpretations of the quantified variable. We show that first-order
arithmetic with measure quantifiers is capable of formalizing simple results
from probability theory and, most importantly, of representing every recursive
random function. Moreover, we introduce a realizability interpretation of this
logic in which programs have access to an oracle from the Cantor space.

##  1 Introduction

The interactions between first-order arithmetic and the theory of computation
are plentiful and deep. On the one side, proof systems for arithmetic can be
used to prove termination of certain classes of algorithms [61], or to
establish complexity bounds [8]. On the other, higher-order programming
languages, such as typed $\lambda$-calculi, can be proved to capture the
computational content of arithmetical proofs. These insights can be pushed
further, giving rise to logical and type theories of various strengths.
Remarkably, all the quoted research directions rely on the tight connection
between the concepts of _totality_ (of functions) and _termination_ (of
algorithms).

However, there is one side of the theory of computation which was only
marginally touched by this fruitful interaction, that is, randomized
computation. Probabilistic models have been widely investigated and are
nowadays pervasive in many areas of computer science. The idea of relaxing the
notion of algorithm to account for computations involving random decisions
appeared early in the history of modern computability theory and studies on
probabilistic computation have been developed since the 1950s and 1960s [9,
40, 14, 51, 52, 57]. Today several formal models are available, such as
probabilistic automata [55, 49], both Markovian and oracle probabilistic
Turing machines (from now on, PTMs) [14, 53, 21, 22], and probabilistic
$\lambda$-calculi [50, 31]. At this point randomized computation is
ubiquitous.

In probabilistic computation, behavioral properties, such as termination, have
a _quantitative_ nature: any computation terminates _with a given
probability_. Can such quantitative properties be studied within a logical
system? Of course, logical systems for set-theory and second-order logic can
be expressive enough to represent measure theory [58] and, thus, are
inherently capable of talking about randomized computations. Yet, what should
one add to _first-order_ arithmetic to make it capable of describing
probabilistic computation?

In this paper we provide an answer to this question by introducing a somehow
_minimal_ extension of first-order Peano Arithmetic by means of measure
quantifiers. We will call this system $\mathsf{MQPA}$. Its language is
obtained by enriching the language of $\mathsf{PA}$ with a special unary
predicate, $\mathsf{FLIP}(\cdot)$, whose interpretation is an element of the
Cantor space, $\\{0,1\\}^{\mathbb{N}}$, and with measure-quantified formulas,
such as $\mathbf{C}^{\frac{1}{2}}F$, which expresses the fact that $F$ has
probability $\geq\frac{1}{2}$ of being true (that is, the subset of
$\\{0,1\\}^{\mathbb{N}}$ which makes $A$ true has measure $\geq\frac{1}{2}$).
The appeal to the Cantor space is essential here, since there is no _a priori_
bound on the amount of random bits a given computation might need; at the same
time, we show that it yields a very natural measure-theoretic semantics.

The rest of this paper is structured as follows. In Section 2 we introduce the
syntax and semantics of $\mathsf{MQPA}$. Section 3 shows that some non-trivial
results in probability theory can be naturally expressed in $\mathsf{MQPA}$.
In Section 4 we establish our main result, that is, a representation theorem
within $\mathsf{MQPA}$ for random functions computed by PTMs, which is the
probabilistic analogous to Gödel’s arithmetization theorem for recursive
functions in $\mathsf{PA}$ [23]. Finally, in Section 5, a realizability
interpretation for $\mathsf{MQPA}$ in terms of computable functions with
oracles on the Cantor space is presented.

##  2 Measure-Quantified Peano Arithmetic

This section is devoted to the introduction of the syntax and semantics for
formulas of $\mathsf{MQPA}$. Before the actual presentation, we need some
(very modest) preliminaries from measure theory.

### Preliminaries.

The standard model $(\mathbb{N},+,\times)$ has nothing probabilistic in
itself. Nevertheless, it can be naturally extended into a probability space:
arithmetic being discrete, one may consider the underlying sample space as
just $\mathbb{B}^{\mathbb{N}}$, namely the set of all infinite sequences of
elements from $\mathbb{B}$ = $\\{0,1\\}$. We will use metavariables, such as
$\omega_{1},\omega_{2},\dots$, for the elements of $\mathbb{B}^{\mathbb{N}}$.
As it is known, there are standard ways of building a well behaved
$\sigma$-algebra and a probability space on $\mathbb{B}^{\mathbb{N}}$, which
we will briefly recall here. The subsets of $\mathbb{B}^{\mathbb{N}}$ of the
form

$\mathsf{C}_{X}=\\{s\cdot\omega\ |\ s\in X\ \&\
\omega\in\mathbb{B}^{\mathbb{N}}\\},$

where $X\subseteq\mathbb{B}^{n}$ and $\cdot$ denotes sequence concatenation,
are called _$n$ -cylinders_ [7]. Specifically, we are interested in $X$s
defined as follows: $X_{n}^{b}=\\{s\cdot b\ |\ s\in\mathbb{B}^{n}\ \&\
b\in\mathbb{B}\\}\subseteq\mathbb{B}^{n+1}$, with $n\in\mathbb{N}$. We will
often deal with cylinders of the form $\mathsf{C}_{X^{1}_{n}}$. We let
$\mathscr{C}_{n}$ and $\mathscr{C}$ indicate the set of all $n$-cylinders and
the corresponding algebra, made of the open sets of the natural topology on
$\mathbb{B}^{\mathbb{N}}$. The smallest $\sigma$-algebra including
$\mathscr{C}$, which is Borel, is indicated as $\sigma(\mathscr{C})$. There is
a natural way of defining a probability measure $\mu_{\mathscr{C}}$ on
$\mathscr{C}$, namely by assigning to $\mathsf{C}_{X}$ the measure
$\frac{|X|}{2^{n}}$. There exists canonical ways to extend this to
$\sigma(\mathscr{C})$. In doing so, the standard model ($\mathbb{N},+,\times$)
can be generalized to $\mathscr{P}$ =
$(\mathbb{N},+,\times,\sigma(\mathscr{C}),\mu_{\mathscr{C}})$, which will be
our standard model for $\mathsf{MQPA}$.111Here, we will focus on this
structure as a “standard model” of $\mathsf{MQPA}$, leaving the study of
alternative models for future work. When interpreting sequences in
$\mathbb{B}^{\mathbb{N}}$ as infinite supplies of random bits, the set of
sequences such that the $k$-th coin flip’s result is $1$ (for any fixed $k$)
is assigned measure $\frac{1}{2}$, meaning that each random bit is uniformly
distributed and independent from the others.

### Syntax.

We now introduce the syntax of $\mathsf{MQPA}$. Terms are defined as in
classic first-order arithmetic. Instead, the formulas of $\mathsf{MQPA}$ are
obtained by endowing the language of $\mathsf{PA}$ with _flipcoin formulas_ ,
such as $\mathsf{FLIP}(t)$, and _measure-quantified formulas_ , as for example
$\mathbf{C}^{t/s}F$ and $\mathbf{D}^{t/s}F$. Specifically,
$\mathsf{FLIP}(\cdot)$ is a special unary predicate with an intuitive
computational meaning. It basically provides an infinite supply of
independently and randomly distributed bits. Intuitively, given a closed term
$t$, $\mathsf{FLIP}(t)$ holds if and only if the $n$-th tossing returns 1,
where $n$ is the denotation of $t+1$.

######  Definition 1 (Terms and Formulas of $\mathsf{MQPA}$)

Let $\mathcal{G}$ be a denumerable set of _ground variables_ , whose elements
are indicated by metavariables such as $x,y.$ The _terms of $\mathsf{MQPA}$_,
denoted by $t,s$, are defined as follows:

$t,s:=x\mid\mathtt{0}\mid\mathtt{S}(t)\mid t+s\mid t\times s.$

The _formulas of $\mathsf{MQPA}$_ are defined by the following grammar:

$F,G:=\mathsf{FLIP}(t)\mid(t=s)\mid\neg F\mid F\vee G\mid F\wedge G\
\mid\exists x.F\mid\forall x.F\mid\mathbf{C}^{t/s}F\mid\mathbf{D}^{t/s}F.$

### Semantics.

Given an environment $\xi:\mathcal{G}\to\mathbb{N}$, the interpretation
$\llbracket t\rrbracket_{\xi}$ of a term $t$ is defined as usual.

######  Definition 2 (Semantics for Terms of $\mathsf{MQPA}$)

An _environment_ $\xi$ is a mapping that assigns to each ground variable a
natural number, $\xi:\mathcal{G}\rightarrow\mathbb{N}$. Given a term $t$ and
an environment $\xi$, the _interpretation of $t$ in $\xi$_ is the natural
number $\llbracket t\rrbracket_{\xi}\in\mathbb{N}$, inductively defined as
follows:

$\displaystyle\llbracket x\rrbracket_{\xi}$
$\displaystyle:=\xi(x)\in\mathbb{N}$
$\displaystyle\llbracket\mathtt{0}\rrbracket_{\xi}$ $\displaystyle:=0$
$\displaystyle\llbracket\mathtt{S}(t)\rrbracket_{\xi}$
$\displaystyle:=\llbracket t\rrbracket_{\xi}+1$

$\displaystyle\llbracket t+s\rrbracket_{\xi}$ $\displaystyle:=\llbracket
t\rrbracket_{\xi}+\llbracket s\rrbracket_{\xi}$ $\displaystyle\llbracket
t\times s\rrbracket_{\xi}$ $\displaystyle:=\llbracket
t\rrbracket_{\xi}\times\llbracket s\rrbracket_{\xi}$

Instead, the interpretation of formulas requires a little care, being it
inherently _quantitative_ : any formula $F$ is associated with a _measurable_
set, $\llbracket F\rrbracket_{\xi}\in\sigma(\mathscr{C})$ (similarly to e.g.
[44]).

######  Definition 3 (Semantics for Formulas of $\mathsf{MQPA}$)

Given a formula $F$ and an environment $\xi$, the _interpretation of $F$ in
$\xi$_ is the measurable set of sequences $\llbracket
F\rrbracket_{\xi}\in\sigma(\mathscr{C})$ inductively defined as follows:

$\displaystyle\llbracket\mathsf{FLIP}(t)\rrbracket_{\xi}$
$\displaystyle:=\mathsf{C}_{X^{1}_{\llbracket t\rrbracket_{\xi}}}$
$\displaystyle\llbracket t=s\rrbracket_{\xi}$
$\displaystyle:=\begin{cases}\mathbb{B}^{\mathbb{N}}\ \ &\text{ if }\llbracket
t\rrbracket_{\xi}=\llbracket s\rrbracket_{\xi}\\\ \emptyset\ \ &\text{
otherwise}\end{cases}$ $\displaystyle\llbracket\neg G\rrbracket_{\xi}$
$\displaystyle:=\mathbb{B}^{\mathbb{N}}\ –\ \llbracket G\rrbracket_{\xi}$

$\displaystyle\llbracket G\vee H\rrbracket_{\xi}$ $\displaystyle:=\llbracket
G\rrbracket_{\xi}\cup\llbracket H\rrbracket_{\xi}$ $\displaystyle\llbracket
G\wedge H\rrbracket_{\xi}$ $\displaystyle:=\llbracket
G\rrbracket_{\xi}\cap\llbracket H\rrbracket_{\xi}$
$\displaystyle\llbracket\exists x.G\rrbracket_{\xi}$
$\displaystyle:=\bigcup_{i\in\mathbb{N}}\llbracket
G\rrbracket_{\xi\\{x\leftarrow i\\}}$ $\displaystyle\llbracket\forall
x.G\rrbracket_{\xi}$ $\displaystyle:=\bigcap_{i\in\mathbb{N}}\llbracket
G\rrbracket_{\xi\\{x\leftarrow i\\}}$

$\displaystyle\llbracket\mathbf{C}^{t/s}G\rrbracket_{\xi}$
$\displaystyle:=\begin{cases}\mathbb{B}^{\mathbb{N}}\ \ &\text{ if }\llbracket
s\rrbracket_{\xi}>0\text{ and }\mu_{\mathscr{C}}(\llbracket
G\rrbracket_{\xi})\geq\llbracket t\rrbracket_{\xi}/{\llbracket
s\rrbracket_{\xi}}\\\ \emptyset\ \ &\text{ otherwise}\end{cases}$
$\displaystyle\llbracket\mathbf{D}^{t/s}G\rrbracket_{\xi}$
$\displaystyle:=\begin{cases}\mathbb{B}^{\mathbb{N}}\ \ &\text{ if }\llbracket
s\rrbracket_{\xi}=0\text{ or }\mu_{\mathscr{C}}({\llbracket
G\rrbracket_{\xi}})<\llbracket t\rrbracket_{\xi}/{\llbracket
s\rrbracket_{\xi}}\\\ \emptyset\ \ &\text{ otherwise}\end{cases}$

The semantics is well-defined since the sets
$\llbracket\mathsf{FLIP}(t)\rrbracket_{\xi}$ and $\llbracket
t=s\rrbracket_{\xi}$ are measurable, and measurability is preserved by all the
logical operators. It is not difficult to see that any $n$-cylinder can be
captured as the interpretation of some $\mathsf{MQPA}$ formula. However, the
language of $\mathsf{MQPA}$ allows us to express more and more complex
measurable sets, as illustrated in the next sections.

The notions of validity and logical equivalence are defined in a standard way.

###### Definition 4

A formula of $\mathsf{MQPA}$, $F$, is _valid_ if and only if for every $\xi$,
$\llbracket F\rrbracket_{\xi}=\mathbb{B}^{\mathbb{N}}$. Two $\mathsf{MQPA}$
formulas $F,G$ are _logically equivalent_ $F\equiv G$ if and only if for every
$\xi$, $\llbracket F\rrbracket_{\xi}=\llbracket G\rrbracket_{\xi}$.

Notably, the two measure quantifiers are inter-definable, since one has
$\llbracket\mathbf{C}^{t/s}F\rrbracket_{\xi}=\llbracket\neg\mathbf{D}^{t/s}F\rrbracket_{\xi}$.

###### Lemma 1

For every formula of $\mathsf{MQPA}$, call it $F$:

$\mathbf{C}^{t/s}F\equiv\neg\mathbf{D}^{t/s}F.$

  * Proof.

The proof is based on Definition 3,

$\displaystyle\llbracket\neg\mathbf{D}^{t/s}F\rrbracket_{\xi}$
$\displaystyle=\mathbb{B}^{\mathbb{N}}\
-\llbracket\mathbf{D}^{t/s}F\rrbracket_{\xi}$
$\displaystyle=\mathbb{B}^{\mathbb{N}}-\begin{cases}\mathbb{B}^{\mathbb{N}}\ \
\ &\text{ if }\mu_{\mathscr{C}}(\llbracket F\rrbracket_{\xi})<\llbracket
t\rrbracket_{\xi}/\llbracket s\rrbracket_{\xi}\\\ \emptyset\ \ \ &\text{
otherwise}\end{cases}$ $\displaystyle=\begin{cases}\emptyset\ \ \ &\text{ if
}\mu_{\mathscr{C}}(\llbracket F\rrbracket_{\xi})<\llbracket
t\rrbracket_{\xi}/\llbracket s\rrbracket_{\xi}\\\ \mathbb{B}^{\mathbb{N}}\ \ \
&\text{ otherwise}\end{cases}$
$\displaystyle=\llbracket\mathbf{C}^{t/s}F\rrbracket_{\xi}.$

$\Box$

The following examples illustrate the use of measure-quantifiers
$\mathbf{C}^{t/s}$ and $\mathbf{D}^{t/s}$ and, in particular, the role of
probabilities of the form $\frac{t}{s}$.

###### Example 1

The formula $F=\mathbf{C}^{1/1}\exists x.\mathsf{FLIP}(x)$ states that a true
random bit will almost surely be met. It is valid, as the set of constantly 0
sequences forms a singleton, which has measure 0.

###### Example 2

The formula222For the sake of readability, $F$ has been written with a little
abuse of notation the actual $\mathsf{MQPA}$ formula being $\forall
x.\mathbf{C}^{1/z}(\mathrm{EXP}(z,x)\land\forall{y}.(\exists
w.(y+w=x)\to\mathsf{FLIP}(y))$, where $\mathrm{EXP}(z,x)$ is an arithmetical
formula expressing $z=2^{x}$ and $\exists w.y+w=x$ expresses $y\leq x$.
$F=\forall x.\mathbf{C}^{1/2^{x}}\forall_{y\leq x}.\mathsf{FLIP}(y)$ states
that the probability for the first $x$ random bits to be true is at least
$\frac{1}{2^{x}}$. This formula is valid too.

##  3 On the Expressive Power of $\mathsf{MQPA}$

As anticipated, the language of $\mathsf{MQPA}$ allows us to express some
elementary results from probability theory, and to check their validity in the
structure $\mathscr{P}$. In this section we sketch a couple of examples.

### The Infinite Monkey Theorem.

Our first example is the so-called _infinite monkey theorem_ ($\mathtt{IMT}$).
It is a classic result from probability theory stating that a monkey randomly
typing on a keyboard has probability 1 of ending up writing the _Macbeth_ (or
any other fixed string), sooner or later. Let the formulas $F(x,y)$ and
$G(x,y)$ of $\mathsf{PA}$ express, respectively, that “$y$ is strictly smaller
than the length of (the binary sequence coded by) $x$”, and that “the $y$+1-th
bit of $x$ is 1”. We can formalize $\mathtt{IMT}$ through the following
formula:

$F_{\mathtt{IMT}}:\forall x.\mathbf{C}^{1/1}\forall y.\exists z.\forall
w.F(x,w)\rightarrow(G(x,w)\leftrightarrow\mathsf{FLIP}(y+z+w)).$

Indeed, let $x$ be a binary encoding of the _Macbeth_. The formula
$F_{\mathtt{IMT}}$ says then that for all choice of start time $y$, there
exists a time $y+z$ after which $\mathsf{FLIP}(\cdot)$ will evolve exactly
like $x$ with probability 1.

How can we justify $F_{\mathtt{IMT}}$ using the semantics of $\mathsf{MQPA}$?
Let $\varphi(x,y,z,w)$ indicate the formula
$F(x,w)\rightarrow(G(x,w)\leftrightarrow\mathsf{FLIP}(y+z+w))$. We must show
that for all natural number $n\in\mathbb{N}$, there exists a measurable set
$S^{n}\subseteq\mathbb{B}^{\mathbb{N}}$ of measure 1 such that any sequence in
$S^{n}$ satisfies the formula $\forall y.\exists z.\forall
w.\varphi(n,y,z,w)$. To prove this fact, we rely on a well-known result from
measure theory, namely the _second Borel-Cantelli Lemma_ :

######  Theorem 1 ([7], Thm. 4.4, p. 55)

If $(U_{y})_{y\in\mathbb{N}}$ is a sequence of independent events in
$\mathbb{B}^{\mathbb{N}}$, and $\sum^{\infty}_{y}\mu_{\mathscr{C}}(U_{y})$
diverges, then
$\mu_{\mathscr{C}}\left(\bigcap_{y}\bigcup_{z>y}U_{z}\right)=1$.

Let us fix $n\in\mathbb{N}$ and let $\ell(n)$ indicate the length of the
binary string encoded by $n$. We suppose for simplicity that $\ell(n)>0$ (as
the case $\ell(n)=0$ is trivial). We construct $S^{n}$ in a few steps as
follows:

  * •

for all $p\in\mathbb{N}$, let $U_{p}^{n}$ be the cylinder of sequences which,
after $p$ steps, agree with $n$; observe that the sequences in $U_{p}^{n}$
satisfy the formula $\forall w.\varphi(n,p,0,w)$;

  * •

for all $p\in\mathbb{N}$, let $V_{p}^{n}=U^{n}_{p\cdot\ell(n)+1}$; observe
that the sets $V^{n}_{p}$ are pairwise independent and
$\mu_{\mathscr{C}}(\sum_{p}^{\infty}V^{n}_{p})=\infty$;

  * •

for all $p\in\mathbb{N}$, let
$S^{n}_{p}=\bigcup\\{U^{n}_{p+q}\mid\exists_{s>p}.p+q=s\cdot\ell(n)+1\\}$.
Observe that any sequence in $S^{n}_{p}$ satisfies $\exists z.\forall
w.\varphi(n,p,z,w)$; Moreover, one can check that
$S^{n}_{p}=\bigcup_{q>p}V^{n}_{q}$;

  * •

we finally let $S^{n}:=\bigcap_{p}S^{n}_{p}$.

We now have that any sequence in $S^{n}$ satisfies $\forall y.\exists
z.\forall w.\varphi(n,y,z,w)$; furthermore, by Theorem 1,
$\mu_{\mathscr{C}}(S^{n})=\mu_{\mathscr{C}}(\bigcap_{p}\bigcup_{q>p}V^{n}_{q})=1$.
Thus, for each choice of $n\in\mathbb{N}$,
$\mu_{\mathscr{C}}$$(\llbracket\forall y.\exists z.\forall
w.\varphi(x,p,z,w)\rrbracket_{\\{x\leftarrow n\\}})$ $\geq$
$\mu_{\mathscr{C}}(S^{n})\geq 1$, and we conclude that $\llbracket
F_{\mathtt{IMT}}\rrbracket_{\xi}=\mathbb{B}^{\mathbb{N}}$.

### The Random Walk Theorem.

A second example we consider is the _random walk theorem_ ($\mathtt{RW}$): any
simple random walk over $\mathbb{Z}$ starting from 1 will pass through 1
infinitely many times with probability 1. More formally, any
$\omega\in\mathbb{B}^{\mathbb{N}}$ induces a simple random walk starting from
1, by letting the $n$-th move be right if $\omega(n)=1$ holds and left if
$\omega(n)=0$ holds. One has then:

######  Theorem 2 ([7], Thm. 8.3, p. 117)

Let $U_{ij}^{(n)}\subseteq\mathbb{B}^{\mathbb{N}}$ be the set of sequences for
which the simple random walk starting from $i$ leads to $j$ in $n$ steps. Then
$\mu_{\mathscr{C}}\left(\bigcap_{x}\bigcup_{y\geq x}U_{11}^{(y)}\right)=1$.

Similarly, the random predicate $\mathsf{FLIP}(n)$ induces a simple random
walk starting from 1, by letting the $n$-th move be right if
$\mathsf{FLIP}(n)$ holds and left if $\neg\mathsf{FLIP}(n)$ holds. To
formalize $\mathtt{RW}$ in $\mathsf{MQPA}$ we make use two arithmetical
formulas:

  * •

$H(y,z)$ expresses that $y$ is even and $z$ is the code of a sequence of
length $\frac{y}{2}$, such that for all $i,j<\frac{y}{2}$, $z_{i}<y$, and
$z_{i}=z_{j}\Rightarrow i=j$ (that is, $z$ codes a subset of
$\\{0,\dots,y–1\\}$ of cardinality $\frac{y}{2}$);

  * •

$K(y,z,v)=H(y,z)\land\exists i.i<\frac{y}{2}\wedge z_{i}=v$.

The formula of $\mathsf{MQPA}$ expressing $\mathtt{RW}$ is as follows:

$F_{\mathtt{RW}}:\mathbf{C}^{1/1}\forall x.\exists y.\exists z.y\geq x\wedge
H(y,z)\wedge\forall
v.\Big{(}v<y\rightarrow\big{(}K(y,z,v)\leftrightarrow\mathsf{FLIP}(v)\big{)}\Big{)}.$

$F_{\mathtt{RW}}$ basically says that for any fixed $x$, we can find $y\geq x$
and a subset $z$ of $\\{0,\dots,y-1\\}$ of cardinality $\frac{y}{2}$,
containing all and only the values $v<y$ such that $\mathsf{FLIP}(v)$ holds
(so that the number of $v<y$ such that $\mathsf{FLIP}(v)$ holds coincides with
the number of $v<y$ such that $\neg\mathsf{FLIP}(v)$ holds). This is the case
precisely when the simple random walk goes back to 1 after exactly $y$ steps.

To show the validity of $F_{\mathtt{RW}}$ we can use the measurable set
$S=\bigcap_{n}\bigcup_{p\geq n}U_{11}^{(p)}$. Let $\psi(y,z,v)$ be the formula
$(v<y\rightarrow(K(y,z,v)\leftrightarrow\mathsf{FLIP}(v)))$. Observe that any
sequence in $U_{11}^{(n)}$ satisfies the formula $\exists z.H(n,z)\land\forall
v.\psi(y,z,v,w)$. Then, any sequence in $S$ satisfies the formula $\forall
x.\exists y.\exists z.y\geq x\land H(y,z)\land\forall v.\psi(y,z,v)$. Since,
by Theorem 2, $\mu_{\mathscr{C}}(S)=1$, we conclude that
$\mu_{\mathscr{C}}(\llbracket
F_{\mathtt{RW}}\rrbracket_{\xi})\geq\mu_{\mathscr{C}}(S)\geq 1$, and thus that
$\llbracket F_{\mathtt{RW}}\rrbracket_{\xi}=\mathbb{B}^{\mathbb{N}}$.

##  4 Arithmetization

It is a classical result in computability theory [23, 25, 26, 59, 61] that all
computable functions are arithmetical, that is, for each partial recursive
function $f:\mathbb{N}^{m}\rightharpoonup\mathbb{N}$ there is an arithmetical
formula $F_{f}$, such that for every $n_{1},\dots,n_{m},l\in\mathbb{N}$:
$f(n_{1},\dots,n_{m})=l$ $\Leftrightarrow$ $(\mathbb{N},+,\times)\vDash
F_{f}(n_{1},\dots,n_{m},l)$. In this section we show that, by considering
arithmetical formulas of $\mathsf{MQPA}$, this fundamental result can be
generalized to computable _random_ functions.

### Computability in Presence of Probabilistic Choice.

Although standard computational models are built around determinism, from the
1950s on, models for _randomized_ computation started to receive wide
attention [40, 14, 49, 53, 54, 21, 22, 57]. The first formal definitions of
probabilistic Turing machines (for short, PTM) are due to Santos [53, 54] and
Gill [22, 21]. Roughly, a PTM is an ordinary Turing machine (for short, TM)
with the additional capability of making random decisions. Two alternative
paradigms have been developed in the literature, the so-called _Markovian_ and
_oracle_ PTMs. Here, we consider the definition by Gill, in which the
probabilistic choices performed by the machines are binary and fair.

######  Definition 5 (Probabilistic Turing Machine [21, 22])

A (one-tape) _probabilistic Turing machine_ is a 5-tuple
$(Q,\Sigma,\delta,q_{0},Q_{f})$, whose elements are defined as in a standard
TM, except for the probabilistic transition function $\delta$, which, given
the current (non-final) state and symbol, specifies two equally-likely
transition steps.

As any ordinary TM computes a partial function on natural numbers, PTM can be
seen as computing a so-called _random function_ [53, pp. 706–707]. Let
$\mathbb{D}(\mathbb{N})$ indicate the set of _pseudo-distributions_ on
$\mathbb{N}$, i.e. of functions $f:\mathbb{N}\to\mathbb{R}_{[0,1]}$, such that
$\sum_{n\in\mathbb{N}}f(n)\leq 1$. Given a PTM, $\mathcal{M}$, a random
function is a function
$\langle\mathcal{M}\rangle:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$ which,
for each natural number $n$, returns a pseudo-distribution supporting all the
possible outcomes $\mathcal{M}$ produces when fed with (an encoding of) $n$ in
input, each with its own probability.333The seminal definition of _random
function_ already appeared in [53]:  Definition. A $k$-ary random function
$\phi$ is a function from $E^{n+1}$, the collection of all $(k+1)$-tuples of
nonnegative integers, to [0,1] satisfying
$\sum_{m=0}^{\infty}\phi(m_{1},m_{2},\cdots,m_{k},m)\leq 1$ for every
$k$-tuple ($m_{1},m_{2},\dots,m_{k})$. [53, pp. 706-707] Remarkably, in the
same paper, Santos also delineated the notion of _probabilistic transition
function_ , on which the Markovian paradigm of PTM is based [53, p. 705] [54,
p. 170]. As expected, the random function
$f:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$ is said to be _computable_
when there is a PTM, $\mathcal{M}$, such that $\langle\mathcal{M}\rangle=f$.

Another widespread definition of TM is the one based on the notion of oracle.
An _oracle TM_ is a pair consisting of a standard deterministic TM and a
random-bit oracle (for further details, see for example [16]). The random-bit
oracle takes the form of an _oracle tape_ , which is consulted whenever a
coin-tossing state is encountered. The two definitions are assumed to be
equivalent but, to the best of the authors’ knowledge, no formal proof of this
equivalence has been presented in the literature yet.

### Stating the Main Result.

In order to generalize Gödel’s arithmetization of partial recursive functions
to the class of computable random functions, we start by introducing the
notion of arithmetical random function.

######  Definition 6 (Arithmetical Random Function)

A random function $f:\mathbb{N}^{m}\rightarrow\mathbb{D}(\mathbb{N})$ is said
to be _arithmetical_ if and only if there is a formula of $\mathsf{MQPA}$,
call it $F_{f}$, with free variables $x_{1},\dots,x_{m},y$, such that for
every $n_{1},\dots,n_{m},l\in\mathbb{N}$, it holds that:

$\displaystyle\mu_{\mathscr{C}}\big{(}\llbracket
F_{f}(n_{1},\dots,n_{m},l)\rrbracket\big{)}=f(n_{1},\dots,n_{m})(l).$ (1)

The _arithmetization theorem_ below relates random functions and the formulas
of $\mathsf{MQPA}$, and is the main result of this paper.

###### Theorem 3

All computable random functions are arithmetical.

Actually, we establish a stronger fact. Let us call a formula $A$ of
$\mathsf{MQPA}$ $\Sigma_{1}^{0}$ if $A$ is equivalent to a formula of the form
$\exists x_{1}.\dots.\exists x_{n}.A^{\prime}$, where $A^{\prime}$ contains
neither first-order nor measure quantifiers. Then Theorem 3 can be
strengthened by saying that any computable random function is represented (in
the sense of Definition 6) by a $\Sigma_{1}^{0}$-formula of $\mathsf{MQPA}$.

Moreover, we are confident that a sort of converse of this fact can be
established, namely that for any $\Sigma_{1}^{0}$-formula
$A(x_{1},\dots,x_{m})$ there exists a computable random relation
$r(x_{1},\dots,x_{m})$ (i.e. a computable random function such that
$r(x_{1},\dots,x_{n})(i)=0$ whenever $i\neq 0,1$) such that
$\mu_{\mathscr{C}}(\llbracket
A(n_{1},\dots,n_{m})\rrbracket)=r(n_{1},\dots,n_{m})(0)$ and
$\mu_{\mathscr{C}}(\llbracket\lnot
A(n_{1},\dots,n_{m})\rrbracket)=r(n_{1},\dots,n_{m})(1)$. However, we leave
this fact and, more generally, the exploration of an _arithmetical hierarchy_
of randomized sets and relations, to future work.

Given the conceptual distance existing between TMs and arithmetic, a direct
proof of Theorem 3 would be cumbersome. It is thus convenient to look for an
alternative route.

### On Function Algebras.

In [11, 13], the class $\mathcal{PR}$ of _probabilistic_ or _random recursive
functions_ is defined as a generalization of Church and Kleene’s standard one
[10, 32, 34, 35]. $\mathcal{PR}$ is characterized as the smallest class of
functions, which (i) contains some basic random functions, and (ii) is closed
under composition, primitive recursion and minimization. For all this to make
sense, composition and primitive recursion are defined following the _monadic_
structure of $\mathbb{D}(\cdot)$. In order to give a presentation as
straightforward as possible, we preliminarily introduce the notion of _Kleisli
extension_ of a function with values in $\mathbb{D}(\mathbb{N})$.

######  Definition 7 (Kleisli Extension)

Given a function $f:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$, its
_(simple) Kleisli extension_
$f^{\mathbf{K}}:\mathbb{D}(\mathbb{N})\rightarrow\mathbb{D}(\mathbb{N})$ is
defined as follows:

$f^{\mathbf{K}}(d)(n)=\sum_{i\in\mathbb{N}}d(i)\cdot f(i)(n).$

More in general, given a $k$-ary function $f:X_{1}\times\dots\times
X_{i-1}\times\mathbb{N}\times X_{i+1}\times\dots\times
X_{k}\rightarrow\mathbb{D}(\mathbb{N})$, its _$i$ -th Kleisli extension_
$f^{\mathbf{K}}_{i}:X_{1}\times\dots\times
X_{i-1}\times\mathbb{D}(\mathbb{N})\times X_{i+1}\times\dots\times
X_{k}\rightarrow\mathbb{D}(\mathbb{N})$ is defined as follows:

$f^{\mathbf{K}}_{i}(x_{1},\dots,x_{i-1},d,x_{i+1},\dots,x_{k})(n)=\sum_{j\in\mathbb{N}}d(j)\cdot
f(x_{1},\dots,x_{i-1},j,x_{i+1},\dots,x_{k})(n).$

The construction at the basis of the $\mathbf{K}$-extension’s general case can
be applied more than once.444For example, let us consider a binary function
$f:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$, its _total_
$\mathbf{K}$-extension is as follows:  $\displaystyle
f_{1}^{\mathbf{K}}(d_{1},d_{2})(y)$
$\displaystyle=\sum_{i_{1}\in\mathbb{N}}d_{1}(i_{1})\cdot
f^{\mathbf{K}}_{2}(i_{1},d_{2})(y)$
$\displaystyle=\sum_{i_{1}\in\mathbb{N}}d_{1}(i_{1})\cdot\Big{(}\sum_{i_{2}\in\mathbb{N}}d_{2}(i_{2})\cdot
f(i_{1},i_{2})(y)\Big{)}$
$\displaystyle=\sum_{i_{1},i_{2}\in\mathbb{N}}f(i_{1},i_{2})(y)\cdot
d_{1}(i_{1})\cdot d_{2}(i_{2})$
$\displaystyle=\sum_{i_{1},i_{2}\in\mathbb{N}}f(i_{1},i_{2})(y)\cdot\prod_{k\in\\{1,2\\}}d_{k}(i_{k}).$
Specifically, given a function
$f:\mathbb{N}^{k}\rightarrow\mathbb{D}(\mathbb{N})$, its _total_
$\mathbf{K}$-extension
$f^{\mathbf{K}}:\left(\mathbb{D}(\mathbb{N})\right)^{k}\rightarrow\mathbb{D}(\mathbb{N})$
is defined as follows:

$f^{\mathbf{K}}(d_{1},\dots,d_{k})(n)=\sum_{i_{1},\dots,i_{k}\in\mathbb{N}}f(i_{1},\dots,i_{k})(n)\cdot\prod_{1\leq
j\leq k}d_{j}(i_{j}).$

We can now define the class $\mathcal{PR}$ formally as follows:

######  Definition 8 (The Class $\mathcal{PR}$ [11])

The _class of probabilistic recursive functions_ , $\mathcal{PR}$, is the
smallest class of probabilistic functions containing:

  * •

The _zero function_ $,z:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$, such
that for every $x\in\mathbb{N}$, $z(x)(0)=1$;

  * •

The _successor function_ , $s:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$,
such that for every $x\in\mathbb{N}$, $s(x)(x+1)=1$;

  * •

The _projection function_ ,
$\pi_{m}^{n}:\mathbb{N}^{n}\rightarrow\mathbb{D}(\mathbb{N})$, defined as for
$1\leq m\leq n$, $\pi_{m}^{n}(x_{1},\dots,x_{n})(x_{m})=1$;

  * •

The _fair coin function_ , $r:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$,
defined as follows:

$r(x)(y)=\begin{cases}\frac{1}{2}\ \ \ &\text{ if }y=x\\\ \frac{1}{2}\ \ \
&\text{ if }y=x+1\\\ 0\ \ \ &\text{ otherwise;}\end{cases}$

and closed under:

  * •

_Probabilistic composition_. Given
$f:\mathbb{N}^{n}\rightarrow\mathbb{D}(\mathbb{N})$ and
$g_{1},\dots,g_{n}:\mathbb{N}^{k}\rightarrow\mathbb{D}(\mathbb{N})$, their
composition is a function
$f\odot(g_{1},\dots,g_{n}):\mathbb{N}^{k}\rightarrow\mathbb{D}(\mathbb{N})$
defined as follows:555That is,
$\displaystyle((f\odot(g_{1},\dots,g_{n}))(\mathtt{x}))(y)$
$\displaystyle=(f^{\mathbf{K}}(g_{1}(\mathtt{x}),\dots,g_{n}(\mathtt{x})))(y)$
$\displaystyle=\sum_{i_{1},\dots,i_{n}}f(i_{1},\dots,i_{k})(y)\cdot\prod_{1\leq
j\leq n}g_{j}(\mathtt{x})(i_{j}).$ The simplest case, is teat of unary
composition which is defined as follows, given
$f:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$ and
$g:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$, the function
$h:\mathbb{N}\rightarrow\mathbb{D}(\mathbb{N})$ obtained by composition from
$f$ and $g$ is:  $(f\odot g)(x)(y)=f^{\mathbf{K}}(g(x))(y)$ Otherwise said,
$((f\odot g)(x))(y)=\sum_{z\in\mathbb{N}}g(x)(z)\cdot f(z)(y).$

$(f\odot(g_{1},\dots,g_{n}))(\mathtt{x})=f^{\mathbf{K}}(g_{1}(\mathtt{x}),\dots,g_{n}(\mathtt{x}));$

  * •

_Probabilistic primitive recursion._ Given
$f:\mathbb{N}^{k}\rightarrow\mathbb{D}(\mathbb{N})$, and
$g:\mathbb{N}^{k+2}\rightarrow\mathbb{D}(\mathbb{N}),$ the function
$h:\mathbb{N}^{k+1}\rightarrow\mathbb{D}(\mathbb{N})$ obtained from them by
primitive recursion is as follows:

$\displaystyle h(\mathtt{x},0)$ $\displaystyle=f(x)$ $\displaystyle
h(\mathtt{x},y+1)$
$\displaystyle=g^{\mathbf{K}}_{k+2}(\mathtt{x},y,h(\mathtt{x},y));$

  * •

_Probabilistic minimization._ Given
$f:\mathbb{N}^{k+1}\rightarrow\mathbb{D}(\mathbb{N}),$ the function
$h:\mathbb{N}^{k}\rightarrow\mathbb{D}(\mathbb{N})$, obtained from it by
minimization is defined as follows:

$\mu
f(\mathtt{x})(y)=f(\mathtt{x},y)(0)\cdot\Big{(}\prod_{z<y}\Big{(}\sum_{k>0}f(\mathtt{x},z)(k)\Big{)}\Big{)}.$

######  Proposition 1 ([11])

$\mathcal{PR}$ coincides with the class of computable random functions.

The class $\mathcal{PR}$ is still conceptually far from $\mathsf{MQPA}$. In
fact, while the latter has access to randomness in the form of a global supply
of random bits, the former can fire random choices locally through a dedicated
initial function. To bridge the gap between the two, we introduce a third
characterization of computable random functions, which is better-suited for
our purposes. In doing so, we will define the class of oracle recursive
functions, $\mathcal{OR}$. Our definition is loosely inspired from _oracle_
TM, which can be defined as deterministic TM whose transition function can
query a _random-bit tape_ $\omega\in\mathbb{B}^{\mathbb{N}}$.

The class of _oracle recursive functions_ , $\mathcal{OR}$, is the smallest
class of partial functions of the form
$f:\mathbb{N}^{m}\times\mathbb{B}^{\mathbb{N}}\rightharpoonup\mathbb{N},$
which (i) contains the class of _oracle basic functions_ , and (ii) is closed
under composition, primitive recursion, and minimization. Formally,

######  Definition 9 (The Class $\mathcal{OR}$)

The _class of oracle recursive functions_ , $\mathcal{OR}$, is the smallest
class of probabilistic functions containing:

  * •

The _zero function_ , $f_{0}$, such that $f_{0}(x_{1},\dots,x_{k},\omega)=0$;

  * •

The _successor function_ , $f_{s},$ such that $f_{s}(x,\omega)=x+1$;

  * •

The _projection function_ , $f_{\pi_{i}},$ such that, for $1\leq i\leq k$,
$f_{\pi_{i}}(x_{1},\dots,x_{k},\omega)=x_{i}$;

  * •

The _query function_ , $f_{q},$ such that $f_{q}(x,\omega)=\omega(x)$;

and closed under:

  * •

_Oracle composition_. Given the oracle functions $h$ from
$\mathbb{N}^{n}\times\mathbb{B}^{\mathbb{N}}$ to $\mathbb{N}$ and $g_{1},\dots
g_{n}$ (from $\mathbb{N}^{m}$), the function $f$ obtained by composition from
them, is defined as follows:

$f(x_{1},\dots,x_{m},\omega)=h(g_{1}(x_{1},\dots,x_{m},\omega),\dots,g_{n}(x_{1},\dots,x_{m},\omega),\omega);$

  * •

_Oracle primitive recursion_. Given two oracle functions $h$ and $g$, from
respectively $\mathbb{N}^{n}\times\mathbb{B}^{\mathbb{N}}$ and
$\mathbb{N}^{n+2}\times\mathbb{B}^{\mathbb{N}}$ to $\mathbb{N}$, the function
$f$, obtained by primitive recursion from them, is defined as follows:

$f(x,x_{1},\dots,x_{n})=\begin{cases}f(0,x_{1},\dots,x_{n},\omega)=h(x_{1},\dots,x_{n},\omega)\\\
f(x+1,x_{1},\dots,x_{n},\omega)=g(f(x,x_{1},\dots,x_{n},\omega),x,x_{1},\dots,x_{n},\omega);\end{cases}$

  * •

_Oracle minimization_. Given the oracle function $g$ from
$\mathbb{N}^{n+1}\times\mathbb{B}^{\mathbb{N}}$ to $\mathbb{N}$, the function
$f$, obtained by minimization from $g$, is defined as follows:

$f(x_{1},\dots,x_{n},\omega)=\mu x(g(x_{1},\dots,x_{n},x,\omega)=0).$

Remarkably, the only basic function depending on $\omega$ is the query
function. All the closure schemes are independent from $\omega$ as well.

But in what sense do functions in $\mathcal{OR}$ represent random functions?
In order to clarify the relationship between $\mathcal{OR}$ and
$\mathcal{PR}$, we associate each $\mathcal{OR}$ function with a corresponding
auxiliary function.

######  Definition 10 (Auxiliary Function)

Given an oracle function
$f:\mathbb{N}^{m}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$, the
corresponding _auxiliary function_ ,
$f^{*}:\mathbb{N}^{m}\times\mathbb{N}\rightarrow\mathcal{P}(\mathbb{B}^{\mathbb{N}})$,
is defined as follows: $f^{*}(x_{1},\dots,x_{m},y)=\\{\omega\ |\
f(x_{1},\dots,x_{m},\omega)=y\\}.$

The following lemma ensures that the value of $f^{*}$ is always a _measurable_
set:

###### Lemma 2

For every oracle recursive function $f\in\mathcal{OR}$,
$f:\mathbb{N}^{m}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$, and
natural numbers $x_{1},\dots,x_{m},y\in\mathbb{N}$, the set
$f^{*}(x_{1},\dots,x_{m},y)$ is measurable.

  * Proof.

We will show that, for each $f\in\mathcal{OR}$, $f^{*}\in\sigma(\mathscr{C})$,
by induction on the structure of oracle recursive functions:

    * •

Let $f\in\mathcal{OR}$ be an oracle basic function. There are four possible
cases:

Zero Function. Let $f_{0}$ be the zero function,
$f_{0}(x_{1},\dots,x_{n},\omega)=0$. Then,

$f_{0}^{*}(x_{1},\dots,x_{n},0)=\\{\omega\ |\
f_{0}(x_{1},\dots,x_{n},\omega)=0\\}=\mathbb{B}^{\mathbb{N}}.$

For Axioms 1 of the $\sigma$-algebra,
$\mathbb{B}^{\mathbb{N}}\in\sigma(\mathscr{C})$, so
$f_{0}^{*}\in\sigma(\mathscr{C})$.

Successor Function. Let $f_{s}$ be the successor function
$f_{s}(x,\omega)=x+1$. Then,

$f_{s}^{*}(x,x+1)=\\{\omega\ |\
f_{s}(x,\omega)=x+1\\}=\mathbb{B}^{\mathbb{N}}.$

As before, $f_{s}^{*}\in\sigma(\mathscr{C})$.

Projection Function. Let $f_{\pi_{i}}$ be the projection function,
$f_{\pi_{i}}(x_{1},\dots,x_{n},\omega)=x_{i}$, with $1\leq i\leq n$. Then,

$f_{\pi_{i}}^{*}(x_{1},\dots,x_{n},x_{i})=\\{\omega\ |\
f_{\pi_{i}}(x_{1},\dots,x_{n},\omega)=x_{i}\\}=\mathbb{B}^{\mathbb{N}}.$

Again, $f_{\pi_{i}}^{*}\in\sigma(\mathscr{C})$.

Query Function. Let $f_{q}$ be the query function,
$f_{q}(x,\omega^{\prime})=\omega^{\prime}(x)$. Then,

$f_{q}^{*}(x,\omega^{\prime})=\\{\omega\ |\
f_{q}(x,\omega)=\omega^{\prime}(x)\\}=\\{\omega\ |\ \omega(x)=0\\}$

for $\omega^{\prime}(x)=0$ or $f_{q}^{*}(x,\omega^{\prime})=\\{\omega$ $|$
$\omega(x)=1\\}$ if $\omega^{\prime}(x)=1$, in both cases
$f_{q}^{*}(x,\omega^{\prime})$ is a (thin) cylinder, so
$f_{q}^{*}(x,0)\in\sigma(\mathscr{C})$. Therefore,
$f_{q}^{*}\in\sigma(\mathscr{C})$.

    * •

Let $f\in\mathcal{OR}$ be obtained by oracle composition, recursion or
minimization from $\mathcal{OR}$ functions. Since the three cases are proved
in a similar way, let us take into account (simple) composition only. Let
$f:\mathbb{N}^{n}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$ be
obtained by (unary) composition from
$h:\mathbb{N}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$ and
$g:\mathbb{N}^{n}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$. Assume
$f(x_{1},\dots,x_{n},\omega)$ = $h(g(x_{1},\dots,x_{n},\omega),\omega)$ = $v$.
By Definition 10, $f^{*}(x_{1},\dots,x_{n},v)$ =
$\bigcup_{z\in\mathbb{N}}\\{\omega$ $|$ $h(z,\omega)=v\\}$ $\cap$ $\\{\omega$
$|$ $g(x_{1},\dots,x_{n},\omega)=z\\}$ =
$\bigcup_{z\in\mathbb{N}}h^{*}(z,v)\cap g^{*}(x_{1},\dots,x_{n},z)$. By IH,
$h^{*},g^{*}\in\sigma(\mathscr{C})$ so, by Axiom 3 of $\sigma$-algebras,
$h^{*}\cap g^{*}\in\sigma(\mathscr{C})$ as well. Therefore, since $f^{*}$ is a
countable union of measurable sets, again for Axiom 3, it is measurable as
well, so $f^{*}\in\sigma(\mathscr{C})$.

$\Box$

Thanks to Lemma 2, we can associate any oracle recursive function
$f:\mathbb{N}^{m}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$ with a
random function $f^{\\#}:\mathbb{N}^{m}\rightarrow\mathbb{D}(\mathbb{N})$,
defined as:
$f^{\\#}(x_{1},\ldots,x_{m})(y)=\mu_{\mathscr{C}}(f^{*}(x_{1},\ldots,x_{m},y)).$
This defines a close correspondence between the classes $\mathcal{PR}$ and
$\mathcal{OR}$.

###### Proposition 2

For each $f\in\mathcal{PR}$, there is an oracle function $g\in\mathcal{OR}$,
such that $f=g^{\\#}$. Symmetrically, for any $f\in\mathcal{OR}$, there is a
random function $g\in\mathcal{PR}$, such that $g=f^{\\#}$.

For our purpose, only the first part of Proposition 2 is necessary, namely
that for every $f\in\mathcal{PR}$, there is a $g\in\mathcal{OR}$ such that
$g^{\\#}=f$. This is established by means of a few intermediate steps.

First, some auxiliary notions are introduced. A _computable bijection_ between
$\mathbb{N}$ and $\mathbb{N}\times\mathbb{N}$ and the corresponding maps
$\langle\cdot,\cdot\rangle:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$
and $\pi_{1},\pi_{2}:\mathbb{N}\rightarrow\mathbb{N}$ is fixed. A _tree_ is
defined as a subset $X$ of $\mathbb{B}^{*}$ (the finite set of strings) such
that if $t\in X$ and $v\sqsubset t$ ($\sqsubseteq$ being the prefix relation),
then $v\not\in X$. Given $t\in\mathbb{B}^{*}$,
$\omega\in\mathbb{B}^{\mathbb{N}}$ is said to be an _n-extension_ of $t$ if
and only if $\omega=v\cdot t\cdot\omega^{\prime}$, where $|v|=n$ and
$\omega^{\prime}\in\mathbb{B}^{\mathbb{N}}$. The set of all $n$-extensions of
$t$ is indicated as $\textsf{EXT}^{n}_{t}$ and is measurable. Moreover,
$\mu(\textsf{EXT}^{n}_{t})=\frac{1}{2^{|t|}}$ for every $n$ and $t$. Given a
tree $X$, every function $f:X\rightarrow\mathbb{N}$ is said to be an _$X$
-function_. Thus, an oracle function
$f:\mathbb{N}^{n+1}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}\in\mathcal{OR}$
returns a tree $X$ and an $X$-function $g$ on input $(m_{1},\dots,m_{n})$ if
and only if for every $k\in\mathbb{N}$, it holds that:

  * •

$f(m_{1},\dots,m_{n},k,\omega)$ is defined if and only if
$\omega\in\textsf{EXT}^{k}_{t}$, where $t\in X$.

  * •

if $\omega\in\textsf{EXT}^{k}_{t}$ and $t\in X$, then

$f(m_{1},\dots,m_{n},k,\omega)=q,$

where $\pi_{1}(q)=g(t)$ and $\pi_{2}(q)=|t|$.

It is now possible to prove the following preliminary lemma.

###### Lemma 3

For every $f:\mathbb{N}^{n}\rightarrow\mathbb{D}(\mathbb{N})\in\mathcal{PR}$,
there is an oracle recursive function
$g:\mathbb{N}^{n+1}\times\mathbb{B}^{\mathbb{N}}\rightharpoonup\mathbb{N}\in\mathcal{OR}$,
such that for every $m_{1},\dots,m_{n}$, $g$ returns a tree
$X_{m_{1},\dots,m_{n}}$ and an $X_{m_{1},\dots,m_{n}}$-function
$h_{m_{1},\dots,m_{n}}$ on input $m_{1},\dots,m_{n}$, and

$f(m_{1},\dots,m_{n})(y)=\sum_{h_{m_{1},\dots,m_{n}}(t)=y}\frac{1}{2^{|t|}}.$

  * Proof.

The proof is by induction on the structure of $f$ as an element of
$\mathcal{PR}$.

    * •

Let $f\in\mathcal{PR}$ be a basic probabilistic function. Then, there are four
possible cases.

Zero Function. Let $z\in\mathcal{PR}$ be the zero function. Then,
$g\in\mathcal{OR}$ is an oracle function, so defined that on inputs
$m_{1},k,\omega$, it returns the value $\langle 0,0\rangle$. Indeed, $g$
returns the tree $X_{m_{1}}=\\{\epsilon\\}$ and the $X_{m_{1}}$-function
$h_{m_{1}}$ always returning 0, as it can be easily checked. Moreover:

$\displaystyle z(m_{1})(y)$ $\displaystyle=\begin{cases}1\ \ \ \text{ if
}y=0\\\ 0\ \ \ \text{ otherwise}\end{cases}$
$\displaystyle=\sum_{h_{m_{1}}(s)=y}\frac{1}{2^{|t|}}.$

Successor Function. Let $s\in\mathcal{PR}$ be the successor function. Then,
$g\in\mathcal{OR}$ is an oracle function, so defined that on inputs
$m_{1},k,\omega$, it returns the value $\langle m_{1}+1,0\rangle$. So, $g$
returns the tree $X_{m_{1}}=\\{\epsilon\\}$ and the $X_{m_{1}}$-function
$h_{m_{1}}$ always returning $m_{1}+1$. Therefore:

$\displaystyle s(m_{1})(y)$ $\displaystyle=\begin{cases}1\ \ \ \text{ if
}y=m_{1}+1\\\ 0\ \ \ \text{ otherwise}\end{cases}$
$\displaystyle=\sum_{h_{m_{1}}(t)=y}\frac{1}{2^{|t|}}.$

Projection Function. Let $\pi^{n}_{i}\in\mathcal{PR}$, with $1\leq i\leq n$,
be the projection function. Then, $g\in\mathcal{OR}$ is an oracle function, so
defined that, on inputs $m_{1},\dots,m_{n},k,\omega$ it returns the value
$\langle m_{i},0\rangle$. Indeed, $g$ returns the tree
$X_{m_{1},\dots,m_{n}}=\\{\epsilon\\}$ and the
$X_{m_{1},\dots,m_{n}}$-function $h_{m_{1},\dots,m_{n}}$ always returning
$m_{i}$. Moreover:

$\displaystyle\pi^{n}_{i}(m_{1},\dots,m_{n})(y)$
$\displaystyle=\begin{cases}1\ \ \ \text{ if }y=m_{i}\\\ 0\ \ \ \text{
otherwise}\end{cases}$
$\displaystyle=\sum_{h_{m_{1},\dots,m_{n}}(t)=y}\frac{1}{2^{|t|}}.$

Fair Coin Function. Let $r\in\mathcal{PR}$ be the fair coin function. Then,
$g\in\mathcal{OR}$ is an oracle function, so defined that
$g(m_{1},k,\omega)=\langle l,1\rangle$ where,

$l=\begin{cases}m_{1}\ \ \ \text{ if }\omega[k]=0\\\ m_{1+1}\ \ \ \text{ if
}\omega[k]=1.\end{cases}$

    * •

If $f$ is obtained by either composition, primitive recursion or minimization,
the argument is a bit more involved, as in defining the function $g$ we must
take into account how the bits of the oracle accessed by $g$ are distributed
in an independent way to each of the component functions. We will here only
illustrate how this works in the case of composition.

Let then $f$ be obtained by composition from
$f_{1},\dots,f_{p}:\mathbb{N}^{n}\rightarrow\mathbb{D}(\mathbb{N})$ and
$f^{\prime}:\mathbb{N}^{p}\rightarrow\mathbb{D}(\mathbb{N})$, i.e.
$f(m_{1},\dots,m_{n})(y)=\sum_{i_{1},\dots,i_{p}}f^{\prime}(i_{1},\dots,i_{p})(y)\cdot\prod_{j=1}^{p}f_{j}(m_{1},\dots,m_{n})(i_{j})$.
By induction hypothesis there exist functions
$g_{1},\dots,g_{p}:\mathbb{N}^{n+1}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$
and
$g^{\prime}:\mathbb{N}^{p+1}\times\mathbb{B}^{\mathbb{N}}\rightarrow\mathbb{N}$
such that

      1. 1.

for all $m_{1},\dots,m_{n}\in\mathbb{N}$, each $g_{i}$ returns a tree
$X^{i}_{m_{1},\dots,m_{n}}$ and an $X^{i}_{m_{1},\dots,m_{n}}$-function
$h^{i}_{m_{1},\dots,m_{n}}$, and
$f_{i}(m_{1},\dots,m_{n})(y)=\sum_{h^{i}_{m_{1},\dots,m_{n}}(t)=y}\frac{1}{2^{|t|}}$;

      2. 2.

for all $m_{1},\dots,m_{p}\in\mathbb{N}$, $g^{\prime}$ returns a tree
$Y_{m_{1},\dots,m_{n}}$ and a $Y_{m_{1},\dots,m_{p}}$-function
$h^{\prime}_{m_{1},\dots,m_{p}}$, and
$f^{\prime}(m_{1},\dots,m_{p})(y)=\sum_{h^{\prime}_{m_{1},\dots,m_{p}}(t)=y}\frac{1}{2^{|t|}}$.

We thus have that

$\displaystyle f(m_{1},\dots,m_{n})(y)$
$\displaystyle=\sum_{i=1,\dots,i_{p}}\left(\sum_{h^{\prime}_{i_{1},\dots,i_{p}}(s)=y}\frac{1}{2^{|s|}}\right)\cdot\left(\prod_{j=1}^{p}\sum_{h^{j}_{m_{1},\dots,m_{n}}(t)=i_{j}}\frac{1}{2^{|t|}}\right)$
$\displaystyle=\sum_{i=1,\dots,i_{p}}\left(\sum_{h^{\prime}_{i_{1},\dots,i_{p}}(s)=y,h^{j}_{m_{1},\dots,m_{n}}(t_{j})=i_{j}}\frac{1}{2^{|s|+\sum_{j=1}^{p}|t_{j}|}}\right)$

For all $m_{1},\dots,m_{n}\in\mathbb{N}$, let
$X_{m_{1},\dots,m_{n}}=\\{t_{1}\cdot\dots\cdot t_{p}\mid s\in t_{j}\in
X^{j}_{m_{1},\dots,m_{n}},s\in
Y_{h_{\vec{m}}^{1}(t_{1}),\dots,h_{\vec{m}}^{p}(t_{p})}\\}$.

Observe that any $v\in X_{m_{1},\dots,m_{n}}$ can be decomposed in a unique
way as $v=t_{0}\cdot t_{1}\cdot\dots\cdot t_{p}$. In fact, if
$t^{\prime}_{0}\cdot t^{\prime}_{1}\cdot\dots\cdot t^{\prime}_{p}$ is any
other decomposition, let $j\leq p$ be minimum such that $t_{j}\neq
t^{\prime}_{j}$. Then it must be either $t_{j}\sqsubset t^{\prime}_{j}$ or
$t^{\prime}_{j}\sqsubset t_{j}$, which contradicts the fact that
$X^{j}_{m_{1},\dots,m_{n}}$ and
$Y_{h_{\vec{m}}^{1}(t_{1}),\dots,h_{\vec{m}}^{p}(t_{p})}$ are all trees.

Using this fact we can show that $X_{m_{1},\dots,m_{n}}$ is also a tree:
suppose $v=t_{0}\cdot t_{1}\cdot\dots\cdot t_{p}\in X_{m_{1},\dots,m_{n}}$ and
suppose $v^{\prime}\in X_{m_{1},\dots,m_{n}}$, where $v^{\prime}\sqsubset v$.
Then $v^{\prime}$ has a unique decomposition $t^{\prime}_{0}\cdot\dots\cdot
t^{\prime}_{p}$ and one can easily show by induction on $j\leq p$ that
$t^{\prime}_{j}=t^{\prime}_{j}$ holds. Hence it must be $v^{\prime}=v$,
against the assumption.

Let $h_{m_{1},\dots,m_{n}}:X_{m_{1},\dots,m_{n}}\to\mathbb{N}$ be defined by
$h_{m_{1},\dots,m_{n}}(v)=y$, where $v$ uniquely decomposes as $s\cdot
t_{1}\cdot\dots\cdot t_{p}$, $h^{j}_{\vec{m}}(t_{j})=i_{j}$ and
$h^{\prime}_{i_{1},\dots,i_{p}}(s)=y$. We can finally define:

$g(m_{1},\dots,m_{n},k,\omega)=\left\langle\pi_{1}\Big{(}g^{\prime}\big{(}\pi_{1}(L_{1}),\dots,\pi_{1}(L_{p}),k+\sum_{j=1}^{p}L_{j},\omega\big{)}\Big{)},\pi_{2}\Big{(}g^{\prime}\big{(}\pi_{1}(L_{1}),\dots,\pi_{1}(L_{p}),k+\sum_{j=1}^{p}L_{j},\omega\big{)}\Big{)}+R_{p}\right\rangle$

where the $L_{j},R_{j}$ are defined inductively as follows:

$\displaystyle L_{1}$ $\displaystyle=g_{1}(\vec{m},k,\omega)$ $\displaystyle
R_{1}$ $\displaystyle=0$ $\displaystyle L_{j+1}$
$\displaystyle=g_{j+1}(\vec{m},k+R_{j+1},\omega)$ $\displaystyle R_{j+1}$
$\displaystyle=R_{j}+\pi_{2}(L_{j})$

It can be checked that, by construction,
$g(m_{1},\dots,m_{n},k,\omega)=\langle h_{m_{1},\dots,m_{n}}(v),|v|\rangle$,
where $v\in\mathsf{EXT}^{k}_{v^{\prime}}$ and $v^{\prime}$ uniquely decomposes
as $s\cdot t_{1}\cdot\dots\cdot t_{p}$. Using the equations above we thus
have:

$\displaystyle f(m_{1},\dots,m_{n})(y)$
$\displaystyle=\sum_{h_{m_{1},\dots,m_{n}}(v)=y}\frac{1}{2^{|v|}}$

$\Box$

The desired Proposition 2 can now be proved as a corollary of Lemma 3. Indeed,
once it is observed that if $g$ is obtained from $f\in$, as in Lemma 3, and
$h(m_{1},\dots,m_{n},\omega)=\pi_{1}(g(m_{1},\dots,m_{n},0,\omega))$, then it
follows that $f=h^{\\#}$.

### The Proof of the Main Result.

The last ingredient to establish Theorem 3 is the following lemma, easily
proved by induction on the structure of $\mathcal{OR}$ functions.

###### Lemma 4

For every oracle function $f\in\mathcal{OR}$, the random function $f^{\\#}$ is
arithmetical.

  * Proof.

By Definition 10, given an arbitrary oracle function $f\in\mathcal{OR}$,
$f(x_{1},\dots,x_{m},\omega)$ = $y$, the corresponding $f^{\\#}$ is defined as
follows

$f^{\\#}=\mu_{\mathscr{C}}(f^{*}(x_{1},\dots,x_{m},y))=\mu_{\mathscr{C}}(\\{\omega\
|\ f(x_{1},\dots,x_{m},\omega)=y\\}).$

Lemma 4 states that such $f^{\\#}$ is arithmetical, i.e. there is an
$\mathsf{MQPA}$ formula $F_{f^{\\#}}$, such that for every
$n_{1},\dots,n_{m},l$,

$\mu_{\mathscr{C}}\big{(}\llbracket
F_{f^{\\#}}(n_{1},\dots,n_{m},l)\rrbracket\big{)}=f^{\\#}(n_{1},\dots,n_{m})(l).$

The proof of the Lemma is by induction on the structure of oracle recursive
functions. Actually, the only case which is worth-considering is the one of
_query_ functions. Indeed, all the other cases are obtained by trivial
generalizations of the standard proof by Gödel [23].

    * •

For each _basic_ oracle function, $f\in\mathcal{OR}$, the corresponding random
function, $f^{\\#}$, is arithmetical. There are four possible cases:

Oracle zero function. Let $f_{0}\in\mathcal{OR}$ be the oracle zero function.
For Definition 10, $f_{0}(x_{1},$ $\dots,x_{n},\omega)=y$, with $y=0$, is such
that the corresponding $f_{0}^{\\#}$ is defined by the $\mathsf{MQPA}$
formula,666Indeed, $f_{0}^{\\#}$ = $\mu_{\mathscr{C}}(\\{\omega\ |\
f(x_{1},\dots,x_{m},\omega)=0\\})=1$ and $F_{f_{0}^{\\#}}:y=\mathtt{0}$ and,
since $y=\mathtt{0}$ as $\llbracket y\rrbracket=0$ and
$\llbracket\mathtt{0}\rrbracket=0$, $\mu_{\mathscr{C}}(F_{f_{0}^{\\#}})=1$.

$F_{f_{0}^{\\#}}:y=\mathtt{0}.$

Oracle successor function. Let $f_{s}\in\mathcal{OR}$ be the successor
function. For Definition 10, $f_{s}(x,\omega)=y$, with $y$ = $x$+1, is such
that $f_{s}^{\\#}$ is defined by the $\mathsf{MQPA}$ formula,

$F_{f_{s}^{\\#}}:\mathtt{S}(x)=y.$

Oracle projection function. Let $f_{\pi_{i}}\in\mathcal{OR}$ be the projection
function Definition 10, $f_{\pi_{i}}(x_{1},$ $\dots,x_{k},\omega)=y$, with
$y=x_{i},$ be the is such that $f_{\pi_{i}}($ such that $f_{\pi_{i}}^{\\#}$ is
defined by the $\mathsf{MQPA}$ formula

$F_{\pi_{i}^{k}}:x_{i}=y.$

Oracle query function. Let $q\in\mathcal{OR}$ be the query function. For
Definition 10, $q(x,\omega)=\omega(x)$, is such that $f_{q}^{\\#}$ is defined
by the $\mathsf{MQPA}$ formula

$F_{q}:x=\mathsf{FLIP}(x).$

    * •

For each oracle function $f\in\mathcal{OR}$ obtained composition, primitive
recursion, or minimization from oracle recursive functions, whose
corresponding random functions are arithmetical, the corresponding random
function $f^{\\#}$ is arithmetical. The proofs for these three cases are very
similar to the standard ones. As an example, let us consider the case of
(simple) composition only.

Oracle (simple) composition. Let $f$ be obtained by composition from $h$ and
$g$, i.e. $f(x_{1},$ $\dots,x_{n},\omega)$ =
$h(g(x_{1},\dots,x_{n},\omega),\omega)$ = $v$. It is possible show that
$f^{\\#}(x_{1},\dots,x_{n})(v)$ is arithmetical, which is, for every
$x_{1},\dots,x_{n},v\in\mathbb{N}$, there is a $\mathsf{MQPA}$ formula,
$F_{f^{\\#}}(x_{1},\dots,x_{n},v)$, such that $\mu_{\mathscr{C}}(\llbracket
F_{f^{\\#}}(x_{1},\dots,x_{n},v)\rrbracket)$ = $f^{\\#}$. Indeed, the desired
formula is

$F_{f^{\\#}}=\exists v\big{(}F_{h^{\\#}}(v,y)\wedge
F_{g^{\\#}}(x_{1},\dots,x_{n},v)\big{)}$

where, by IH, $\mu_{\mathscr{C}}(\llbracket F_{h^{\\#}}\rrbracket)$ =
$h^{\\#}$ and $\mu_{\mathscr{C}}(\llbracket F_{g^{\\#}}\rrbracket)$ =
$g^{\\#}$.

$\Box$

As seen, since for both $\mathcal{OR}$ and $\mathsf{MQPA}$ the source of
randomness consists in a denumerable amount of random bits, the proof of Lemma
4 is easy, and follows the standard induction of [23]. Theorem 3 comes out as
a corollary of the Lemma 4 above, together with Proposition 1: any computable
random function is in $\mathcal{PR}$, by Proposition 1, and each
$\mathcal{PR}$ function is arithmetical, by Lemma 4 and Proposition 2. Indeed,
by Proposition 2, for any $f\in\mathcal{PR}$ there is a $g\in\mathcal{OR}$
such that $f=g^{\\#}$ and, since $g\in\mathcal{OR}$, by Lemma 4, $g^{\\#}$ (=
$f$) is arithmetical.

##  5 Realizability

In this section we sketch an extension of realizability, a well-known
computational interpretation of Peano Arithmetics, to $\mathsf{MQPA}$. The
theory of realizability [63, 24, 39, 61], which dates back to Kleene’s 1945
paper [36], provides a strong connection between logic, computability, and
programming language theory. The fundamental idea behind realizability is that
from every proof of an arithmetical formula in $\mathsf{HA}$ or equivalently
(via the Gödel-Gentzen translation) in $\mathsf{PA}$, one can extract a
program, called the _realizer_ of the formula, which encodes the computational
content of the proof. In Kreisel’s _modified-realizability_ [39] realizers are
typed programs: any formula $A$ of $\mathsf{HA}$ is associated with a type
$A^{*}$ and any proof of $A$ yields a realizer of type $A^{*}$.

Our goal is to show that the modified-realizability interpretation of
$\mathsf{HA}$ can be extended to the language $\mathsf{MQPA}$. As we have not
introduced a proof system for $\mathsf{MQPA}$ yet, we limit ourselves to
establishing the soundness of modified-realizability with respect to the
semantics of $\mathsf{MQPA}$. Similarly to what happens with the class
$\mathcal{OR}$, the fundamental intuition is that realizers correspond to
programs which can query an _oracle_ $\omega\in\mathbb{B}^{\mathbb{N}}$. For
instance, a realizer of $\mathbf{C}^{t/s}A$ is a program which, for a randomly
chosen oracle, yields a realizer of $A$ with probability at least $\llbracket
t\rrbracket_{\xi}/\llbracket s\rrbracket_{\xi}$.

Our starting point is a PCF-style language with oracles. The types of this
language are generated by basic types $\mathrm{nat},\mathrm{bool}$ and the
connectives $\to$ and $\times$. We let
$\mathrm{O}:=\mathrm{nat}\to\mathrm{bool}$ indicate the type of _oracles_. For
any type $\sigma$, we let $[\sigma]$ (resp. $[\sigma]_{\mathrm{O}}$) indicate
the set of closed terms of type $\sigma$ (resp. of terms of type $\sigma$ with
a unique free variable $o$ of type $\mathrm{O}$). Moreover, for all
$i\in\\{0,1\\}$ (resp. $n\in\mathbb{N}$), we indicate as $\overline{i}$ (resp.
$\overline{n}$) the associated normal form of type $\mathrm{bool}$ (resp.
$\mathrm{nat}$). For all term $M$ and normal form $N$, we let $M\Downarrow N$
indicate that $M$ converges to $N$. For any term $M\in[\sigma_{\mathrm{O}}]$
and oracle $\omega\in\mathbb{B}^{\mathbb{N}}$, we let $M^{\omega}\in[\sigma]$
indicate the closed program in which any call to the variable $o$ is answered
by the oracle $\omega$.

We consider the language of $\mathsf{MQPA}$ without negation and disjunction,
enriched with implication $A\to B$. As is usually done in modified-
realizability, we take $\lnot A$ and $A\lor B$ as _defined_ connectives, given
by $A\to(\mathtt{0}=\mathtt{S}(\mathtt{0}))$ and $\exists x.(x=\mathtt{0}\to
A)\land(x=\mathtt{S}(\mathtt{0})\to B)$, respectively. With any closed formula
$A$ of $\mathsf{MQPA}$ we associate a type $A^{*}$ defined as follows:
$\displaystyle\mathsf{FLIP}(t)^{*}$ $\displaystyle=\mathrm{nat}$
$\displaystyle(\forall x.A)^{*}$ $\displaystyle=\mathrm{nat}\to A^{*}$
$\displaystyle(t=u)^{*}$ $\displaystyle=\mathrm{bool}$ $\displaystyle(\exists
x.A)^{*}$ $\displaystyle=\mathrm{nat}\times A^{*}$ $\displaystyle(A\land
B)^{*}$ $\displaystyle=A^{*}\times B^{*}$
$\displaystyle(\mathbf{C}^{t/s}A)^{*}$
$\displaystyle=(\mathbf{D}^{t/s}A)^{*}=\mathrm{O}\to A^{*}$
$\displaystyle(A\to B)^{*}$ $\displaystyle=A^{*}\to B^{*}$

We define by induction the realizability relation $M,\omega\Vdash A$ where
$\omega\in\mathbb{B}^{\mathbb{N}}$ and, if $A=\mathbf{C}^{t/s}B$ or
$A=\mathbf{D}^{t/s}B$, $M\in[\sigma]$, and otherwise
$M\in[\sigma]_{\mathrm{O}}$.

  * 1.

$M,\omega\Vdash\mathsf{FLIP}(t)$ iff $\omega(\llbracket t\rrbracket)=1$;

  * 2.

$M,\omega\Vdash t=s$ iff $\llbracket t\rrbracket=\llbracket s\rrbracket$;

  * 3.

$M,\omega\Vdash A_{1}\land A_{2}$ iff $\pi_{1}(M),\omega\Vdash A_{1}$ and
$\pi_{2}(M),\omega\Vdash A_{2}$;

  * 4.

$M,\omega\Vdash A\to B$ iff $\omega\in\llbracket A\to B\rrbracket$ and
$P,\omega\Vdash A$ implies $MP,\omega\Vdash B$;

  * 5.

$M,\omega\Vdash\exists x.A$ iff $\pi_{1}(M^{\omega})\Downarrow\overline{k}$
and $\pi_{2}(M),\omega\Vdash A(k/x)$;

  * 6.

$M,\omega\Vdash\forall x.A$ iff for all $k\in\mathbb{N}$,
$M\overline{k},\omega\Vdash A(k/x)$;

  * 7.

$M,\omega\Vdash\mathbf{C}^{t/s}A$ iff $\llbracket s\rrbracket>0$ and
$\mu_{\mathscr{C}}\left(\\{\omega^{\prime}\mid Mo,\omega^{\prime}\Vdash
A\\}\right)\geq{\llbracket t\rrbracket}/{\llbracket s\rrbracket}$;

  * 8.

$M,\omega\Vdash\mathbf{D}^{t/s}A$ iff
$\omega\in\llbracket\mathbf{D}^{t/s}A\rrbracket$, and $\llbracket
s\rrbracket=0$ or $\mu_{\mathscr{C}}\left(\\{\omega^{\prime}\mid
Mo,\omega^{\prime}\Vdash A\\}\right)<{\llbracket t\rrbracket}/{\llbracket
s\rrbracket}$.

Condition 7. is justified by the fact that for all term $M$ and formula $A$,
the set $\\{\omega\mid M,\omega\Vdash A\\}$ can be shown to be measurable.
Conditions 5. and 9. include a semantic condition of the form
$\omega\in\llbracket A\rrbracket$, which has no computational meaning. This
condition is added in view of Theorem 4 below. In fact, also in standard
realizability a similar semantic condition for implication is required to show
that realizable formulas are true in the standard model, see [63].

###### Lemma 5

For each term $M\in[\sigma]_{\mathrm{O}}$ and normal form $N\in[\sigma]$, the
set $S_{M,N}$ of oracles $\omega$ such that $M^{\omega}\Downarrow N$ is
measurable.

  * Proof.

Let $\widehat{M}=\\{M^{\omega}\mid\omega\in\mathbb{B}^{\mathbb{N}}\\}$. Let
$r$ be a reduction from some $P=M^{\omega}\in\widehat{M}$ to $N$; since $r$ is
finite, it can only query finitely many values $b_{1},\dots,b_{n_{q}}$ of
$\omega$. Let $C_{r}$ be the cylinder of all sequences which agree with
$\omega$ at $b_{1},\dots,b_{n_{q}}$. It is clear that for all
$\omega^{\prime}\in C_{r}$, $M^{\omega^{\prime}}$ reduces to $N$. We have then
that $S_{M,N}=\bigcup\\{C_{r}\mid\exists P\in\widehat{M}\text{ and }r\text{ is
a reduction from }P\text{ to }N\\}$, so $S_{M,N}$ is a countable union of
measurable sets, and it is thus measurable. $\Box$

###### Lemma 6

For each term $M$ and closed formula $A$, the set $S_{M,A}=\\{\omega\mid
M,\omega\vDash A\\}$ is measurable.

  * Proof.

By induction on the structure of $A$:

    * 1.

if $A=\mathsf{FLIP}(t)$, then $S_{M,A}$ is the cylinder of all $\omega$ such
that $\omega(\llbracket t\rrbracket)=1$;

    * 2.

if $A=t=s$, then $S_{M,A}=\begin{cases}\mathbb{B}^{\mathbb{N}}&\text{ if
}\llbracket t\rrbracket=\llbracket s\rrbracket\\\ \emptyset&\text{
otherwise;}\end{cases}$

    * 3.

if $A=A_{1}\land A_{2}$, then $S_{M,A}=S_{\pi_{1}(M),A_{1}}\cap
S_{\pi_{2}(M),A_{2}}$;

    * 4.

if $A=B\to C$, then $S_{M,A}=\bigcap_{P\in[B^{*}]_{\mathrm{O}}}(S_{P,B}\cap
S_{MP,C})$;

    * 5.

if $A=\exists x.B$, then $S_{M,A}=\bigcup_{k}(S_{\pi_{1}(M),\overline{k}}\cap
S_{\pi_{2}(M),A(k/x)})$;

    * 6.

if $A=\forall x.B$, then $S_{M,A}=\bigcap_{k}S_{M\overline{k},A(k/x)}$;

    * 7.

if $A=\mathbf{C}^{t/s}B$, then
$S_{M,A}=\begin{cases}\mathbb{B}^{\mathbb{N}}&\text{ if }\llbracket
s\rrbracket>0\text{ and }\mu_{\mathscr{C}}(S_{Mo,B})\geq\llbracket
t\rrbracket/\llbracket s\rrbracket\\\ \emptyset&\text{ otherwise;}\end{cases}$

    * 8.

if $A=\mathbf{D}^{t/s}B$, then
$S_{M,A}=\begin{cases}\mathbb{B}^{\mathbb{N}}&\text{ if }\llbracket
s\rrbracket=0\text{ or }\mu_{\mathscr{C}}(S_{Mo,B})<\llbracket
t\rrbracket/\llbracket s\rrbracket\\\ \emptyset&\text{ otherwise.}\end{cases}$

$\Box$

######  Theorem 4 (Soundness)

For a closed formula $A$, if $M,\omega\Vdash A$, then $\omega\in\llbracket
A\rrbracket$.

  * Proof.

By induction on $A$:

    * 1.

if $A=\mathsf{FLIP}(t)$ and $M,\omega\Vdash A$, then $\omega(\llbracket
t\rrbracket)=1$, so $\omega\in\llbracket\mathsf{FLIP}(t)\rrbracket$;

    * 2.

if $A=t=s$ and $M,\omega\Vdash A$, then $\llbracket t\rrbracket=\llbracket
s\rrbracket$, so $\omega\in\mathbb{B}^{\mathbb{N}}=\llbracket A\rrbracket$;

    * 3.

if $A=A_{1}\land A_{2}$ and $M,\omega\Vdash A$, then from
$\pi_{1}(M),\omega\vDash A_{1}$ and $\pi_{2}(M),\omega\vdash A_{2}$ we deduce
$\omega\in\llbracket A_{1}\rrbracket\cap\llbracket A_{2}\rrbracket=\llbracket
A\rrbracket$;

    * 4.

if $A=B\to C$ and $M,\omega\Vdash A$, then by definition $\omega\in\llbracket
A\rrbracket$;

    * 5.

if $A=\exists x.B$ and $M,\omega\Vdash A$ then
$\pi_{1}(M^{\omega})\Downarrow\overline{k}$ and $\pi_{2}(M),\omega\Vdash
B(k/x)$, so by IH $\omega\in\llbracket B(k/x)\rrbracket\subseteq\llbracket
A\rrbracket$;

    * 6.

if $A=\forall x.B$ and $M,\omega\Vdash A$ then for all $k\in\mathbb{N}$,
$M\overline{k},\omega\Vdash A(k/x)$, so by IH $\omega\in\llbracket
A(k/x)\rrbracket$ and we conclude $\omega\in\llbracket
A\rrbracket=\bigcap_{k}\llbracket A(k/x)\rrbracket$;

    * 7.

if $A=\mathbf{C}^{t/s}B$ and $M,\omega\Vdash A$ then $\llbracket
s\rrbracket>0$ and $\mu_{\mathscr{C}}(S)\geq\llbracket t\rrbracket/\llbracket
s\rrbracket$, where $S=\\{\omega^{\prime}\mid Mo,\omega^{\prime}\Vdash B\\}$.
Then, by IH $S\subseteq\llbracket B\rrbracket$, hence
$\mu_{\mathscr{C}}(\llbracket
B\rrbracket)\geq\mu_{\mathscr{C}}(S)\geq\llbracket t\rrbracket/\llbracket
s\rrbracket$. We conclude then that $\llbracket
A\rrbracket=\mathbb{B}^{\mathbb{N}}$ and thus $\omega\in\llbracket
A\rrbracket$;

    * 8.

if $A=\mathbf{D}^{t/s}B$ and $M,\omega\Vdash A$ then by definition
$\omega\in\llbracket\mathbf{D}^{t/s}B\rrbracket$.

$\Box$

For example, the term $M=\lambda o.\mathrm{fix}\big{(}\lambda
fx.(\mathrm{iszero}(ox))(f(x+1))\langle x,x\rangle\big{)}\overline{0}$
realizes the valid formula $\mathbf{C}^{1/1}\exists x.\mathsf{FLIP}(x)$. $M$
looks for the first value $k$ such that $o(k)=1$ and returns the pair
$\langle\overline{k},\overline{k}\rangle$. Similarly, the program $\lambda
xoyz.o(y)$, which checks whether the $y$-th bit of $\omega$ is true, realizes
the formula $\forall x.\mathbf{C}^{1/2^{x}}\forall_{y\leq x}\mathsf{FLIP}(y)$.
With the same intuition, one can imagine how a realizer $M$ of the formula
$F_{\mathtt{IMT}}$ can be constructed: given inputs $x,o,y$, $M$ looks for the
first $k$ such that the finite sequence
$o(y+k),o(y+k+1),\dots,o(y+k+{\ell(n))}$ coincides with the string coded by
$x$ (where this last check can be encoded by a program $\lambda
w.P(x,o,y,z,w)$), and returns the pair $\langle\overline{k},\lambda
w.P(x,0,y,\overline{k},w)\rangle$.

##  6 Related Works

To the best of the authors’ knowledge, the term “measure quantifier” was first
introduced by Morgenstern in 1979 in order to formalize the idea that a
formula $F(x)$ is true _for almost all x_ [45].777 Morgenstern’s definition
was inspired by the notion of generalized quantifier, which was “introduced to
specify that a given formula was true for “many $x$’s”” [45, p. 103].
Morgenstern defined a language $L_{\mu}$, obtained by adding the measure
quantifier $Q_{\mu}$ to the standard first-order grammar and presented the the
central notions of his logic as follows (actually, other extended languages
are considered in [45]):  Definition 2.1 A _measure structure_ $\mathcal{U}$
is a pair $\mathcal{U}=(\mathcal{U},\mu^{\mathcal{U}})$, where
$\mathcal{U}^{\prime}$ is a first-order structure, card$|\mathcal{U}|=k$, a
measurable cardinal, and $\mu^{\mathcal{U}}$ is a nontrivial $k$-additive
measure on $|\mathcal{U^{\prime}}|$ which satisfies the partition property.
[…] Definition 2.2 Define a language $L_{\mu}$ to be a first-order language
together with a quantifier $Q_{\mu}$, binding one free variable, where a
measure $\mathcal{U}\vDash Q_{\mu}v_{0}\varphi(v_{0})$ iff
$\\{x\in|\mathcal{U}|\ |\
\mathcal{U^{\prime}}\vDash\varphi[x]\\}\in\mu^{\mathcal{U}}$. [45, pp.
103-104] In the same years, similar quantifiers were investigated from a
model-theoretic perspective by H. Friedman (see [62] for a survey). More
recently, Mio et al. [43, 44] investigated the possibility for such
quantifiers to define extensions of MSO. Generally speaking, all these works
have been strongly inspired by the notion of generalized quantifiers, which
already appeared in a seminal work by Mostowski [46].888 Specifically,
generalized quantifiers were first introduced by Mostowski, as “operators
which represent a natural generalization of the logical quantifiers” [46, p.
13] and have then been extensively studied in the context of finite-model
theory [42, 37]. Second-order generalized quantifiers have been recently
defined as well [1]. Nevertheless, the main source of inspiration for our
treatment of measure quantifiers comes from computational complexity, namely
from Wagner’s counting operators on classes of languages [65, 66, 67].999For
further details, see [2], where the model theory and proof theory of an
extension of propositional logic with counting quantifiers is studied (in
particular, the logic $\mathsf{CPL}_{0}$ can be seen as a “finitary” fragment
of $\mathsf{MQPA}$).

On the other hand, there is an extensive amount of publications dealing with
different forms of probabilistic reasoning (without references to arithmetic).
Most of the recent probability systems have been developed in the realm of
modal logic, starting with the seminal (propositional) work by Nilsson [47].
From the 1990s on, first-order probability logic and (axiomatic) proof
systems, have been independently introduced by Bacchus [6, 4, 5] and Fagin,
Halpern and Megiddo [19, 18, 27, 28]. Remarkably, Bacchus defined _probability
terms_ , by means of a modal operator $\mathsf{prob}$ computing the
probability of certain events, and _probability formulas_ , which are
equalities between probability terms and numbers. A similar first-order
probability logic was introduced by Fagin, Halpern and Megiddo [19] (and later
studied in [18, 27, 28]), in which probability spaces define the underlying
models, and can be accessed through the so-called weight terms. Another class
of probabilistic modal logics have been designed to model Markov chains and
similar structure, for example in [38, 29, 41, 20]. However, once again, no
reference to arithmetic is present in these works.

From the 1950s on, the interest for probabilistic algorithms and models
started spreading [40, 14, 9, 49, 51, 21, 56]. Nowadays, random computation is
pervasive in many area of computer science and, several formal models are
available, such as probabilistic automata [55], both Markovian and oracle
probabilistic Turing machines [53, 54, 21, 22], and probabilistic
$\lambda$-calculi [50, 31, 15, 12, 17]. As seen, also a well-defined
probabilistic recursion theory has been developed by [11, 13]. Our definition
of the class $\mathcal{OR}$ is guided by both by recent $\mathcal{PR}$ [11,
13] and by classical recursion theory [23, 10, 32, 33, 34, 35, 64,
48].101010For further details on the history of the notion of recursion, see
[60]. Our definition of random arithmetical formulas and Theorem 3 generalize
the original results by Gödel [26, pp. 63–65]. Also our study of realizability
is inspired by classical works. The functional or D-interpretation was first
introduced by Gödel in 1958 in order to prove the consistency of arithmetic
[24].111111Actually, Gödel started conceiving the D-interpretation in the late
1930s [60, 3]. The theory was further developed by Kreisel, who introduced the
notion of modified-realizability [39], starting from Kleene’s realizability
[36].

##  7 Conclusion

This paper can be seen as “a first exploration” of $\mathsf{MQPA}$, providing
some preliminary results, but also leaving many problems and challenges open.
The most compelling one is certainly that of defining a proof system for
$\mathsf{MQPA}$, perhaps inspired from realizability. Furthermore, our
extension of $\mathsf{PA}$ is _minimal_ by design. In particular, we confined
our presentation to a unique predicate variable, $\mathsf{FLIP}(x)$. Yet, it
is possible to consider a more general language with countably many predicate
variables $\mathsf{FLIP}_{a}(x)$, and suitably-_named_ quantifiers
$\mathbf{C}^{t/s}_{a}$ and $\mathbf{D}^{t/s}_{a}$ (as in [2]). We leave the
exploration of this more sophisticated syntax to future work. Another
intriguing line of work concerns the study of bounded versions of
$\mathsf{MQPA}$, which may suggest novel ways of capturing probabilistic
complexity classes, different from those in the literature, e.g. [30].

## References

  * [1] Andersson, A.: On second-order generalized quantifiers and finite structures. Annals of Pure and Applied Logic 115(1–3), 1–32 (2002)
  * [2] Antonelli, M., Dal Lago, U., Pistone, P.: On counting propositional logic (2021), available from: https://arxiv.org/abs/2103.12862
  * [3] Avigad, J., Feferman, S.: Gödel’s functional (“Dialectica”) interpretation. In: Buss, S. (ed.) Handbook of Proof Theory, vol. 137, pp. 337–405. Elsavier Science (1998)
  * [4] Bacchus, F.: On probability distributions over possible worlds. Machine Intelligence and Pattern Recognition 9, 217–226 (1990)
  * [5] Bacchus, F.: Representing and Reasoning with Probabilistic Knowledge. MIT Press (1990)
  * [6] Bacchus, F.: Lp, a logic for representing and reasoning with statistical knowledge. Comput. Intell. 6(4), 209–231 (1990)
  * [7] Billingsley, P.: Probability and Measure. Wiley (1995)
  * [8] Buss, S.: Bounded Arithmetic. Ph.D. thesis, Princeton University (1986)
  * [9] Carlyle, J.: Reduced forms for stochastic sequential machines. J. Math. Anal. Appl. 7, 167–174 (1963)
  * [10] Church, A., Kleene, S.: Formal definitions in the theory of ordinal numbers. Fund. Math. 28, 11–21 (1936)
  * [11] Dal Lago, U., Gabbrielli, M., Zuppiroli, S.: Probabilistic recursion theory and implicit computational complexity. Sci. Ann. Comput. Sci. 24(2), 177–216 (2014)
  * [12] Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO 46(3), 413–450 (2012)
  * [13] Dal Lago, U., Zuppiroli, S.: Probabilistic recursion theory and implicit computational complexity. In: ICTAC. Lecture Notes in Computer Science, vol. 8687, pp. 97–114 (2014)
  * [14] Davis, A.: Markov chains as random input automata. Am. Math. Mon. 68(3), 264–267 (1961)
  * [15] Di Pierro, A., Wiklicky, H.: Probabilistic lambda-caclulus and quantitative program analysis. J. Log. Comput. 15(2), 159–179 (2005)
  * [16] Du, D.Z., Ko, K.I.: Computational Complexity: A modern approach. Wiley (2000)
  * [17] Ethard, T., Pagani, M., Tasso, C.: The computational meaning of probabilistic coherence spaces. In: IEEE (ed.) LICS. pp. 87–96. Toronto, ON, Canada (2011)
  * [18] Fagin, R., Halpern, J.: Reasoning about knowledge and probability. J. of ACM 41(2), 340–367 (1994)
  * [19] Fagin, R., Halpern, J., Megiddo, N.: A logic for reasoning about probabilities. Inf. Comput. 87(1/2), 78–128 (1990)
  * [20] Furber, R., Mardare, R., Mio, M.: Probabilistic logics based on Riesz spaces. LMCS 16(1) (2020)
  * [21] Gill, J.: Computational complexity of probabilistic Turing machines. In: STOC. pp. 91–95. ACM (1974)
  * [22] Gill, J.: Computational complexity of probabilistic Turing machines. J. Comput. 6(4), 675–695 (1977)
  * [23] Gödel, K.: Über formal unentscheidbare sätze der _Principia Mathematica_ und verwandter systeme. Monatsch. Math. Phys. 38, 173–178 (1931)
  * [24] Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten standpunktes. Dialectica 12, 280–287 (1958)
  * [25] Gödel, K.: On undecidable propositions of formal mathematical systems. In: Davis, M. (ed.) The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Dover Publications (1965)
  * [26] Gödel, K.: On Formally Undecidable Propositions of _Principia Mathematica_ and Related Systems. Dover Publications (1992)
  * [27] Halpern, J.: An analysis of first-order logics for probability. Artif. Intell. 46(3), 311–350 (1990)
  * [28] Halpern, J.: Reasoning About Uncertainty. MIT Press (2003)
  * [29] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)
  * [30] Jerábek, E.: Approximate counting in bounded arithmetic. J. Symb. Log. 72(3), 959–993 (2007)
  * [31] Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: LICS. vol. 4, pp. 186–195. IEEE (1989)
  * [32] Kleene, S.: General recursive functions of natural numbers. Math. Ann. 112, 727–742 (1936)
  * [33] Kleene, S.: $\lambda$-definability and recursiveness. Duke Math. J. 2, 340–353 (1936)
  * [34] Kleene, S.: A note on recursive functions. Bul. of AMS 42, 544–546 (1936)
  * [35] Kleene, S.: Recursive predicates and quantifiers. Trans. of AMS 53, 41–73 (1943)
  * [36] Kleene, S.: On the interpretation of intuitionistic number theory. J. Symb. Log. 10(4), 109–124 (1945)
  * [37] Kontinen, J.: A logical characterization of the counting hierarchy. ACM 10(1) (2009)
  * [38] Kozen, D.: Semantics of probabilistic programs. JCSS 22(3), 328–350 (1981)
  * [39] Kreisel, G.: Gödel’s interpretation of Heyting’s arithmetic. In: Summaries of talks, Summer Institute for Symbolic Logic (1957)
  * [40] de Leeuw, e.a.: Computability by probabilistic machines. In: Press, P.U. (ed.) Automata Studies, pp. 183–212. No. 34, Shannon, C.E. and McCarthy, J. (1956)
  * [41] Lehmann, D., Shelah, S.: Reasoning with time and chance. Inf. Control 53(3), 165 – 198 (1982)
  * [42] Lindström, P.: First order predicate logic with generalized quantifiers. Theoria 32, 186–195 (1966)
  * [43] Michalewski, H., Mio, M.: Measure quantifiers in monadic second order logic. LFCS pp. 267–282 (2016)
  * [44] Mio, M., Skrzypczak, M., Michalewski, H.: Monadic second order logic with measure and category quantifiers. LMCS 8(2) (2012)
  * [45] Morgenstern, C.: The measure quantifier. J. Symb. Log. 44(1) (1979)
  * [46] Mostowski, A.: On a generalization of quantifiers. Fundamenta Mathematicae 44, 12–36 (1957)
  * [47] Nilsson, N.: Probabilistic logic. Artif. Intell. 28(1), 71–87 (1986)
  * [48] Peter, R.: Rekursive Funktionen. Akadémiai Kiadó (1951)
  * [49] Rabin, M.O.: Probabilistic automata. Inf. Comput. 6(3), 230–245 (1963)
  * [50] Saheb-Djaromi, N.: Probabilistic LCF. In: MFCS. pp. 442–452. No. 64 in
  * [51] Santos, E.: Maximin automata. Inf. Control 13, 363–377 (1968)
  * [52] Santos, E.: Maximin sequential-like machines and chains. Math. Syst. Theory 3(4), 300–309 (1969)
  * [53] Santos, E.: Probabilistic Turing machines and computability. AMS 22(3), 704–710 (1969)
  * [54] Santos, E.: Computability by probabilistic Turing machines. AMS 159, 165–184 (1971)
  * [55] Segala, R.: A compositional trace-based semantics for probabilistic automata. In: CONCUR. pp. 234–248 (1995)
  * [56] Simon, J.: On some central problems in computational complexity. Ph.D. thesis, Cornell University (1975)
  * [57] Simon, J.: On tape-bounded probabilistic Turing machine acceptors. TCS 16, 75–91 (1981)
  * [58] Simpson, S.: Subsystems of Second Order Arithmetic. Cambridge Press (2009)
  * [59] Smith, P.: An Introduction to Gödel’s Theorems. Cambridge University Press (2013)
  * [60] Soare, R.: Computability and recursion. Bull. Symb. Log. 2, 284–321 (1996)
  * [61] Sorensen, M., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier (2006)
  * [62] Steinhorn, C.I.: Borel Structures and Measure and Category Logics, vol. 8, pp. 579–596. Springer-Verlag (1985)
  * [63] Troelstra, A.: Realizability. In: Buss, S.R. (ed.) Handbook of Proof Theory, vol. 137, pp. 407–473. Elsevier (1998)
  * [64] Turing, A.: Computability and $\lambda$-definability. J. Symb. Log. 2, 153–163 (1937)
  * [65] Wagner, K.: Compact descriptions and the counting polynomial-time hierarchy. In: Frege Conference 1984. pp. 383–392 (1984)
  * [66] Wagner, K.: The complexity of combinatorial problems with succinct input representation. Acta Informatica 23, 325–356 (1986)
  * [67] Wagner, K.: Some observations on the connection between counting and recursion. TCS 47, 131–147 (1986)