internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Structure.extendStructure.val_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
k : ℕ
f : L₁.Func k
v : Fin k → Semiterm L₁ μ n
ih : ∀ (a : Fin k), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (v a)) = Semiterm.val s₁ e ε (v a)
⊢ (func (Φ.func f) fun i => Semiterm.val s₁ e ε (v i)) = func f fun i => Semiterm.val s₁ e ε (v i)
Tactic:
case func k f v ih =>
  exact extendStructure.func Φ s₁ (injf k) f (fun i => Semiterm.val s₁ e ε (v i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.val_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
k : ℕ
f : L₁.Func k
v : Fin k → Semiterm L₁ μ n
ih : ∀ (a : Fin k), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (v a)) = Semiterm.val s₁ e ε (v a)
⊢ (func (Φ.func f) fun i => Semiterm.val s₁ e ε (v i)) = func f fun i => Semiterm.val s₁ e ε (v i)
Tactic:
exact extendStructure.func Φ s₁ (injf k) f (fun i => Semiterm.val s₁ e ε (v i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.eval_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L₁ μ n
⊢ (Eval (extendStructure Φ s₁) e ε) ((lMap Φ) p) ↔ (Eval s₁ e ε) p
Tactic:
induction p using Semiformula.rec' <;> simp[*, val_lMap Φ e ε injf s₁, Semiformula.lMap_rel, Semiformula.lMap_nrel, eval_rel, eval_nrel]
Proof state after:
case hrel
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r✝) fun i => Semiterm.val s₁ e ε (v✝ i)) ↔ rel r✝ fun i => Semiterm.val s₁ e ε (v✝ i)

case hnrel
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r✝) fun i => Semiterm.val s₁ e ε (v✝ i)) ↔ ¬rel r✝ fun i => Semiterm.val s₁ e ε (v✝ i)
Theorem: LO.FirstOrder.Structure.extendStructure.eval_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
case hrel k r v =>
exact extendStructure.rel Φ s₁ (injr k) r (fun i => Semiterm.val s₁ e ε (v i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.eval_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
exact extendStructure.rel Φ s₁ (injr k) r (fun i => Semiterm.val s₁ e ε (v i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.eval_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ ¬rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
case hnrel k r v =>
simpa[not_iff_not] using
  extendStructure.rel Φ s₁ (injr k) r (fun i => Semiterm.val s₁ e ε (v i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.eval_lMap
Proof state before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ ¬rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
simpa[not_iff_not] using
  extendStructure.rel Φ s₁ (injr k) r (fun i => Semiterm.val s₁ e ε (v i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.extendStructure.models_lMap
Proof state before:
μ : Sort ?u.144343
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
σ : Sentence L₁
⊢ (extendStructure Φ s₁).toStruc ⊧ (lMap Φ) σ ↔ s₁.toStruc ⊧ σ
Tactic:
simp[Semantics.Realize, Evalf, eval_lMap Φ injf injr]
Proof state after:
no goals
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ ↔ T ⊨ σ
Tactic:
constructor
Proof state after:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ → T ⊨ σ

case mpr
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ T ⊨ σ → Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ → T ⊨ σ
Tactic:
intro h s₁ hs₁
Proof state after:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ s₁ ⊧ σ
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
case mp
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ s₁ ⊧ σ
Tactic:
exact (Structure.extendStructure.models_lMap Φ injf injr s₁.struc σ).mp $ h
  (by simp[Semantics.realizeSet_iff, Theory.lMap, Semantics.models]
      intro σ hσ; exact (Structure.extendStructure.models_lMap (Φ := Φ) injf injr s₁.struc σ).mpr (hs₁.realize hσ))
Proof state after:
no goals
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ (Structure.extendStructure Φ s₁.struc).toStruc ∈ Semantics.models (SmallStruc L₂) (Theory.lMap Φ T)
Tactic:
simp[Semantics.realizeSet_iff, Theory.lMap, Semantics.models]
Proof state after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ ∀ a ∈ T, (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) a
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
⊢ ∀ a ∈ T, (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) a
Tactic:
intro σ hσ
Proof state after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ✝ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ✝
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) σ
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ✝ : Sentence L₁
h : Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ✝
s₁ : SmallStruc L₁
hs₁ : s₁ ∈ Semantics.models (SmallStruc L₁) T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ (Structure.extendStructure Φ s₁.struc).toStruc ⊧ (Semiformula.lMap Φ) σ
Tactic:
exact (Structure.extendStructure.models_lMap (Φ := Φ) injf injr s₁.struc σ).mpr (hs₁.realize hσ)
Proof state after:
no goals
Theorem: LO.FirstOrder.lMap_models_lMap_iff
Proof state before:
case mpr
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
σ : Sentence L₁
⊢ T ⊨ σ → Theory.lMap Φ T ⊨ (Semiformula.lMap Φ) σ
Tactic:
exact lMap_models_lMap
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_lMap
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
s : Satisfiable T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
Tactic:
rcases s with ⟨⟨M, i, s⟩, hM⟩
Proof state after:
case intro.mk
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
Theorem: LO.FirstOrder.satisfiable_lMap
Proof state before:
case intro.mk
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
Tactic:
exact ⟨⟨M, i, s.extendStructure Φ⟩, by
  simp[Semantics.realizeSet_iff]
  intro σ hσ
  exact (Structure.extendStructure.models_lMap Φ injf injr s σ).mpr (hM.realize hσ)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_lMap
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧* ⇑(Semiformula.lMap Φ) '' T
Tactic:
simp[Semantics.realizeSet_iff]
Proof state after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ ∀ a ∈ T, { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) a
Theorem: LO.FirstOrder.satisfiable_lMap
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ ∀ a ∈ T, { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) a
Tactic:
intro σ hσ
Proof state after:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) σ
Theorem: LO.FirstOrder.satisfiable_lMap
Proof state before:
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
σ : Semiformula L₁ Empty 0
hσ : σ ∈ T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) σ
Tactic:
exact (Structure.extendStructure.models_lMap Φ injf injr s σ).mpr (hM.realize hσ)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p : Formula α
d : L ⊢ p
⊢ 𝔽(Ax(L)) ⊧ p
Tactic:
induction d using Deduction.inducition_with_nec with
| hMaxm h => exact validOnAxiomSetFrameClass_axiom h;
| hMdp _ _ ihpq ihp =>
  intro F hF V w;
  exact Satisfies.mdp (ihpq F hF V w) (ihp F hF V w);
| hNec _ ih =>
  intro F hF V w w' _;
  exact ih F hF V w';
| hDisj₃ =>
  simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel];
  intros; rename_i hpr hqr hpq;
  cases hpq with
  | inl hp => exact hpr hp;
  | inr hq => exact hqr hq;
| _ => simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel];
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hMaxm
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
h : p✝ ∈ Ax(L)
⊢ 𝔽(Ax(L)) ⊧ p✝
Tactic:
exact validOnAxiomSetFrameClass_axiom h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
⊢ 𝔽(Ax(L)) ⊧ q✝
Tactic:
intro F hF V w
Proof state after:
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ q✝
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ q✝
Tactic:
exact Satisfies.mdp (ihpq F hF V w) (ihp F hF V w)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
⊢ 𝔽(Ax(L)) ⊧ □p✝
Tactic:
intro F hF V w w' _
Proof state after:
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
w' : { Frame := F, Valuation := V }.Frame.World
a✝ : w ≺ w'
⊢ Satisfies { Frame := F, Valuation := V } w' p✝
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
w' : { Frame := F, Valuation := V }.Frame.World
a✝ : w ≺ w'
⊢ Satisfies { Frame := F, Valuation := V } w' p✝
Tactic:
exact ih F hF V w'
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ 𝔽(Ax(L)) ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel]
Proof state after:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ ∀ F ∈ 𝔽(Ax(L)),
    ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
      (Satisfies { Frame := F, Valuation := V } w p✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
        (Satisfies { Frame := F, Valuation := V } w q✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
          Satisfies { Frame := F, Valuation := V } w p✝ ∨ Satisfies { Frame := F, Valuation := V } w q✝ →
            Satisfies { Frame := F, Valuation := V } w r✝
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ ∀ F ∈ 𝔽(Ax(L)),
    ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
      (Satisfies { Frame := F, Valuation := V } w p✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
        (Satisfies { Frame := F, Valuation := V } w q✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
          Satisfies { Frame := F, Valuation := V } w p✝ ∨ Satisfies { Frame := F, Valuation := V } w q✝ →
            Satisfies { Frame := F, Valuation := V } w r✝
Tactic:
intros
Proof state after:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝³ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
a✝² : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝¹ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝³ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
a✝² : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝¹ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
rename_i hpr hqr hpq
Proof state after:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hpq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hpq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
cases hpq with
| inl hp => exact hpr hp;
| inr hq => exact hqr hq;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDisj₃.inl
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hp : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
exact hpr hp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDisj₃.inr
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
Tactic:
exact hqr hq
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.sound_on_frameclass
Proof state before:
case hDne
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
⊢ 𝔽(Ax(L)) ⊧ ~~p✝ ⟶ p✝
Tactic:
simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.unprovable_bot
Proof state before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FrameClass.IsNonempty 𝔽(Ax(L))
⊢ L ⊬! ⊥
Tactic:
intro h
Proof state after:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FrameClass.IsNonempty 𝔽(Ax(L))
h : L ⊢! ⊥
⊢ False
Theorem: LO.Modal.Standard.Kripke.unprovable_bot
Proof state before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FrameClass.IsNonempty 𝔽(Ax(L))
h : L ⊢! ⊥
⊢ False
Tactic:
obtain ⟨F, hF⟩ := ne
Proof state after:
case mk.intro
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
h : L ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(L))
⊢ False
Theorem: LO.Modal.Standard.Kripke.unprovable_bot
Proof state before:
case mk.intro
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
h : L ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(L))
⊢ False
Tactic:
simpa using sound!_on_frameclass h F hF
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.unprovable_bot_finite
Proof state before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FiniteFrameClass.IsNonempty 𝔽ꟳ(Ax(L))
⊢ L ⊬! ⊥
Tactic:
intro h
Proof state after:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FiniteFrameClass.IsNonempty 𝔽ꟳ(Ax(L))
h : L ⊢! ⊥
⊢ False
Theorem: LO.Modal.Standard.Kripke.unprovable_bot_finite
Proof state before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FiniteFrameClass.IsNonempty 𝔽ꟳ(Ax(L))
h : L ⊢! ⊥
⊢ False
Tactic:
obtain ⟨F, hF⟩ := ne
Proof state after:
case mk.intro
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
h : L ⊢! ⊥
F : FiniteFrame
hF : F ∈ 𝔽ꟳ(Ax(L))
⊢ False
Theorem: LO.Modal.Standard.Kripke.unprovable_bot_finite
Proof state before:
case mk.intro
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
h : L ⊢! ⊥
F : FiniteFrame
hF : F ∈ 𝔽ꟳ(Ax(L))
⊢ False
Tactic:
simpa using sound!_on_frameclass h F.toFrame hF
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.neg_neg
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
⊢ p.neg.neg = p
Tactic:
induction p <;> simp[*, neg]
Proof state after:
no goals