Interactive Realizers and Monads

Stefano Berardi, Ugo de'Liguoro

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.

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment