internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
case intro.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p
Tactic:
existsi λ w a => V₂ (f w) a, w₁
Proof state after:
case intro.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
case intro.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p
Tactic:
subst e
Proof state after:
case intro.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
case intro.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p
Tactic:
exact Satisfies.morphism ({
  forth := by intro w v hwv; apply hMorF.forth hwv,
  back := by intro w v h; apply hMorF.back h,
  atomic := by simp_all;
}) |>.not.mpr h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ¬F₂ ⊧ p
⊢ ?m.13927
Tactic:
simpa [ValidOnFrame, ValidOnModel] using h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ w₁, f w₁ = w₂
Tactic:
apply hSur
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w v : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World}, w ≺ v → f w ≺ f v
Tactic:
intro w v hwv
Proof state after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w v : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
hwv : w ≺ v
⊢ f w ≺ f v
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w v : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
hwv : w ≺ v
⊢ f w ≺ f v
Tactic:
apply hMorF.forth hwv
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World}
    {v : { Frame := F₂, Valuation := V₂ }.Frame.World}, f w ≺ v → ∃ u, w ≺ u ∧ f u = v
Tactic:
intro w v h
Proof state after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝¹ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h✝ : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
v : { Frame := F₂, Valuation := V₂ }.Frame.World
h : f w ≺ v
⊢ ∃ u, w ≺ u ∧ f u = v
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝¹ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h✝ : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
v : { Frame := F₂, Valuation := V₂ }.Frame.World
h : f w ≺ v
⊢ ∃ u, w ≺ u ∧ f u = v
Tactic:
apply hMorF.back h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.World} {a : α},
    { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Valuation w a ↔
      { Frame := F₂, Valuation := V₂ }.Valuation (f w) a
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ F₁ ⊧* T → F₂ ⊧* T
Tactic:
simp only [Semantics.realizeSet_iff]
Proof state after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ (∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f) → ∀ ⦃f : Formula α⦄, f ∈ T → F₂ ⊧ f
Theorem: LO.Modal.Standard.Theory.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ (∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f) → ∀ ⦃f : Formula α⦄, f ∈ T → F₂ ⊧ f
Tactic:
intro h p hp
Proof state after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p✝ : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f
p : Formula α
hp : p ∈ T
⊢ F₂ ⊧ p
Theorem: LO.Modal.Standard.Theory.Kripke.ValidOnFrame.morphism
Proof state before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p✝ : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f
p : Formula α
hp : p ∈ T
⊢ F₂ ⊧ p
Tactic:
exact Formula.Kripke.ValidOnFrame.morphism hSur hMorF (h hp)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
⊢ ¬∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
Tactic:
by_contra hC
Proof state after:
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
hC : ∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
hC : ∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False
Tactic:
obtain ⟨Ax, h⟩ := hC
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False
Tactic:
let F₁ : Frame' α := { World := Unit ⊕ Unit, Rel := λ w v => w ≠ v }
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
⊢ False
Tactic:
have hIF₁ : Irreflexive F₁.Rel' := by exact f;
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
⊢ False
Tactic:
let F₂ : Frame' α := { World := Unit, Rel := λ w v => w = v }
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ False
Tactic:
have hIF₂ : ¬Irreflexive F₂.Rel' := by simp [Irreflexive]; existsi (); trivial;
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
⊢ False
Tactic:
let f : F₁.World → F₂.World := λ _ => ()
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
⊢ False
Tactic:
have hSur : Function.Surjective f := by simp [Function.Surjective];
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ False
Tactic:
have hMorF : Frame.pMorphism F₁ F₂ f := {
  forth := by aesop;
  back := by
    simp [F₁, F₂];
    constructor;
    . intro a; right; exists (); intro; contradiction;
    . intro a; left; use (); intro; contradiction;
}
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ False
Tactic:
have : Irreflexive F₂.Rel := h.mpr $ Theory.Kripke.ValidOnFrame.morphism hSur hMorF (h.mp hIF₁)
Proof state after:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
this : Irreflexive F₂.Rel
⊢ False
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
this : Irreflexive F₂.Rel
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
⊢ Irreflexive Frame.Rel'
Tactic:
exact f
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ ¬Irreflexive Frame.Rel'
Tactic:
simp [Irreflexive]
Proof state after:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ ∃ x, x ≺ x
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ ∃ x, x ≺ x
Tactic:
existsi ()
Proof state after:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ () ≺ ()
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
⊢ () ≺ ()
Tactic:
trivial
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
⊢ Function.Surjective f
Tactic:
simp [Function.Surjective]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ {w v : F₁.World}, w ≺ v → f w ≺ f v
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.undefinability_irreflexive
Proof state before:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ ∀ {w : F₁.World} {v : F₂.World}, f w ≺ v → ∃ u, w ≺ u ∧ f u = v
Tactic:
simp [F₁, F₂]
Proof state after:
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
⊢ (∀ (a : Unit), (∃ a_1, Sum.inl a ≺ Sum.inl a_1) ∨ ∃ b, Sum.inl a ≺ Sum.inr b) ∧
    ∀ (b : Unit), (∃ a, Sum.inr b ≺ Sum.inl a) ∨ ∃ b_1, Sum.inr b ≺ Sum.inr b_1