Running into universe level issues

Stream: new members

[Matt Diamond]

I'm trying to do some basic model theory stuff but I'm hitting a universe issue that I simply can't figure out (or at least that's what it appears to be):

import Mathlib

universe u

open FirstOrder

variable (L : Language)

example : ¬∃ (φ : L.Sentence), ∀ (M : Type u) [L.Structure M], M ⊨ φ ↔ Infinite M :=
by
  classical
  intro ⟨φ, hφ⟩
  let T : L.Theory := Set.range (Language.Sentence.cardGe L) ∪ {∼φ}
  let f := fun (s : L.Sentence) => if h : ∃ k, Language.Sentence.cardGe L k = s then h.choose else 0
  have : T.IsSatisfiable := by
    rw [Language.Theory.isSatisfiable_iff_isFinitelySatisfiable]
    intro T0 T0_subset_T
    let n := (T0.sup f).succ
    let M := ULift (Fin n)
    have : L.Structure M := ⟨fun _ _ => 0, fun _ _ => True⟩
    have : M ⊨ (T0 : Set L.Sentence) := by
      rw [Language.Theory.model_iff]
      intro ψ ψ_mem
      have h1 := T0_subset_T ψ_mem
      rw [Set.mem_union, Set.mem_singleton_iff] at h1
      cases h1 with
      | inl hl =>
        rw [Set.mem_range] at hl
        have hk := hl.choose_spec
        rw [← hk, Language.Sentence.realize_cardGe, Cardinal.mk_fintype, Nat.cast_le]
        rw [Fintype.card_ulift, Fintype.card_fin]
        apply Nat.le_succ_of_le
        have : hl.choose = f ψ := by
          unfold f
          rw [dif_pos hl]
        rw [this]
        exact Finset.le_sup ψ_mem
      | inr hr =>
        rw [hr, Language.Sentence.realize_not]
        intro h
        rw [hφ] at h
        exact (instFiniteULift (α := Fin n)).false
    let modelType := Language.Theory.ModelType.of (T0 : Set L.Sentence) M
    constructor
    exact modelType -- this fails due to universe issues
  sorry

Would appreciate any advice on how to solve this (the universe issue, not the theorem).

[Anthony Wang]

This works:

import Mathlib

universe u v

namespace FirstOrder

variable (L : Language.{u, v})

example : ¬∃ (φ : L.Sentence), ∀ (M : Type (max u v)) [L.Structure M], M ⊨ φ ↔ Infinite M :=
by
  classical
  intro ⟨φ, hφ⟩
  let T : L.Theory := Set.range (Language.Sentence.cardGe L) ∪ {∼φ}
  let f := fun (s : L.Sentence) => if h : ∃ k, Language.Sentence.cardGe L k = s then h.choose else 0
  have : T.IsSatisfiable := by
    rw [Language.Theory.isSatisfiable_iff_isFinitelySatisfiable]
    intro T0 T0_subset_T
    let n := (T0.sup f).succ
    let M := ULift (Fin n)
    have : L.Structure M := ⟨fun _ _ => 0, fun _ _ => True⟩
    have : M ⊨ (T0 : Set L.Sentence) := by
      rw [Language.Theory.model_iff]
      intro ψ ψ_mem
      have h1 := T0_subset_T ψ_mem
      rw [Set.mem_union, Set.mem_singleton_iff] at h1
      cases h1 with
      | inl hl =>
        rw [Set.mem_range] at hl
        have hk := hl.choose_spec
        rw [← hk, Language.Sentence.realize_cardGe, Cardinal.mk_fintype, Nat.cast_le]
        rw [Fintype.card_ulift, Fintype.card_fin]
        apply Nat.le_succ_of_le
        have : hl.choose = f ψ := by
          unfold f
          rw [dif_pos hl]
        rw [this]
        exact Finset.le_sup ψ_mem
      | inr hr =>
        rw [hr, Language.Sentence.realize_not]
        intro h
        rw [hφ] at h
        exact (instFiniteULift (α := Fin n)).false
    let modelType := Language.Theory.ModelType.of (T0 : Set L.Sentence) M
    constructor
    exact modelType
  sorry

[Matt Diamond]

for some reason I was unable to write Language.{u, v} but I was able to write FirstOrder.Language.{u, v} (which did indeed allow me to solve the problem right before you answered)

[Matt Diamond]

Lean complained about "too many explicit universe levels for Language"

[Matt Diamond]

which doesn't really make sense

[Matt Diamond]

oh, you know what, I wrote open FirstOrder instead of namespace FirstOrder... maybe that's why

[Anthony Wang]

My guess is that Lean is getting confused because Language is also defined in Mathlib/Computability/Language.lean as a set of strings over an alphabet and only takes one universe parameter instead of two.

[Matt Diamond]

well what's odd is that I'm able to write L.Sentence and when I hover over the L it shows FirstOrder.Language... seems like a bug if Lean mixes up the count of universe params but not the actual meaning

[Matt Diamond]

regardless, thanks for the help!