FO-definability of ℕ

Stream: mathlib4

[Marcus Rossel]

I'm trying to state that the class of structures isomorphic to $\mathbb{N}$ is not FO-definable, according to this definition of FO-definability.

Is this a sensible translation, or will I have a hard time trying to prove it this way?

import Mathlib.ModelTheory.Definability
open scoped FirstOrder

namespace Nat

inductive FunctionSymbol : ℕ → Type where
  | zero : FunctionSymbol 0
  | succ : FunctionSymbol 1

def ℕLang : FirstOrder.Language where
  Functions := FunctionSymbol
  Relations _ := Empty

-- The canonical structure for `ℕLang` with domain `ℕ`.
instance : ℕLang.Structure ℕ where
  funMap
    | .zero => 0
    | .succ => fun ns => Nat.succ (ns 0)
  RelMap := nofun

theorem not_FO_definable :
    ¬∃ φ : ℕLang.Sentence, ∀ M [ℕLang.Structure M], M ⊨ φ → Nonempty (ℕ ≃[ℕLang] M) :=
  sorry

I noticed that there's also a notion of FO-definability in Mathlib, but I'm struggling to understand it.

[Matt Diamond]

I noticed that there's also a notion of FO-definability in Mathlib, but I'm struggling to understand it.

If you're referring to docs#Set.Definable, that appears to be about sets of tuples within a single structure, where the set is defined by a formula φ which is true iff the variables in the formula are assigned according to the tuple. For example, the set of zeros of a multivariable polynomial is a definable set in this context (docs#FirstOrder.Ring.mvPolynomial_zeroLocus_definable).

[Dexin Zhang]

Your theorem is actually false

open FirstOrder.Language in
theorem FO_definable :
    ∃ φ : ℕLang.Sentence, ∀ M [ℕLang.Structure M], M ⊨ φ → Nonempty (ℕ ≃[ℕLang] M) :=
  ⟨⊥, by simp [Sentence.Realize]⟩

[Matt Diamond]

hmm... maybe changing → to ↔ would be enough to repair it?

[Dexin Zhang]

I think you need to assume ℕ ⊨ φ

Here is a proof of your claim, using Löwenheim–Skolem theorem:

open FirstOrder.Language in
lemma card_ℕLang : ℕLang.card = 2 := by
  letI : Fintype ℕLang.Symbols := by
    refine ⟨⟨{Sum.inl ⟨0, .zero⟩, Sum.inl ⟨1, .succ⟩}, ?_⟩, ?_⟩
    · simp
    · rintro (⟨_, x⟩ | ⟨_, x⟩)
      · cases x <;> simp
      · cases x
  exact Cardinal.mk_fintype _

open FirstOrder.Language Cardinal in
theorem not_FO_definable :
    ¬∃ φ : ℕLang.Sentence, ℕ ⊨ φ ∧ ∀ (M : Type u) [ℕLang.Structure M], M ⊨ φ → Nonempty (ℕ ≃[ℕLang] M) := by
  intro ⟨φ, hφ, hφ'⟩
  obtain ⟨⟨N, _⟩, hN, hN'⟩ := exists_elementarilyEquivalent_card_eq.{0, 0, u} ℕLang ℕ ℵ₁
    (aleph0_le_aleph _) (by simpa [card_ℕLang] using (aleph0_le_aleph 1).trans' (lt_aleph0.2 ⟨2, rfl⟩).le)
  obtain ⟨e⟩ := hφ' N ((hN.realize_sentence φ).1 hφ)
  have := e.lift_cardinal_eq
  simp [hN', aleph0_lt_aleph_one.ne] at this

[Matt Diamond]

I think you need to assume ℕ ⊨ φ

perhaps either approach works... I think ↔ should suffice because the claim is that the set of structures that realize φ is exactly equal to the set of structures isomorphic to ℕ

[Dexin Zhang]

Yeah, that two versions are not very different. Here is a proof of ↔ version based on ℕ ⊨ φ version:

theorem not_FO_definable' :
    ¬∃ φ : ℕLang.Sentence, ∀ (M : Type) [ℕLang.Structure M], M ⊨ φ ↔ Nonempty (ℕ ≃[ℕLang] M) := by
  intro ⟨φ, hφ⟩
  have hφ' := (hφ ℕ).2 ⟨.refl _ _⟩
  exact not_FO_definable ⟨φ, hφ', fun M _ => (hφ M).1⟩

Unfortunately I have to get rid of Type u, because I don't know how to lift ℕ to Type u with its Structure

[Marcus Rossel]

Dexin Zhang said:

I think you need to assume ℕ ⊨ φ

Ah yes, thank you, I forgot that.