Por Paulo Firmino (University of Lisbon).

We define two functional interpretations on intuitionistic logic over finite types with the introduction of star types representing finite non-empty sets. The characteristic principles of the first (the semi-intuitionistic case) are variations of known principles, such as a form of choice, independence of premises and the lesser limited principle of omniscience, which take into account the star type. The second (the intuitionistic case) involves the standard principles of choice and independence of premises and requires a variation of Markov’s principle. We give Soundness and Characterization results, as well as corolaries regarding term extraction.

Transmissão via Zoom.