Compactness theorem application

Stream: new members

[Janitha Aswedige]

I'm trying to prove that if a first order theory has arbitrarily large finite models then it has an infinite model using the compactness theorem.

import Mathlib

open FirstOrder

theorem compactness_app {L : Language} (T : L.Theory) (h : ∀ n : ℕ, ∃ (M : T.ModelType), Finite ↑M ∧ n < Nat.card ↑M) :
  ∃ (N : T.ModelType), Infinite N := by
    let L' := L.withConstants ℕ
    let L'' :=  L.sum L'
    let distinctness := L'.distinctConstantsTheory (α := ℕ) Set.univ
    let T' : L''.Theory := (L'.lhomWithConstants ℕ).onTheory T ∪ distinctness

I'm having trouble getting T'; can't use T in the let T' line. Please help.

[Yongxi Lin (Aaron)]

I think you want your T' defined to be the union of T and the collection of inequalities a_n≠a_m right?

[Yongxi Lin (Aaron)]

So first of all, I don't think it is necessary to define L'' if you ultimately just want a language that is equal to the union of L and a sequence of constants a_n, because L.withConstants have already done that for you.

[Janitha Aswedige]

Yes, we want a_n \neq a_m .

You mean this is enough?

theorem compactness_app {L : Language} (T : L.Theory) (h : ∀ n : ℕ, ∃ (M : T.ModelType), Finite ↑M ∧ n < Nat.card ↑M) :
  ∃ (N : T.ModelType), Infinite N := by
    let L' := L.withConstants ℕ
    let distinctness := L.distinctConstantsTheory (α := ℕ) Set.univ
    let T' : L'.Theory := (L.lhomWithConstants ℕ).onTheory T ∪ distinctness

[Yongxi Lin (Aaron)]

I believe so, also you should not get any warnings now.

[Janitha Aswedige]

Yes there are no warnings. :)

[Yongxi Lin (Aaron)]

There's a warning in the code you provide above because the type of (L'.lhomWithConstants ℕ).onTheory is L'.Theory→ L'[[ℕ]].Theory, and your T is of type L.Theorynot L'.Theory. The type mismatch is the source of warning.

[Janitha Aswedige]

I thought L' was not enough. That's why I had written L'' as the sum initially.

[Yongxi Lin (Aaron)]

The equation for Language.withConstants is L.sum FirstOrder.Language.constantsOn α so I believe L' has already included L.

[Janitha Aswedige]

got it!