FirstOrder.Language.LHom.comp_onTerm
theorem FirstOrder.Language.LHom.comp_onTerm :
∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {L'' : FirstOrder.Language} (φ : L'.LHom L'')
(ψ : L.LHom L'), (φ.comp ψ).onTerm = φ.onTerm ∘ ψ.onTerm
The theorem `FirstOrder.Language.LHom.comp_onTerm` states that for any three first-order languages `L`, `L'`, and `L''` and any two language homomorphisms `φ : L' →ᴸ L''` and `ψ : L →ᴸ L'`, the composition of `φ` and `ψ` when applied to a term is equivalent to first applying `ψ` to the term, and then applying `φ` to the resulting term. This is an assertion of the commutativity of the `onTerm` function with the composition operation for language homomorphisms.
More concisely: For any first-order languages $L$, $L'$, $L''$, and homomorphisms $\varphi : L' \rightarrow L''$ and $\psi : L \rightarrow L'$, we have $\varphi \circ \psi (t) = \varphi ( \psi (t))$ for all terms $t$ in $L$.
|
FirstOrder.Language.BoundedFormula.castLE.proof_2
theorem FirstOrder.Language.BoundedFormula.castLE.proof_2 : ∀ (_m _n : ℕ), _m ≤ _n → _m + 1 ≤ _n + 1
This theorem states that for any two natural numbers, `_m` and `_n`, if `_m` is less than or equal to `_n`, then `_m + 1` is also less than or equal to `_n + 1`. This property is fundamental to the order-preserving nature of natural number arithmetic.
More concisely: For all natural numbers m and n, if m ≤ n then m + 1 ≤ n + 1.
|
FirstOrder.Language.BoundedFormula.castLE_rfl
theorem FirstOrder.Language.BoundedFormula.castLE_rfl :
∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (h : n ≤ n) (φ : L.BoundedFormula α n),
FirstOrder.Language.BoundedFormula.castLE h φ = φ
This theorem states that for any first-order language `L`, type `α`, and natural number `n`, if we have a proof `h` that `n` is less than or equal to `n` itself (which is always true by reflexivity), then the effect of casting a bounded formula `φ` of `L` with the bound `n` using `h` is a no-op. That is, `FirstOrder.Language.BoundedFormula.castLE h φ` is identical to the original formula `φ`. This asserts the reflexivity of the cast operation under the condition of equality in the language `L`.
More concisely: For any first-order language `L`, type `α`, and bounded formula `φ` of `L` with bound `n`, if `n` equals `n`, then casting `φ` with `n` using a reflexivity proof is a no-op.
|
FirstOrder.Language.BoundedFormula.isQF_bot
theorem FirstOrder.Language.BoundedFormula.isQF_bot : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, ⊥.IsQF := by
sorry
This theorem states that, for any first-order language `L`, any type `α`, and any natural number `n`, the bottom (falsum) of the set of bounded formulas in `L` is quantifier-free. In the context of first-order logic, a formula is quantifier-free (QF) if it doesn't contain any universal or existential quantifiers. The symbol `⊥` represents the logical constant for "false". This theorem thus asserts a very basic fact about the structure of logical formulas.
More concisely: In any first-order language, the bottom formula is quantifier-free.
|
FirstOrder.Language.BoundedFormula.IsAtomic.isQF
theorem FirstOrder.Language.BoundedFormula.IsAtomic.isQF :
∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsAtomic → φ.IsQF
This theorem states that for any first-order language `L`, any type `α`, and any natural number `n`, if a bounded formula `φ` in the language `L` with `α` and `n` is atomic, then it is also quantifier-free (QF). In other words, every atomic bounded formula in a given first-order language does not contain any quantifiers.
More concisely: For any first-order language L, any type α, and natural number n, every atomic bounded formula φ(α, n) in L is quantifier-free.
|
FirstOrder.Language.LHom.id_onTerm
theorem FirstOrder.Language.LHom.id_onTerm :
∀ {L : FirstOrder.Language} {α : Type u'}, (FirstOrder.Language.LHom.id L).onTerm = id
The theorem `FirstOrder.Language.LHom.id_onTerm` states that for any first-order language `L` and any type `α`, the function `FirstOrder.Language.LHom.onTerm` applied to the identity language homomorphism of `L` is the identity function. In other words, the identity language homomorphism leaves all terms of the language unchanged when applied via the `onTerm` function.
More concisely: For any first-order language L and type α, the identity language homomorphism's `onTerm` application is the identity function on L's terms.
|
FirstOrder.Language.BoundedFormula.IsQF.isPrenex
theorem FirstOrder.Language.BoundedFormula.IsQF.isPrenex :
∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsPrenex
This theorem states that for any first-order language `L`, any type `α`, any natural number `n`, and any bounded formula `φ` in the language `L` with `α` and `n`, if `φ` is a quantifier-free (QF) formula, then `φ` is in prenex form. Prenex form is a logical form of a formula where all quantifiers are at the front. Hence, this theorem asserts that all quantifier-free formulas in a first-order language are in prenex form.
More concisely: In a first-order language, all quantifier-free formulas are equivalent to formulas in prenex normal form.
|
FirstOrder.Language.Term.relabel_relabel
theorem FirstOrder.Language.Term.relabel_relabel :
∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_3} (f : α → β) (g : β → γ) (t : L.Term α),
FirstOrder.Language.Term.relabel g (FirstOrder.Language.Term.relabel f t) =
FirstOrder.Language.Term.relabel (g ∘ f) t
The theorem `FirstOrder.Language.Term.relabel_relabel` states that for any first-order language `L`, types `α`, `β`, and `γ`, a function `f` from `α` to `β`, a function `g` from `β` to `γ`, and a term `t` in the language `L` with variables of type `α`, the operation of relabeling (renaming) variables in `t` first with `f` and then with `g` is the same as relabeling the variables in `t` once with the composition of the functions `g ∘ f`. This is a property of the `relabel` function in the context of first-order logic terms, and relates to the idea that the renaming of variables should be consistent, regardless of whether it's done in stages or all at once.
More concisely: For any first-order language L, functions f: α → β and g: β → γ, and term t in L with variables of type α, the operation of relabeling variables in t first with f and then with g equals relabeling variables in t once with the composition g ∘ f.
|
FirstOrder.Language.Term.relabel_id_eq_id
theorem FirstOrder.Language.Term.relabel_id_eq_id :
∀ {L : FirstOrder.Language} {α : Type u'}, FirstOrder.Language.Term.relabel id = id
This theorem states that for any first-order language `L` and any type `α`, the relabeling of a term in `L` with the identity function (`id`) is equivalent to the identity operation. In other words, performing a relabel operation on a term where each element is mapped to itself (which is what the identity function does) leaves the term unchanged. Hence, `relabel id` and `id` are the same for any term in any first-order language.
More concisely: For any first-order language and type, the relabeling of terms with the identity function equals the identity operation.
|