The predicate logic of a theory T is defined as the set of all predicate formulas that are provable in T under all substituitions of T-formulas for predicate letters (of the same arity). It is like the predicate provability logic without the provability operator.
By Hilbert and Bernays, the predicate logic of Peano Arithmetic coincides with the standard first order predicate logic. The predicate logic of HA coincides with the intuitionistic predicate logic by an equally well-known theorem of De Jongh. The question is open for some standard extensions of HA: HA+MP (Markov's principle); HA+ECT0 (Church's thesis).
These problems are related to the famous open question about the logic of Kleene realizability and the results of Plisko. In particular, Plisko established that the predicate logic of HA+MP+ECT0 is Pi_2^0-complete, hence not axiomatizable. See
V.E.Plisko. On arithmetic complexity of certain constructive logics. Math. Notes, 1993, 701-709. (Russian original in Mat.Zametki, 52 (1992), 94-104.)
Troelstra's theorem states that a formula A is provable in HA+ECT0 iff its realizability translation Ar is provable in HA. A similar result holds with HA+MP instead of HA. Thus, the predicate logic of HA+ECT0 is precisely the set of all predicate formulas whose realizability translations for every substitution are HA-provable. Similarly, for HA+MP in place of HA. Another important result of Plisko states that the set of all predicate realizable formulas that are true under every substitution is Pi_1^1-complete.
It is unknown, if the set of all propositional formulas that are Kleene realizable under every substitution is axiomatizable. It is known that it strictly contains intuitionistic propositional logic Int. A similar question about the HA-provably realizable formulas is also open. It is known, however, that the propositional logics of HA+MP and HA+ECT0 coincide with Int, whereas the logic of HA+MP+ECT0 strictly contains Int. For further details and references see
A. Visser. Rules and arithmetics. Department of Philosophy, Utrecht University, Logic Group Preprint Series 186, June 1998.