Define entailment (Model Theory)

Stream: mathlib4

[Moritz R]

I believe mathlib doesn't have entailment (correct me if i'm wrong!).
In Set Theory one would put the quantifier over all possible domains. What would be a sensible approach in Lean?
I was thinking of checking for all models with domain in Type (max u v) (the smallest universe containing all the Language symbols), since one can prove that all larger universes don't change the meaning. Is this the right approach? What about smaller universes than Type (max u v) ?

import Mathlib.ModelTheory.Bundled

namespace FirstOrder
namespace Language
namespace Theory

variable {L : Language.{u, v}} {T : L.Theory} {α : Type w} {n : ℕ}

def entails (T T' : L.Theory) : Prop :=
    ∀ (M : Type (max u v)) [L.Structure M], T.Model M → T'.Model M

def entails2 (T T' : L.Theory) : Prop := --this one contains `w` as "free" universe parameter
    ∀ (M : Type max (max u v) w) [L.Structure M], T.Model M → T'.Model M


theorem larger_universes_dont_change_meaning : entails2 T T' ↔ entails T T' := sorry --provable

end Theory
end Language
end FirstOrder

[Moritz R]

One should definitely add Nonempty M to the premises in both definitons

[Dexin Zhang]

Isn't docs#FirstOrder.Language.Theory.ModelsBoundedFormula entailment?

[Moritz R]

oh, nice. Thank you!

[Dexin Zhang]

Oh you mean theories entails theories. I guess it's equivalent to ∀ φ ∈ T', T ⊨ᵇ φ

[Moritz R]

I find the naming to be very unintuitive. I searched for all the synonyms i could come up with, but still didn't find it

[Moritz R]

Maybe we could add a comment that this is typically called entailment or semantic consequence in the literature

[Dexin Zhang]

Moritz R said:

I was thinking of checking for all models with domain in Type (max u v) (the smallest universe containing all the Language symbols), since one can prove that all larger universes don't change the meaning. Is this the right approach? What about smaller universes than Type (max u v) ?

And the definition of ⊨ᵇ uses the Type (max u v) approach. I guess due to Lowenheim-Skolem this quantifies for all models in any universe

[Dexin Zhang]

Moritz R said:

I find the naming to be very unintuitive. I searched for all the synonyms i could come up with, but still didn't find it

You can search for symbol ⊨, that's how I found it

[Moritz R]

Dexin Zhang schrieb:

Moritz R said:

I find the naming to be very unintuitive. I searched for all the synonyms i could come up with, but still didn't find it

You can search for symbol ⊨, that's how I found it

good idea!

[Dexin Zhang]

Moritz R said:

Maybe we could add a comment that this is typically called entailment or semantic consequence in the literature

It should be nicer to just rename it as Entails :innocent:

[Moritz R]

This would also be fine with me. But i can also understand that someone might want to use the same name for all the uses of a symbol, though it feels weird

[Moritz R]

Also the docstring is currently

/-- A theory models a (bounded) formula when
any of its nonempty models realizes that formula on all inputs. -/

and i would much rather have it be formulated like this:

/-- A theory models a (bounded) formula when
all of its nonempty models realize that formula on all inputs. -/

or even better:

/-- A theory models a (bounded) formula when
all of its nonempty models realize that formula on for all realizations `v` of free variables. -/

[Moritz R]

The current docstring sounds a bit like existential quantification to me. It definitely isn't unambigous

[Kevin Buzzard]

Moritz R said:

Also the docstring is currently

/-- A theory models a (bounded) formula when
any of its nonempty models realizes that formula on all inputs. -/

and i would much rather have it be formulated like this:

/-- A theory models a (bounded) formula when
all of its nonempty models realize that formula on all inputs. -/

or even better:

/-- A theory models a (bounded) formula when
all of its nonempty models realize that formula on for all realizations `v` of free variables. -/

Then make a PR just changing the docstrings.

[Moritz R]

Dexin Zhang schrieb:

Moritz R said:

Maybe we could add a comment that this is typically called entailment or semantic consequence in the literature

It should be nicer to just rename it as Entails :innocent:

Any opinions on this?

[James E Hanson]

As a model theorist myself, I am not a huge fan of reading $\models$ as 'models' in this context (i.e., when neither of the objects in the relationship is actually a model at all), although I know that some model theorists do read it that way.