[The question has been edited]


Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:


$T + \\ \forall \mathcal S \, [\exists x: \operatorname {Proof}\_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}\_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$


is consistent?


Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.


In other words, can $T$ be consistently extended by its own completeness and consistency?



Can there be an effectively generated consistent theory that extends PA and be consistently extended by its own completeness and consistency?
The answer to the edited question is No, there is no such theory $T$, because the incompleteness theorem is provable in PA and hence also in $T$. The theory $T$ will prove that there is no effective complete consistent theory of arithmetic, and in particular, $T$ will prove that $T$ itself (as defined by its effective algorithm) cannot have the property of your exclusive disjunction clause.


