$\Delta_1$-definability of theories

𝗜𝚺₁ and 𝗣𝗔 are $\Delta_1$-definable; the proofs are in Foundation.FirstOrder.Incompleteness.InductionSchemeDelta1 (instances ISigma1_delta1Definable, PA_delta1Definable).

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatUnionCon : 𝗜𝚺₁ ⪱ 𝗜𝚺₁ ∪ Theory.Con 𝗜𝚺₁

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionISigmaOfNatNatConFirstOrderTrueArith : 𝗜𝚺₁ ∪ Theory.Con 𝗜𝚺₁ ⪱ 𝗧𝗔

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatUnionIncon : 𝗜𝚺₁ ⪱ 𝗜𝚺₁ ∪ Theory.Incon 𝗜𝚺₁

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryPeanoUnionCon : 𝗣𝗔 ⪱ 𝗣𝗔 ∪ Theory.Con 𝗣𝗔

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionPeanoConFirstOrderTrueArith : 𝗣𝗔 ∪ Theory.Con 𝗣𝗔 ⪱ 𝗧𝗔

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryPeanoUnionIncon : 𝗣𝗔 ⪱ 𝗣𝗔 ∪ Theory.Incon 𝗣𝗔

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionPeanoConIncon : 𝗣𝗔 ∪ Theory.Con 𝗣𝗔 ⪱ 𝗣𝗔 ∪ Theory.Con 𝗣𝗔 ∪ Theory.Incon (𝗣𝗔 ∪ Theory.Con 𝗣𝗔)