Randomising Realisability

TL;DR

This paper introduces a randomized version of Kleene's realisability for intuitionistic arithmetic, exploring its logical properties and differences from classical realisability, including the behavior of axioms and induction schemes.

Contribution

It defines a new probabilistic realisability framework and analyzes its logical closure, axiomatic validity, and differences from standard realisability.

Findings

Realisability with probability 1 equals standard realisability.

The set of randomly realisable statements is closed under intuitionistic logic.

Some instances of the induction scheme are not randomly realisable.

Abstract

We consider a randomised version of Kleene's realisability interpretation of intuitionistic arithmetic in which computability is replaced with randomised computability with positive probability. In particular, we show that (i) the set of randomly realisable statements is closed under intuitionistic first-order logic, but (ii) different from the set of realisable statements, that (iii) "realisability with probability 1" is the same as realisability and (iv) that the axioms of bounded Heyting's arithmetic are randomly realisable, but some instances of the full induction scheme fail to be randomly realisable.