CountableModels.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Countable elementary submodels in arbitrary membership structures.

def OAI.PartitionConsistency.CountableModel.witness line 18
Source documentation
One local existential witness for each formula and parameter tuple. The selection is external: it makes no choice function in the object structure.
```
noncomputable def witness [Nonempty M] {n}
    (φ : BasicFormula (n + 1)) (v : Fin n → M) : M := by
…
```
theorem OAI.PartitionConsistency.CountableModel.witness_spec line 25
def OAI.PartitionConsistency.CountableModel.step line 33
Source documentation
Close a set once under all formula witnesses with finitely many parameters.
```
noncomputable def step [Nonempty M] (S : Set M) : Set M :=
…
```
theorem OAI.PartitionConsistency.CountableModel.subset_step line 37
theorem OAI.PartitionConsistency.CountableModel.step_countable line 39

def OAI.PartitionConsistency.CountableModel.stage line 45

Source documentation

Skolem-hull stages, starting from a given nonempty countable set.

noncomputable def stage [Nonempty M] (S : Set M) : ℕ → Set M
  | 0 => S
  | n + 1 => step E (stage S n)

/-- The countable union of the finite stages, not closure under arbitrary
external functions. -/

Mentions: OAI.PartitionConsistency.CountableModel.step

def OAI.PartitionConsistency.CountableModel.hull line 51
Source documentation
The countable union of the finite stages, not closure under arbitrary external functions.
```
noncomputable def hull [Nonempty M] (S : Set M) : Set M := ⋃ n, stage E S n
```
Mentions: OAI.PartitionConsistency.CountableModel.stage
theorem OAI.PartitionConsistency.CountableModel.stage_mono line 53
theorem OAI.PartitionConsistency.CountableModel.stage_countable line 58
theorem OAI.PartitionConsistency.CountableModel.hull_countable line 64
theorem OAI.PartitionConsistency.CountableModel.subset_hull line 67
theorem OAI.PartitionConsistency.CountableModel.tuple_bounded line 72
Source documentation
Every finite tuple drawn from the hull lies at one stage.
```
theorem tuple_bounded [Nonempty M] {S : Set M} {n : ℕ}
    (v : Fin n → hull E S) :
    ∃ k, ∀ i, (v i).val ∈ stage E S k := by
…
```
Mentions: OAI.PartitionConsistency.CountableModel.hull, OAI.PartitionConsistency.CountableModel.stage
theorem OAI.PartitionConsistency.CountableModel.witness_mem_hull line 83
Source documentation
The hull is closed under the chosen witness for each formula.
```
theorem witness_mem_hull [Nonempty M] {S : Set M} {n : ℕ}
    (φ : BasicFormula (n + 1)) (v : Fin n → hull E S) :
    witness E φ (Subtype.val ∘ v) ∈ hull E S := by
…
```
Mentions: OAI.PartitionConsistency.CountableModel.hull, OAI.PartitionConsistency.CountableModel.witness
def OAI.PartitionConsistency.CountableModel.HasWitnesses line 92
Source documentation
Tarski–Vaught condition for a subdomain, stated for the formula basis.
```
def HasWitnesses (S : Set M) : Prop :=
…
```
theorem OAI.PartitionConsistency.CountableModel.hull_hasWitnesses line 97
theorem OAI.PartitionConsistency.CountableModel.basic_elementary line 104
Source documentation
Formula truth is preserved and reflected in any subdomain satisfying the Tarski–Vaught condition. Nothing requires external well-foundedness.
```
theorem basic_elementary {S : Set M} (hS : HasWitnesses E S)
    {n} (φ : BasicFormula n) (v : Fin n → S) :
    BasicFormula.Realize (fun x y : S => E x.val y.val) v φ ↔
      BasicFormula.Realize E (Subtype.val ∘ v) φ := by
…
```
Mentions: OAI.PartitionConsistency.CountableModel.HasWitnesses
theorem OAI.PartitionConsistency.CountableModel.elementary line 127
Source documentation
Elementarity for the full language used in ZF and the target theory.
```
theorem elementary {S : Set M} (hS : HasWitnesses E S)
    {n} (φ : Formula n) (v : Fin n → S) :
    Formula.Realize (fun x y : S => E x.val y.val) v φ ↔
      Formula.Realize E (Subtype.val ∘ v) φ := by
…
```
Mentions: OAI.PartitionConsistency.CountableModel.HasWitnesses, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.Realize
theorem OAI.PartitionConsistency.CountableModel.exists_countable_elementary line 137
Source documentation
Downward Löwenheim–Skolem for this countable membership language, with parameters: a countable subset of a nonempty structure extends to a nonempty countable elementary subdomain of that same structure.
```
theorem exists_countable_elementary [Nonempty M] {S : Set M} (hS : S.Countable) :
    ∃ N : Set M, S ⊆ N ∧ N.Nonempty ∧ N.Countable ∧
      ∀ n (φ : Formula n) (v : Fin n → N),
        Formula.Realize (fun x y : N => E x.val y.val) v φ ↔
          Formula.Realize E (Subtype.val ∘ v) φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.Realize
theorem OAI.PartitionConsistency.CountableModel.exists_countable_model line 153
Source documentation
Every nonempty relational model of any theory in the target language has a nonempty countable submodel. This is only the downward Löwenheim–Skolem step: it does not prove completeness or construct a model from syntactic consistency.
```
theorem exists_countable_model [Nonempty M] {T : Theory} (hT : Models E T) :
    ∃ N : Set M, N.Nonempty ∧ N.Countable ∧
      Models (fun x y : N => E x.val y.val) T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Models