On Measure Quantifiers in First-Order Arithmetic

Melissa Antonelli (1) , Ugo Dal Lago (1) , Paolo Pistone (1)

1 FOCUS - Foundations of Component-based Ubiquitous Systems

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.

Mots clés: Probabilistic computation; Peano; Arithmetic; Realizability

Domaines: Logique en informatique [cs.LO]

Melissa Antonelli, Ugo Dal Lago, Paolo Pistone. On Measure Quantifiers in First-Order Arithmetic. Proceedings of CIE 2021, pp.12-24, 2021, ⟨10.1007/978-3-030-80049-9_2⟩. ⟨hal-03346804⟩