Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.ModelType.defaultExpansion

{L : FirstOrder.Language} →
  {T : L.Theory} →
    {L' : FirstOrder.Language} →
      {φ : L →ᴸ L'} →
        φ.Injective →
          [(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)] →
            [(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)] →
              (M : T.ModelType) → [Inhabited ↑M] → (φ.onTheory T).ModelType

When φ is injective, defaultExpansion expands a model of T to a model of φ.onTheory T arbitrarily.

Defined in

Mathlib.ModelTheory.Bundled

Cited by

3 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableDecidableInhabited