Por Trifon Trifonov (Sofia University).

Gödel's functional (Dialectica) interpretation is a powerful tool for obtaining computations from proofs involving non-constructive principles. Practical uses necessitate control mechanisms for the complexity of the extracted terms.

We show how Dialectica can be soundly adapted to interpret a non-standard modal arithmetic extending system T and S4 into classical finite type arithmetic. The modalities act as erasers of irrelevant code "en masse", complementary to the finer mechanism of light quantifiers providing erasure of individual variables. The realizability of the defining axiom of the classical modal system S5 is shown to be equivalent to the Drinker's Paradox.

This is joint research with Dan Hernest.

Transmissão via Zoom.