FirstOrder.Language.ElementarilyEquivalent.theory_model_iff
theorem FirstOrder.Language.ElementarilyEquivalent.theory_model_iff :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
{T : L.Theory}, L.ElementarilyEquivalent M N → (M ⊨ T ↔ N ⊨ T)
This theorem states that for any first-order language `L`, any two types `M` and `N`, and any theory `T` of `L` (where `M` and `N` are both structures of `L`), if `M` and `N` are elementarily equivalent in `L` (meaning they satisfy the same sentences of `L`), then `M` is a model of `T` if and only if `N` is a model of `T`. In other words, if two structures are elementarily equivalent, then any theory that one structure satisfies is also satisfied by the other structure.
More concisely: If two first-order structures `M` and `N` of a language `L` are elementarily equivalent, then `M` is a model of theory `T` in `L` if and only if `N` is a model of `T`.
|
Mathlib.ModelTheory.Semantics._auxLemma.45
theorem Mathlib.ModelTheory.Semantics._auxLemma.45 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {t₁ t₂ : L.Term α} {x : α → M},
(t₁.equal t₂).Realize x = (FirstOrder.Language.Term.realize x t₁ = FirstOrder.Language.Term.realize x t₂)
The theorem `Mathlib.ModelTheory.Semantics._auxLemma.45` states that for any first-order language `L`, any type `M` with a structure for `L`, and any type `α`, for any two terms `t₁` and `t₂` of the language `L` over `α` and any assignment `x` of values in `M` to variables in `α`, realizing the formula that expresses the equality of `t₁` and `t₂` under the assignment `x` is equivalent to the statement that the realization of `t₁` under `x` is equal to the realization of `t₂` under `x`. In other words, a formula expressing the equality of two terms is realized as true if and only if the two terms evaluate to the same value under the given variable assignment.
More concisely: For any first-order language L, structure M for L, type α, terms t₁ and t₂ over α in L, and assignment x in M, the formula expressing the equality of t₁ and t₂ under x is true if and only if the realizations of t₁ and t₂ under x are equal.
|
Mathlib.ModelTheory.Semantics._auxLemma.20
theorem Mathlib.ModelTheory.Semantics._auxLemma.20 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ}
{θ : L.BoundedFormula α l.succ} {v : α → M} {xs : Fin l → M},
θ.all.Realize v xs = ∀ (a : M), θ.Realize v (Fin.snoc xs a)
The theorem `Mathlib.ModelTheory.Semantics._auxLemma.20` states that for any first-order language `L`, a type `M` equipped with a structure for `L`, a type `α`, a natural number `l`, a bounded formula `θ` in `L` with arity `Nat.succ l`, a function `v` from `α` to `M`, and a function `xs` from `Fin l` to `M`, the realization of the universal quantification of `θ` with respect to `v` and `xs` is equivalent to the statement that for all `a` in `M`, `θ` is realized with respect to `v` and `xs` to which `a` has been added at the end (i.e., `Fin.snoc xs a`). This essentially captures the semantics of the universal quantifier in first-order logic in terms of function realization.
More concisely: For any first-order language L, a structure M, a type α, a natural number l, a bounded formula θ in L with arity Nat.succ l, a valuation v from α to M, and an assignment xs from Fin l to M, the universal quantification of θ with respect to v and xs is equivalent to the statement that for all a in M, θ is realized with respect to v and xs extended by a.
|
FirstOrder.Language.Theory.Model.mono
theorem FirstOrder.Language.Theory.Model.mono :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T T' : L.Theory}, M ⊨ T' → T ⊆ T' → M ⊨ T := by
sorry
This theorem states that for any given first-order language `L`, and a set `M` with the structure of `L`, if `M` is a model of a theory `T'` (i.e., `M` satisfies all sentences in `T'`), and if all sentences of a theory `T` are included in `T'` (i.e., `T` is a subset of `T'`), then `M` is also a model of `T`. In essence, it guarantees that if a structure satisfies a larger theory, it also satisfies any smaller theory contained within the larger one.
More concisely: If `M` is a model of a theory `T'` and `T` is a subset of `T'`, then `M` is a model of `T`.
|
Mathlib.ModelTheory.Semantics._auxLemma.54
theorem Mathlib.ModelTheory.Semantics._auxLemma.54 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (T : L.Theory), M ⊨ T = ∀ φ ∈ T, M ⊨ φ
This theorem, under the context of model theory in first-order languages, states that for any first-order language `L` and any structure `M` of `L`, a theory `T` (which is a set of sentences in `L`) is said to be satisfied by `M` (denoted by `M ⊨ T`) if and only if every sentence `φ` in the theory `T` is satisfied by `M` (denoted by `M ⊨ φ`).
More concisely: A first-order theory T is satisfied by a structure M if and only if every sentence φ in T is satisfied by M.
|
FirstOrder.Language.model_nonemptyTheory_iff
theorem FirstOrder.Language.model_nonemptyTheory_iff :
∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M], M ⊨ L.nonemptyTheory ↔ Nonempty M
This theorem connects the concepts of a structure and nonemptiness in a first-order language. Specifically, for a given first-order language 'L' and a type 'M' that has a structure in 'L', the theorem states that 'M' is a model of the nonempty theory of 'L' if and only if 'M' is nonempty. In other words, a type 'M' satisfies all sentences in the nonempty theory of 'L' (i.e., there is at least one element in 'M') if and only if there exists at least one element in 'M'.
More concisely: For a first-order language L and a nonempty type M in it, M is a model of L's nonempty theory if and only if M is nonempty.
|
Mathlib.ModelTheory.Semantics._auxLemma.22
theorem Mathlib.ModelTheory.Semantics._auxLemma.22 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ}
{θ : L.BoundedFormula α l.succ} {v : α → M} {xs : Fin l → M},
θ.ex.Realize v xs = ∃ a, θ.Realize v (Fin.snoc xs a)
This theorem in the Model Theory of First-Order Languages states that, for any first-order language `L`, any structure `M` of `L`, any type `α`, any natural number `l`, any bounded formula `θ` of `L` with `l + 1` variables, any function `v` from `α` to `M`, and any function `xs` from the first `l` natural numbers to `M`, the bounded formula obtained by prefixing `θ` with an existential quantifier is true under the realization function `v` and `xs` if and only if there exists an element `a` in `M` such that the original formula `θ` is true under `v` and the function obtained by extending `xs` with `a` at the last position.
In simpler terms, it states that an existential quantification in a first-order language corresponds to the existence of some element that makes the original formula true.
More concisely: For any first-order language L, structure M, type α, natural number l, bounded formula θ of L with l + 1 variables, function v from α to M, and function xs from the first l natural numbers to M, the existential quantification of θ is true under realizations v and xs if and only if there exists an element a in M making θ true under v and xs extended with a.
|
FirstOrder.Language.LHom.onTheory_model
theorem FirstOrder.Language.LHom.onTheory_model :
∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [inst_1 : L'.Structure M]
(φ : L.LHom L') [inst_2 : φ.IsExpansionOn M] (T : L.Theory), M ⊨ φ.onTheory T ↔ M ⊨ T
This theorem, `FirstOrder.Language.LHom.onTheory_model`, states that for any two languages `L` and `L'`, and any type `M` that has a structure for both `L` and `L'`, given a language homomorphism `φ` from `L` to `L'` that is an expansion on `M`, and a theory `T` in the language `L`, then `M` is a model of the theory `T` under the language map `φ` if and only if `M` is a model of the theory `T`. In other words, the truth of a theory `T` under a language map `φ` in a model `M` depends solely on whether `M` is a model of `T` itself.
More concisely: For any languages L and L', type M with structures for L and L', theory T in L, language homomorphism φ from L to L' that is an expansion on M: M is a model of T under φ if and only if M is a model of T.
|
FirstOrder.Language.elementarilyEquivalent_iff
theorem FirstOrder.Language.elementarilyEquivalent_iff :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
L.ElementarilyEquivalent M N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
The theorem `FirstOrder.Language.elementarilyEquivalent_iff` states that for any first-order language `L` and any two structures `M` and `N` of `L`, `M` and `N` are elementarily equivalent if and only if they satisfy the same sentences of `L`. Here, a sentence is defined as a formula with no free variables, and a structure is said to satisfy a sentence if the sentence holds true under an interpretation in that structure. Essentially, this theorem is reflecting the fact that two structures are identical in the language if they agree on all sentences of the language.
More concisely: Two first-order structures of the same language are elementarily equivalent if and only if they satisfy the same sentences in that language.
|
FirstOrder.Language.Theory.realize_sentence_of_mem
theorem FirstOrder.Language.Theory.realize_sentence_of_mem :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (T : L.Theory) [inst_1 : M ⊨ T] {φ : L.Sentence},
φ ∈ T → M ⊨ φ
This theorem states that for any first-order language `L`, any type `M` that has a `FirstOrder.Language.Structure` over `L`, and any theory `T` in the language `L` that `M` realizes, if a sentence `φ` belongs to the theory `T`, then `M` realizes the sentence `φ`. In other words, an interpretation `M` of a theory `T` in a first-order language `L` makes every sentence in `T` true.
More concisely: For any first-order language L, type M with a FirstOrder.Language.Structure over L, and theory T in L realized by M, if φ ∈ T then M |- φ (M satisfies sentence φ from theory T).
|
FirstOrder.Language.Theory.model_iff_subset_completeTheory
theorem FirstOrder.Language.Theory.model_iff_subset_completeTheory :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T : L.Theory}, M ⊨ T ↔ T ⊆ L.completeTheory M := by
sorry
This theorem states that for any first-order language `L`, structure `M` of language `L`, and theory `T` of language `L`, `M` is a model of `T` if and only if `T` is a subset of the complete theory of `M` in `L`. In other words, a structure `M` satisfies a theory `T` exactly when every sentence in `T` is also in the set of all sentences that `M` satisfies, that is, the complete theory of `M`.
More concisely: A first-order structure modelally satisfies a theory if and only if the theory is a subset of its complete theory.
|
Mathlib.ModelTheory.Semantics._auxLemma.14
theorem Mathlib.ModelTheory.Semantics._auxLemma.14 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, (φ ⊔ ψ).Realize v xs = (φ.Realize v xs ∨ ψ.Realize v xs)
The theorem `Mathlib.ModelTheory.Semantics._auxLemma.14` from the `Mathlib` library states that for any first-order language `L`, any type `M` that is a structure for `L`, any type `α`, length `l`, bounded formulas `φ` and `ψ` in `L`, function `v` from `α` to `M`, and function `xs` from finite set of size `l` to `M`, the realization (interpretation) of the join (logical disjunction) of `φ` and `ψ` is equivalent to either the realization of `φ` or the realization of `ψ`. This is a fundamental theorem in model theory, a branch of mathematical logic that deals with the relationship between syntactic expressions (formulas) and their interpretations in mathematical structures.
More concisely: For any first-order language L, structure M for L, function v : α -> M, finite set xs : set (M)^l of size l, and bounded formulas φ and ψ in L, the realization of φ \/\ψ equals the realization of φ or the realization of ψ.
|
FirstOrder.Language.Theory.model_iff
theorem FirstOrder.Language.Theory.model_iff :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (T : L.Theory), M ⊨ T ↔ ∀ φ ∈ T, M ⊨ φ
This theorem pertains to theories and models in the context of first-order logic. Specifically, it states that for any language `L` and any model `M` of that language (where `M` is a structure for `L`), a theory `T` (which is a set of sentences in `L`) is a model of `M` if and only if every sentence `φ` in the theory `T` is a model of `M`. In other words, a model `M` satisfies a theory `T` precisely when `M` satisfies every sentence in `T`.
More concisely: A first-order theory T is a model of a structure M if and only if every sentence φ in T is satisfied in M.
|
Mathlib.ModelTheory.Semantics._auxLemma.9
theorem Mathlib.ModelTheory.Semantics._auxLemma.9 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, (φ.imp ψ).Realize v xs = (φ.Realize v xs → ψ.Realize v xs)
This theorem is part of Model Theory in the field of mathematical logic and is about the semantics of logical formulas. It states that for any first-order language `L`, any model `M` of that language, any type `α`, any natural number `l`, any two bounded formulas `φ` and `ψ` in `L` of the same quantifier depth `l`, and any variable assignment `v` from `α` to `M` and `xs` from `Fin l` to `M`, realizing the implication `φ -> ψ` is equivalent to the logical implication: if `φ` is realized then `ψ` is also realized. Here, "realizing a formula" refers to the formula being true under the given variable assignment in the model.
More concisely: For any first-order language L, model M, type α, natural number l, bounded formulas φ and ψ of depth l in L, variable assignment v from α to M, and xs from Fin l to M, realizing implication φ -> ψ (in the sense of being true under v in M for all xs) is equivalent to the logical implication (φ implies ψ).
|
FirstOrder.Language.model_infiniteTheory_iff
theorem FirstOrder.Language.model_infiniteTheory_iff :
∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M], M ⊨ L.infiniteTheory ↔ Infinite M
The theorem `FirstOrder.Language.model_infiniteTheory_iff` states that for any first-order language `L` and any structure `M` of that language, `M` models the infinite theory of `L` if and only if `M` is infinite. In other words, a structure `M` satisfies all sentences in `L` stating that there exists more than `n` elements for all natural numbers `n` if and only if the cardinality of `M` is infinite.
More concisely: A first-order structure is a model of the infinite theory of a language if and only if it has infinite cardinality.
|
FirstOrder.Language.BoundedFormula.realize_rel₂
theorem FirstOrder.Language.BoundedFormula.realize_rel₂ :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
{R : L.Relations 2} {t₁ t₂ : L.Term (α ⊕ Fin l)},
(R.boundedFormula₂ t₁ t₂).Realize v xs ↔
FirstOrder.Language.Structure.RelMap R
![FirstOrder.Language.Term.realize (Sum.elim v xs) t₁, FirstOrder.Language.Term.realize (Sum.elim v xs) t₂]
The theorem "FirstOrder.Language.BoundedFormula.realize_rel₂" states that for every first-order language `L`, type `M`, structure instance `inst` for `L` and `M`, type `α`, natural number `l`, function `v` mapping `α` to `M`, function `xs` mapping a finite sequence of natural numbers to `M`, relation `R` of `L` with arity 2, and terms `t₁` and `t₂` of the language `L` with variables from either `α` or the finite sequence of `n` elements, the realisation of the bounded formula obtained by applying the relation `R` to the terms `t₁` and `t₂`, under the variable assignments `v` and `xs`, is equivalent to the interpretation of the relation `R` in the structure `M`, applied to the realised values of the terms `t₁` and `t₂` (which are obtained by realising the terms under the combined variable assignment given by the sum elimination of `v` and `xs`).
This essentially relates the semantics of a relation applied to two terms in a first-order language to the interpretation of that relation in a structure for that language.
More concisely: For any first-order language L, type M, structure instance inst for L and M, relation R of arity 2, and terms t₁ and t₂ in L with variables from α or a finite sequence of natural numbers, the realization of the bounded formula obtained by applying R to t₁ and t₂ under variable assignments v and xs is equivalent to interpreting R in M on the realized values of t₁ and t₂.
|
FirstOrder.Language.BoundedFormula.realize_iff
theorem FirstOrder.Language.BoundedFormula.realize_iff :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)
The theorem `FirstOrder.Language.BoundedFormula.realize_iff` states that for any first-order language `L`, type `M` with a structure for `L`, type `α`, natural number `l`, bounded formulas `φ` and `ψ` in `L` for `α` and `l`, a function `v` from `α` to `M`, and a function `xs` from the finite set of size `l` to `M`, the realization of the biimplication (if and only if, represented by the "iff" function) of `φ` and `ψ` with respect to `v` and `xs` is equivalent to the biimplication of the realizations of `φ` and `ψ` with respect to `v` and `xs`. In other words, realizing the biimplication of two bounded formulas is equivalent to the biimplication of the realizations of each formula.
More concisely: For any first-order language L, type α, natural number l, bounded formulas φ and ψ in L for α, and functions v : α → M and xs : finite set of size l → M, the realization of the biimplication of φ and ψ with respect to v and xs is equivalent to the biimplication of the realizations of φ and ψ with respect to v and xs.
|
FirstOrder.Language.Term.realize_constants
theorem FirstOrder.Language.Term.realize_constants :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {c : L.Constants} {v : α → M},
FirstOrder.Language.Term.realize v c.term = ↑c
The theorem `FirstOrder.Language.Term.realize_constants` states that for any first-order language `L`, an arbitrary type `M`, a structure of `L` on `M`, an arbitrary type `α`, a constant of `L`, and a function from `α` to `M`, the realization of the term representation of the constant (using the function from `α` to `M`) is equal to the original constant. In other words, it guarantees that interpreting or "realizing" a constant term in a first-order language gives back the constant itself.
More concisely: For any first-order language L, type M, structure σ on M, constant c of L, and function g : α → M, the realization of the constant term for c using g is equal to c itself.
|
FirstOrder.Language.Sentence.realize_not
theorem FirstOrder.Language.Sentence.realize_not :
∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {φ : L.Sentence},
M ⊨ FirstOrder.Language.Formula.not φ ↔ ¬M ⊨ φ
This theorem states that for any first-order language `L` and any `L`-structure `M`, for any sentence `φ` of the language `L`, the structure `M` satisfies the negation of the sentence `φ` (denoted as `M ⊨ FirstOrder.Language.Formula.not φ`) if and only if it is not the case that the structure `M` satisfies the sentence `φ` (denoted as `¬M ⊨ φ`). This is a formalization of the classical logical principle of negation in the context of first-order structures and languages.
More concisely: For any first-order language L and structure M, M satisfies the negation of a sentence φ if and only if φ is not satisfied by M.
|
FirstOrder.Language.Formula.realize_equivSentence_symm_con
theorem FirstOrder.Language.Formula.realize_equivSentence_symm_con :
∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {α : Type u'}
[inst_1 : (L.withConstants α).Structure M] [inst_2 : (L.lhomWithConstants α).IsExpansionOn M]
(φ : (L.withConstants α).Sentence),
((FirstOrder.Language.Formula.equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ M ⊨ φ
This theorem states that for any first-order language `L`, a type `M`, and a type `{α : Type u'}`, given the structures `inst : FirstOrder.Language.Structure L M`, `inst_1 : FirstOrder.Language.Structure (FirstOrder.Language.withConstants L α) M`, and a condition `inst_2 : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L α) M` that the language homomorphism with constants is an expansion on `M`, any sentence `φ` of the language with constants can be realized as a formula (by the inverse function of the bijection `FirstOrder.Language.Formula.equivSentence`) such that the assignment of constants to the formula corresponds to the constant symbols indexed by elements of the parameter set `α`. The theorem further claims that this realization is equivalent to the model `M` satisfying the sentence `φ`. That is, when the variables in the formula are replaced with their corresponding constants from `M`, the formula evaluates to `true` if and only if `M` satisfies `φ`.
More concisely: For any first-order language L, type M, and constant type α, given that the language homomorphism with constants is an expansion on M, any sentence φ of the language with constants can be realized as an equivalent formula in which the constants correspond to elements of α, and this formula holds in M if and only if M satisfies φ.
|
Mathlib.ModelTheory.Semantics._auxLemma.7
theorem Mathlib.ModelTheory.Semantics._auxLemma.7 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, (φ ⊓ ψ).Realize v xs = (φ.Realize v xs ∧ ψ.Realize v xs)
This theorem is about the semantics of first-order logic in the context of Model Theory. Specifically, it states that for any first-order language `L`, a type `M` which is a structure of `L`, a type `α`, a natural number `l`, and two bounded formulas `φ` and `ψ` of `L` with `α` and `l`, the realization of the conjunction of `φ` and `ψ` with respect to a function `v` mapping `α` to `M` and a function `xs` mapping `Fin l` to `M` is equal to the conjunction of the realization of `φ` and the realization of `ψ` with respect to the same `v` and `xs`. In other words, the realization operation respects the logical conjunction operation in the sense that realizing a conjunction of two formulas is the same as realizing each formula individually and then taking the logical conjunction of the results.
More concisely: For any first-order language L, structure M of L, type α, natural number l, bounded formulas φ and ψ of L with α and l, and functions v mapping α to M and xs mapping Fin l to M, the realization of φ ∧ ψ with respect to v and xs equals the realization of φ with respect to v and xs conjuncted with the realization of ψ with respect to v and xs.
|
FirstOrder.Language.Term.realize_relabel
theorem FirstOrder.Language.Term.realize_relabel :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α}
{g : α → β} {v : β → M},
FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.relabel g t) =
FirstOrder.Language.Term.realize (v ∘ g) t
The theorem `FirstOrder.Language.Term.realize_relabel` states that for any first-order language `L`, any type `M`, any instances of the structure of the language `L` on `M`, any types `α` and `β`, any term `t` of the language `L` with variables of type `α`, any function `g` from `α` to `β`, and any valuation function `v` from `β` to `M`, the realization of the term `t` relabeled by the function `g` using the valuation `v` is the same as the realization of the original term `t` using the composition of the valuation `v` and the function `g`. In simpler words, relabeling the variables of a term and then realizing it is the same as first applying the relabeling function to the variables and then realizing the term.
More concisely: For any first-order language L, type M, valuation function v from the type of constants in L to M, function g from the domain of v to the type M, term t of L with variables of type α, the realization of the term t relabeled by g using v is equal to the realization of the original term t using the composition of g and v.
|
Mathlib.ModelTheory.Semantics._auxLemma.4
theorem Mathlib.ModelTheory.Semantics._auxLemma.4 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, φ.not.Realize v xs = ¬φ.Realize v xs
This theorem, named `_auxLemma.4` in the `Mathlib.ModelTheory.Semantics` module, asserts that for any first-order language `L`, any structure `M` of `L`, any type `α`, any natural number `l`, any bounded formula `φ` of `L` with `α` and `l`, any function `v` from `α` to `M`, and any function `xs` from `Fin l` to `M`, the realization of the negation of the bounded formula `φ` with respect to `v` and `xs` is the negation of the realization of `φ` with `v` and `xs`. In simpler terms, it states that negating a formula in a first-order language and realizing it gives the same result as realizing the formula first and then negating the result.
More concisely: For any first-order language L, structure M, type α, natural number l, bounded formula φ of L with variables α and l, functions v : α -> M and xs : Fin l -> M, the realization of the negation of φ with respect to v and xs is equal to the negation of the realization of φ with v and xs.
|
Mathlib.ModelTheory.Semantics._auxLemma.1
theorem Mathlib.ModelTheory.Semantics._auxLemma.1 : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b := by
sorry
This theorem, `Mathlib.ModelTheory.Semantics._auxLemma.1`, states that for any proposition `b` and any type or sort `α` that is nonempty (i.e., there exists at least one element of type `α`), the type of functions from `α` to `b` is equivalent to `b` itself. This theorem is a facet of mathematical logic and model theory.
More concisely: For any nonempty type or sort `α`, the type of functions from `α` to a proposition `b` is equivalent to `b`.
|
FirstOrder.Language.BoundedFormula.realize_rel
theorem FirstOrder.Language.BoundedFormula.realize_rel :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
{k : ℕ} {R : L.Relations k} {ts : Fin k → L.Term (α ⊕ Fin l)},
(R.boundedFormula ts).Realize v xs ↔
FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)
The theorem `FirstOrder.Language.BoundedFormula.realize_rel` states that for any first-order language `L`, any `L`-structure `M`, any function `v` from type `α` to `M`, any function `xs` from `Fin l` to `M` (where `l` is a natural number), any natural number `k`, any `k`-ary relation `R` in `L`, and any function `ts` from `Fin k` to the set of terms in `L` over `α ⊕ Fin l`, the realization of the bounded formula obtained by applying `R` to `ts` using `v` and `xs` is equivalent to the application of the relation map of `R` to the function which maps each element `i` of `Fin k` to the realization of the term `ts i` using the function `Sum.elim v xs`. In simpler terms, this theorem connects the realization of a bounded formula with the realization of terms under a relation in a first-order language structure.
More concisely: For any first-order language L, structure M, function v : α -> M, function xs : Fin l -> M, natural number k, k-ary relation R in L, and function ts : Fin k -> terms(L) over α ⊕ Fin l, the realization of the bounded formula obtained by applying R to ts using v and xs is equivalent to applying the relation map of R to the function that maps i in Fin k to the realization of ts i using Sum.elim v xs.
|
Mathlib.ModelTheory.Semantics._auxLemma.25
theorem Mathlib.ModelTheory.Semantics._auxLemma.25 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, (φ.iff ψ).Realize v xs = (φ.Realize v xs ↔ ψ.Realize v xs)
The theorem `Mathlib.ModelTheory.Semantics._auxLemma.25` states that for any first-order language `L`, any structure `M` of that language, any type `α`, any natural number `l`, any two bounded formulas `φ` and `ψ` of the language `L` with a bound `l`, any function `v` from `α` to `M`, and any function `xs` from the finite set of size `l` to `M`, the realization of the biimplication (iff) between `φ` and `ψ` is equivalent to the biimplication between the realizations of `φ` and `ψ`. In other words, realizing the logical equivalence of two bounded formulas is the same as the logical equivalence of their realizations.
More concisely: For any first-order language L, structure M, type α, natural number l, bounded formulas φ and ψ of L with bound l, function v from α to M, and function xs of size l to M, the realization of the biimplication between φ and ψ under assignments v and xs is equivalent to the biimplication between the realizations of φ and ψ.
|