Interactive Realizers and Monads

TL;DR

This paper introduces an interactive realizability interpretation of a quantifier-free arithmetic system, modeling classical proofs as learning strategies through monads, bridging logic and category theory.

Contribution

It presents a novel categorical framework using monads to interpret classical proofs as interactive learning processes in a quantifier-free arithmetic setting.

Findings

Interpretation of classical proofs as interactive learning strategies

Construction of two monads for categorical presentation

Application to EM1-arithmetic fragment

Abstract

We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without "nested" quantifiers, called here EM1-arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the "environment" and with each other. We give a categorical presentation of the interpretation through the construction of two suitable monads.