FirstOrder.Language.Embedding.isElementary_of_exists
theorem FirstOrder.Language.Embedding.isElementary_of_exists :
∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
(f : L.Embedding M N),
(∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))) →
∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
This theorem, known as the Tarski-Vaught test, is a criterion for the elementarity of an embedding in first-order logic. It states that for any first-order language `L` and any two structures `M` and `N` for `L`, given an embedding `f` from `M` into `N`, if for every natural number `n`, every `n+1`-bounded formula `φ` of `L`, every `n`-tuple `x` from `M`, and every element `a` from `N`, if `φ` holds in `N` when applied to the `n+1`-tuple formed by appending `a` to the image of `x` under `f`, then there is an element `b` in `M` such that `φ` also holds in `N` when applied to the `n+1`-tuple formed by appending the image of `b` under `f` to the image of `x` under `f`. If this condition holds, then for every natural number `n` and every `n`-tuple `x` from `M`, a formula `φ` of `L` holds in `N` under the mapping `f` if and only if `φ` holds in `M`.
More concisely: The Tarski-Vaught test for an embedding between first-order structures `M` and `N` holds if for every `n`, every `n`-bounded formula `φ`, every `n`-tuple `x` from `M`, and every element `a` from `N`, if `φ` holds in `N` when appended to the image of `x` under `f`, then there exists `b` in `M` such that `φ` holds in `N` when appended to the image of `x` under `f`. If this condition holds, then `φ` holds in `N` under `f` if and only if it holds in `M`.
|
FirstOrder.Language.ElementaryEmbedding.map_formula
theorem FirstOrder.Language.ElementaryEmbedding.map_formula :
∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
(f : L.ElementaryEmbedding M N) {α : Type u_5} (φ : L.Formula α) (x : α → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
This theorem, `FirstOrder.Language.ElementaryEmbedding.map_formula`, states that for any first-order language `L` and two structures `M` and `N` of `L`, if `f` is an elementary embedding from `M` to `N`, then for any formula `φ` in the language `L` with free variables indexed by some type `α`, and any function `x` from `α` to `M`, the realization of `φ` given values by the composition of `f` and `x` is equivalent to the realization of `φ` given values directly by `x`. In other words, it says that the truth value of a formula does not change when we first apply an elementary embedding to the values of its variables before evaluating it.
More concisely: For any first-order language L, structures M and N, elementary embedding f from M to N, formula φ of L with free variables indexed by type α, and function x from α to M, the realization of φ given values by the composition of f and x is equivalent to the realization of φ given values directly by x.
|
FirstOrder.Language.ElementaryEmbedding.map_sentence
theorem FirstOrder.Language.ElementaryEmbedding.map_sentence :
∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N],
L.ElementaryEmbedding M N → ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
This theorem states that for any first-order logical language `L`, and any two structures `M` and `N` for `L`, any elementary embedding from `M` to `N` preserves sentences. In other words, for each sentence `φ` in the language `L`, `M` satisfies `φ` if and only if `N` satisfies `φ`. This is a key property of elementary embeddings in model theory, as it shows they preserve the truth of sentences between structures.
More concisely: For any first-order logical language L and structures M and N with an elementary embedding from M to N, they satisfy the same first-order sentences.
|
FirstOrder.Language.ElementaryEmbedding.map_fun
theorem FirstOrder.Language.ElementaryEmbedding.map_fun :
∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
(φ : L.ElementaryEmbedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
The theorem `FirstOrder.Language.ElementaryEmbedding.map_fun` asserts that for any first-order language `L`, types `M` and `N` with structures as `FirstOrder.Language.Structure`, and an elementary embedding `φ` from `M` to `N`, for any function symbol `f` in `L` and for any map `x` from `Fin n → M`, where `n` is the arity of the function, the image of the interpretation of `f` in `M` under `φ` is equal to the interpretation of `f` in `N`. This embedding is done by mapping the arguments of `f` in `M` to `N` according to `φ` before applying `f`. This states that the elementary embedding `φ` preserves the interpretation of the function symbols in the language `L`.
More concisely: For any first-order language L, structures M and N, and elementary embedding φ from M to N, if f is a function symbol in L and x is a map from Fin n to M (where n is the arity of f), then the interpretation of f in N under φ is equal to the application of f to the images of x under φ.
|
FirstOrder.Language.ElementaryEmbedding.comp_assoc
theorem FirstOrder.Language.ElementaryEmbedding.comp_assoc :
∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : L.Structure M]
[inst_1 : L.Structure N] [inst_2 : L.Structure P] [inst_3 : L.Structure Q] (f : L.ElementaryEmbedding M N)
(g : L.ElementaryEmbedding N P) (h : L.ElementaryEmbedding P Q), (h.comp g).comp f = h.comp (g.comp f)
This theorem states that the composition of elementary embeddings is associative in the context of first-order logic. Specifically, for any first-order language 'L' and given types 'M', 'N', 'P', and 'Q' that have structure of 'L', if we have elementary embeddings 'f' from 'M' to 'N', 'g' from 'N' to 'P', and 'h' from 'P' to 'Q', then composing 'h' with 'g', and then the result with 'f' is equal to the composition of 'h' with the composition of 'g' and 'f'. This means you can change the grouping of the composition operation without changing the result, which is the definition of associativity.
More concisely: For first-order structures M, N, P, and Q, and elementary embeddings f : M -> N, g : N -> P, and h : P -> Q, we have h ∘ (g ∘ f) = (h ∘ g) ∘ f.
|