There was a recent question on Artemov's paper here on MO Situation with Artemov's paper?

In one of the answers there it was asserted (apparently incorrectly - see Noah Schweber's comments and answer) that the main mathematical claim of the paper is (where PA is 1st-order Peano Arithmetic):

1. for each $n$, PA proves the statement “$n$ does not code a proof of $\bot$ in PA” (which we abbreviate as “$\lnot (n \colon \bot)$”)
2. moreover, there is a primitive recursive function taking each $n$ to the PA-proof of “$\lnot (n \colon \bot)$”

My question is, are there any systems $T$ stronger than PA such that

1. for each $n$, PA proves the statement “$n$ does not code a proof of $\bot$ in $T$” (which we abbreviate as “$\lnot_T (n \colon \bot)$”)
2. moreover, there is a primitive recursive function taking each $n$ to the PA-proof of “$\lnot_T (n \colon \bot)$”

If so, can one give a characterisation of such $T$?