theorem LO.FirstOrder.Arith.re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P

theorem LO.FirstOrder.Arith.goedel_first_incompleteness (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐑₀ ≼ T] [LO.FirstOrder.Arith.Sigma1Sound T] [T.Delta1Definable] : ¬LO.System.Complete T

Gödel's First Incompleteness Theorem