This continues my question here.
I think the following versions of Gödel's incompleteness theorems must be true, but I can't find references. I would be happy if specialists could help.
To give accurate formulations I need the following definition which is a modification of Shoenfield's construction of interpretation of a theory in another theory [Shoenfield, 4.7].
Let $S$ and $T$ be formal theories over the predicate logic. Let us say that $S$ has an interpretation in $T$, if
the alphabet of $T$ contains the alphabet of $S$,
to each propositional symbol $p$ in the signature of $S$ we assigned an extended propositional symbol $p'$ (of the same arity) in $T$ in the sense of [Kunen,II.15.1]
to each functional symbol $f$ in the signature of $S$ we assigned an extended functional symbol $f'$ (of the same arity) in $T$, again in the sense of [Kunen,II.15.1]
in the arising correspondence between formulas $\varphi\mapsto\varphi'$ each axiom $\varphi$ in $S$ turns into a theorem $\varphi'$ in the theory $S'$ that appears as an extension by definitions of $T$.
The versions of Gödel's theorems I am interested in are the following:
Theorem 1. Suppose $T$ is a consistent theory where the Peano arithmetic has an interpretation. Then $T$ is incomplete.
Theorem 2. Suppose $T$ is a consistent theory where the Peano arithmetic has an interpretation. Then the proposition that $T$ is consistent is not deducible in $T$.
Is this correct?
If yes, where is it written?
If no, then perhaps it is possible to modify the formulations so that they become true?