Completeness for $T$ $\iff$ (Ω-consistent $\Rightarrow$ Ω-satisfiable)

Open

OmegaLogic.completeness_iff_consistent_imp_satisfiable

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

forcinglarge-cardinalsomega-logicset-theory

Fact 3.9 (primer). For every set of sentences $T$ , the following are equivalent:

for every sentence $\varphi$ , $T \models_\Omega \varphi$ implies $T \vdash_\Omega \varphi$ ;
if $T$ is Ω-consistent ( $T \nvdash_\Omega \bot$ ), then $T$ is Ω-satisfiable (some $V^B_\alpha \models T$ ).

\Big(\forall \varphi,\ T \models_\Omega \varphi \Rightarrow T \vdash_\Omega \varphi\Big) \iff \Big(T \text{ Ω-consistent} \Rightarrow T \text{ Ω-satisfiable}\Big).

No large-cardinal hypothesis is assumed. The primer gives this as a restatement of the Ω-conjecture: completeness for a fixed theory is equivalent to the model-existence form.

Preamble

import Definitions.Def_OmegaLogic_Provability
import Definitions.Def_OmegaLogic_LargeCardinals

universe u

Formal statement

namespace OmegaLogic

theorem completeness_iff_consistent_imp_satisfiable (T : Set Sent) :
    (∀ φ : Sent, OmegaValid.{u} T φ → OmegaProvable.{u} T φ) ↔
      (OmegaConsistent.{u} T → OmegaSatisfiable.{u} T) := by sorry

end OmegaLogic

Source

J. Bagaria, N. Castells, P. Larson, "An Ω-logic primer", in Set Theory (Trends in Mathematics), Birkhäuser 2006, pp. 1–28, doi:10.1007/3-7643-7692-9_1; online version https://paulblarson.github.io/omegalogicmaster5.pdf, Fact 3.9, pp. 24–25.

View graph

Completeness for TTT ⟺ \iff⟺ (Ω-consistent ⇒\Rightarrow⇒ Ω-satisfiable)

Completeness for $T$ $\iff$ (Ω-consistent $\Rightarrow$ Ω-satisfiable)