The propositional logic of a formal theory U is defined as the set of all propositional formulas A such that f(A) is provable in U, for every substitution f of formulas of U for propositional variables in A. Let T be Gödel's system of finite type functionals. The well-known Dialectica interpretation provides a translation of Heyting arithmetic HA into T. What is the propositional logic of T? Similar questions can be asked about any particular model of T, say HRO.