On Measure Quantifiers in First-Order Arithmetic (Long Version)

TL;DR

This paper explores an extension of first-order arithmetic with measure quantifiers, enabling the formalization of probability concepts and recursive random functions, and introduces a realizability interpretation involving oracles from the Cantor space.

Contribution

It introduces measure quantifiers into first-order arithmetic, allowing for probabilistic reasoning and representation of recursive random functions, along with a realizability interpretation involving Cantor space oracles.

Findings

First-order arithmetic with measure quantifiers can formalize basic probability results.

It can represent all recursive random functions.

A realizability interpretation with Cantor space oracles is developed.

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.