In 1958 Gödel introduced the Dialectica interpretation [4] to prove the (relative) consistency of intuitionistic arithmetic and, over …