[Written together with A. Visser]

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+ECT_{0} (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+ECT_{0} 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 inMat.Zametki, 52 (1992), 94-104.)

Troelstra's theorem states
that a formula A is provable in HA+ECT_{0} iff
its realizability translation A^{r} is provable in HA.
A similar result holds with HA+MP instead of HA.
Thus, the predicate logic of
HA+ECT_{0} 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+ECT_{0} coincide with **Int**,
whereas the logic of HA+MP+ECT_{0} 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.