Preservation of the quantifier classes under embeddings (issue #15, Unit 1)

The semantic content of the signed quantifier traversal of Lomega1omega/QuantifierClass.lean: along an embedding e : A ↪[L] B,

• universal formulas transport downwards — from B to A, and
• existential formulas transport upwards — from A to B.

realize_of_embedding_signed e φ v xs :
  (IsUniversal φ   → φ.Realize (e ∘ v) (e ∘ xs) → φ.Realize v xs) ∧
  (IsExistential φ → φ.Realize v xs → φ.Realize (e ∘ v) (e ∘ xs))

The statement is valuation-aware: it quantifies over free-variable valuations v : α → A and bound-variable tuples xs : Fin n → A, with the two structures' data related only through e. That is what makes the induction go through — the all case instantiates the B-side quantifier at e a and must then recognise Fin.snoc (e ∘ xs) (e a) as e ∘ Fin.snoc xs a, which is a statement about tuples, not about sentences.

The two directions are proved simultaneously, as a conjunction, for the same reason that universalSigned is a single signed recursion: the imp case transports the antecedent by the other direction, so neither implication is provable on its own.

all is where the sign convention is tested. Its universal half is the substructure argument; its existential half is discharged because IsExistential φ.all is outright false — an existential quantifier in this syntax is a .not (.all (.not _)), so it is handled by the imp recursion, and isExistential_ex records that the encoding lands in the right class.

Neither the general theorem nor the sentence corollaries need the carriers to be nonempty; the _of_nonempty corollary carries the instance binders only so it matches the nonempty convention of Sentenceω.Entails and of the relative-preservation statements built on top of it.

theorem FirstOrder.Language.BoundedFormulaω.realize_of_embedding_signed {L : Language} {α A B : Type} [L.Structure A] [L.Structure B] (e : L.Embedding A B) {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → A) (xs : Fin n → A) : (φ.IsUniversal → φ.Realize (⇑e ∘ v) (⇑e ∘ xs) → φ.Realize v xs) ∧ (φ.IsExistential → φ.Realize v xs → φ.Realize (⇑e ∘ v) (⇑e ∘ xs))

Preservation of the quantifier classes under embeddings (the Unit-1 acceptance gate). Universal formulas reflect from the codomain to the domain; existential formulas transport from the domain to the codomain. Both halves are stated for arbitrary valuations and bound-variable tuples, and are proved by one simultaneous induction.

theorem FirstOrder.Language.BoundedFormulaω.realize_of_embedding_isUniversal {L : Language} {α A B : Type} [L.Structure A] [L.Structure B] (e : L.Embedding A B) {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → A) (xs : Fin n → A) (hφ : φ.IsUniversal) (h : φ.Realize (⇑e ∘ v) (⇑e ∘ xs)) : φ.Realize v xs

Universal formulas reflect along an embedding.

theorem FirstOrder.Language.BoundedFormulaω.realize_of_embedding_isExistential {L : Language} {α A B : Type} [L.Structure A] [L.Structure B] (e : L.Embedding A B) {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → A) (xs : Fin n → A) (hφ : φ.IsExistential) (h : φ.Realize v xs) : φ.Realize (⇑e ∘ v) (⇑e ∘ xs)

Existential formulas transport along an embedding.

theorem FirstOrder.Language.Sentenceω.realize_of_embedding_isUniversal {L : Language} {A B : Type} [L.Structure A] [L.Structure B] (e : L.Embedding A B) (σ : L.Sentenceω) (hσ : BoundedFormulaω.IsUniversal σ) (h : σ.Realize B) : σ.Realize A

A universal sentence true in an extension is true in the substructure.

theorem FirstOrder.Language.Sentenceω.realize_of_embedding_isExistential {L : Language} {A B : Type} [L.Structure A] [L.Structure B] (e : L.Embedding A B) (σ : L.Sentenceω) (hσ : BoundedFormulaω.IsExistential σ) (h : σ.Realize A) : σ.Realize B

An existential sentence true in a structure is true in every extension.

theorem FirstOrder.Language.Sentenceω.realize_of_embedding_isExistential_of_nonempty {L : Language} {A B : Type} [L.Structure A] [Nonempty A] [L.Structure B] [Nonempty B] (e : L.Embedding A B) (σ : L.Sentenceω) (hσ : BoundedFormulaω.IsExistential σ) (h : σ.Realize A) : σ.Realize B

The shape consumed by relative-preservation statements, whose semantics — like that of Sentenceω.Entails — quantifies over nonempty structures. The nonemptiness instances are carried for interface compatibility only; the proof above does not use them.