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.