If we extend $\sf PA$ with the following axiom asserting its own inconsistency:
Inconsistency: $\exists x: \operatorname {Proof}_{\sf PA} (x, \ulcorner 0=1 \urcorner)$
For short denote this axiom by $\mathbb I$.
Now, from this we get the explosion phenomena where every sentence in the language of $\sf PA$ is internally provable, so we do have:
$({\sf PA + \mathbb I}) \vdash (\forall s \exists x : \operatorname {Proof}_{\sf PA} (x,\ulcorner s \urcorner))$
Now, that $\sf PA + \mathbb I.$ is consistent (metatheoretically), is a corollary of Gödel's second incompleteness theorem.
Lets define the notion of strong provability of a sentence as having a code of its proof that is strictly smaller than every code of a proof of its negation. That is,
$s \text { is strongly provable in } T \iff\\ \exists x: \operatorname {Proof}_T (x,\ulcorner s \urcorner) \land \forall y \, ( \operatorname {Proof}_T(y,\operatorname {neg}(\ulcorner s \urcorner)) \to x < y )$
Now, $\sf PA + \mathbb I$ proves that for any sentence $s$ either it or its negation is strongly provable in $\sf PA$. For the standard theorems of $\sf PA$, those would be coded by standard naturals and so would be strongly provable and their negation would have non-standard codes. Now working in $\sf PA + \mathbb I$ take the set $\sf SPv$ of all sentences that $\sf PA + \mathbb I$ proves them to be strongly provable sentences in $\sf PA$. Now $\sf SPv$ is syntactically consistent, i.e. it doesn't contain both a sentence and its negation among its elements, also $\sf SPv$ is complete, since it decides on every sentence. But, the problem is that it is not theoretically consistent, i.e. sentences derived from them by applications of modus ponens may be contradictory (as in the case of the Rosser's sentence, which would prove its negation)
Now, if we work in the opposite theory that is $\sf PA + \neg \mathbb I$, and define proof notions with respect to that theory, then here we don't have the inflation we had with $\sf PA + \mathbb I$.
Here, I'm concerned about the sentences $\sf PA+\mathbb I$ proves them to be strongly provable sentences in $\sf PA$, that are undecidable in $\sf PA + \neg \mathbb I$. Such sentences to be called remotely strongly provable For example the Godel sentence if $\sf PA + \mathbb I$ proves it to be strongly provable in $\sf PA$, then it would be a remotely strongly provable sentence.
The idea is to work within $\sf PA + \mathbb I$ and define $\sf PA + \neg \mathbb I$ proofs (denoted by $\operatorname {Proof}_{\sf PA+\neg \mathbb I}$) by imposing syntactical restrictions on proofs in $\sf PA +\mathbb I$ as to bar them from including the sentence $\mathbb I$ in their definition, and only depend on $\sf PA + \neg \mathbb I$ as starters of proofs.
Define: $(T \vdash^* s)$ if and only if $s$ is proved by $\sf PA + \mathbb I$ to be strongly provable in $\sf PA $, and yet undecidable in $\sf PA + \neg \mathbb I$. Formally:
$(T\vdash^* s) \iff \\ s \text{ is strongly provable in } {\sf PA} \land \\ \neg \exists x : \operatorname {Proof}_{\sf PA + \mathbb I} (x,\ulcorner s \urcorner) \land \\ \neg \exists x : \operatorname {Proof}_{\sf PA + \mathbb I} (x,\operatorname {neg} (\ulcorner s \urcorner))$
Now, the question:
Can we have an effectively generated set $A$ of remotely strongly provable sentences in $\sf PA + \mathbb I$ that can capture all remote strongly provable sentences via repeated applications of Remote Modus Ponens starting from sentences in $A$.
Remote Modus Ponens: $ T \vdash^* a \\ \underline {T \vdash^*(a \to b) } \\ T \vdash^* b$
