[FOM] PA Completeness

[Jan Pax]

I react to the CONJECTURE in http://cs.nyu.edu/pipermail/fom/2006-October/011044.html

"CONJECTURE. Every true sentence in 0,S,+,dot with at most two variables and
term complexity at most 2, is provable in PA (and even in EFA). Every
instance of every universally true scheme in 0,S,+,dot and the unary
schematic letter R, with at most two variables and term complexity at most
2, is provable in PA.

Why 2,2? Because 2,2 is sufficient to axiomatize PA."

with question

Which standard theories T in f.o.m. do have the property that
n,k is sufficient to axiomatize T, but some true sentence of T
with at most n variables and term complexity at most k is unprovable in T?
The CONJECTURE just says that PA is not such a theory.

And, is there a connection between the interpretability of a theory S in T and the above property?

Thank you, JP