A herbrandized functional interpretation
Fernando Ferreira
CMAF-CIO, Universidade de Lisboa
Abstract: We introduce and study a functional interpretation that accumulates existential witnesses into finite sets. This semi-intuitionistic interpretation is able to realize the principles LLPO, WKL and the so-called FAN theorem.
[This seminar is partly a repetition of material given in the first four SLM seminars of this year.]