There was a recent question on Artemov's paper here on MO https://mathoverflow.net/questions/469247/situation-with-artemovs-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$?