Faithful embeddings among logical systems #
def
LO.Entailment.IsFaithfulEmbedding
{F₁ : Type u_1}
{F₂ : Type u_2}
{S₁ : Type u_4}
{S₂ : Type u_5}
[Entailment S₁ F₁]
[Entailment S₂ F₂]
(𝓢₁ : S₁)
(𝓢₂ : S₂)
(f : F₁ → F₂)
:
Equations
- LO.Entailment.IsFaithfulEmbedding 𝓢₁ 𝓢₂ f = ∀ (φ : F₁), 𝓢₂ ⊢ f φ ↔ 𝓢₁ ⊢ φ
Instances For
class
LO.Entailment.FaithfullyEmbeddable
{F₁ : Type u_1}
{F₂ : Type u_2}
{S₁ : Type u_4}
{S₂ : Type u_5}
[Entailment S₁ F₁]
[Entailment S₂ F₂]
(𝓢₁ : S₁)
(𝓢₂ : S₂)
:
- prop : ∃ (f : F₁ → F₂), IsFaithfulEmbedding 𝓢₁ 𝓢₂ f
Instances
theorem
LO.Entailment.FaithfullyEmbeddable.fun_exists
{F₁ : Type u_1}
{F₂ : Type u_2}
{S₁ : Type u_4}
{S₂ : Type u_5}
[Entailment S₁ F₁]
[Entailment S₂ F₂]
(𝓢₁ : S₁)
(𝓢₂ : S₂)
[FaithfullyEmbeddable 𝓢₁ 𝓢₂]
:
∃ (f : F₁ → F₂), IsFaithfulEmbedding 𝓢₁ 𝓢₂ f
instance
LO.Entailment.FaithfullyEmbeddable.refl
{F₁ : Type u_1}
{S₁ : Type u_4}
[Entailment S₁ F₁]
(𝓢₁ : S₁)
:
FaithfullyEmbeddable 𝓢₁ 𝓢₁
theorem
LO.Entailment.FaithfullyEmbeddable.trans
{F₁ : Type u_1}
{F₂ : Type u_2}
{F₃ : Type u_3}
{S₁ : Type u_4}
{S₂ : Type u_5}
{S₃ : Type u_6}
[Entailment S₁ F₁]
[Entailment S₂ F₂]
[Entailment S₃ F₃]
(𝓢₁ : S₁)
(𝓢₂ : S₂)
(𝓢₃ : S₃)
[FaithfullyEmbeddable 𝓢₁ 𝓢₂]
[FaithfullyEmbeddable 𝓢₂ 𝓢₃]
:
FaithfullyEmbeddable 𝓢₁ 𝓢₃