internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.provable_iff_of_consistent_of_complete
Proof state before:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
h : ¬T ⊢! ~σ
⊢ T ⊢! σ
Tactic:
exact or_iff_not_imp_right.mp (comp σ) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ
Tactic:
have : Partrec fun σ : Semisentence ℒₒᵣ 1 ↦ (provableFn T (~σ/[⸢σ⸣])).map (fun _ ↦ ()) :=
  Partrec.map
    ((provableFn_partrec T).comp <| Primrec.to_comp
      <| (Semiformula.neg_primrec (L := ℒₒᵣ)).comp
      <| (Semiformula.substs₁_primrec (L := ℒₒᵣ)).comp
        ((Semiterm.Operator.const_primrec (L := ℒₒᵣ)).comp
          <| (Semiterm.Operator.numeral_primrec (L := ℒₒᵣ)).comp .encode) .id)
    (.const ())
Proof state after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ
Tactic:
exact this.of_eq <| by intro σ; ext; simp[←provable_iff_provableFn]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ ∀ (n : Semisentence ℒₒᵣ 1),
    Part.map (fun x => ()) (provableFn T (~[→ ⸢n⸣].hom n)) =
      Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) n) fun x => Part.some ()
Tactic:
intro σ
Proof state after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
⊢ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) =
    Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
⊢ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) =
    Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
Tactic:
ext
Proof state after:
case H
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
a✝ : Unit
⊢ a✝ ∈ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) ↔
    a✝ ∈ Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_re
Proof state before:
case H
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
σ : Semisentence ℒₒᵣ 1
a✝ : Unit
⊢ a✝ ∈ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) ↔
    a✝ ∈ Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
Tactic:
simp[←provable_iff_provableFn]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.diagRefutation_spec
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
σ : Semisentence ℒₒᵣ 1
⊢ T ⊢! [→ ⸢σ⸣].hom ρ ↔ T ⊢! ~[→ ⸢σ⸣].hom σ
Tactic:
simpa[diagRefutation] using pred_representation T (diagRefutation_re T) (x := σ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.undecidable
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ System.Undecidable T γ
Tactic:
have h : T ⊢! γ ↔ T ⊢! ~γ := by simpa using diagRefutation_spec T ρ
Proof state after:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
h : T ⊢! γ ↔ T ⊢! ~γ
⊢ System.Undecidable T γ
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.undecidable
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
h : T ⊢! γ ↔ T ⊢! ~γ
⊢ System.Undecidable T γ
Tactic:
exact
  ⟨fun b ↦ (Gentzen.inconsistent_of_provable_and_refutable! b (h.mp b)).not_con (consistent_of_sigmaOneSound T),
   fun b ↦ (Gentzen.inconsistent_of_provable_and_refutable! (h.mpr b) b).not_con (consistent_of_sigmaOneSound T)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.undecidable
Proof state before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ T ⊢! γ ↔ T ⊢! ~γ
Tactic:
simpa using diagRefutation_spec T ρ
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Ver
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
⊢ Isolated (CanonicalFrame 𝓓).Rel
Tactic:
intro x y hxy
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Ver
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
⊢ False
Tactic:
have : 𝓓 ⊢! □⊥ := ⟨Deduction.maxm (Set.mem_of_subset_of_mem hAx (by simp))⟩
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this : 𝓓 ⊢! □⊥
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Ver
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this : 𝓓 ⊢! □⊥
⊢ False
Tactic:
have := iff_valid_on_canonicalModel_deducible.mpr this x y hxy
Proof state after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this✝ : 𝓓 ⊢! □⊥
this : Satisfies (CanonicalModel 𝓓) y ⊥
⊢ False
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Ver
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
this✝ : 𝓓 ⊢! □⊥
this : Satisfies (CanonicalModel 𝓓) y ⊥
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Ver
Proof state before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : 𝗩𝗲𝗿 ⊆ Ax(𝓓)
x y : (CanonicalFrame 𝓓).World
hxy : (CanonicalFrame 𝓓).Rel x y
⊢ □⊥ ∈ 𝗩𝗲𝗿
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.reducible_of_subset_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
⊢ L₁ ≤ₛ L₂
Tactic:
apply System.reducible_iff.mpr
Proof state after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
⊢ ∀ {f : Formula α}, L₁ ⊢! f → L₂ ⊢! f
Theorem: LO.Modal.Standard.Kripke.reducible_of_subset_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
⊢ ∀ {f : Formula α}, L₁ ⊢! f → L₂ ⊢! f
Tactic:
intro p hp
Proof state after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ L₂ ⊢! p
Theorem: LO.Modal.Standard.Kripke.reducible_of_subset_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ L₂ ⊢! p
Tactic:
apply complete₂.complete
Proof state after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ 𝔽(Ax(L₂)) ⊧ p
Theorem: LO.Modal.Standard.Kripke.reducible_of_subset_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
⊢ 𝔽(Ax(L₂)) ⊧ p
Tactic:
intro F hF
Proof state after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
F : Frame' α
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ⊧ p
Theorem: LO.Modal.Standard.Kripke.reducible_of_subset_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
p : Formula α
hp : L₁ ⊢! p
F : Frame' α
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ⊧ p
Tactic:
exact sound₁.sound hp F $ hs hF
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.reducible_of_definability
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
⊢ L₁ ≤ₛ L₂
Tactic:
apply reducible_of_subset_axiomSetFrameClass
Proof state after:
case hs
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
⊢ ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
Theorem: LO.Modal.Standard.Kripke.reducible_of_definability
Proof state before:
case hs
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
⊢ ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
Tactic:
intro F hF
Proof state after:
case hs
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ∈ 𝔽(Ax(L₁))
Theorem: LO.Modal.Standard.Kripke.reducible_of_definability
Proof state before:
case hs
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ F ∈ 𝔽(Ax(L₁))
Tactic:
apply iff_definability_memAxiomSetFrameClass definability₁ |>.mpr
Proof state after:
case hs
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ P₁ F
Theorem: LO.Modal.Standard.Kripke.reducible_of_definability
Proof state before:
case hs
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs : ∀ {F : Frame}, P₂ F → P₁ F
F : Frame
hF : F ∈ 𝔽(Ax(L₂))
⊢ P₁ F
Tactic:
exact hs $ iff_definability_memAxiomSetFrameClass definability₂ |>.mp hF
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_eq_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₁ =ₛ L₂
Tactic:
apply System.Equiv.antisymm_iff.mpr
Proof state after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₁ ≤ₛ L₂ ∧ L₂ ≤ₛ L₁
Theorem: LO.Modal.Standard.Kripke.equiv_of_eq_axiomSetFrameClass
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₁ ≤ₛ L₂ ∧ L₂ ≤ₛ L₁
Tactic:
constructor
Proof state after:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₁ ≤ₛ L₂

case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₂ ≤ₛ L₁
Theorem: LO.Modal.Standard.Kripke.equiv_of_eq_axiomSetFrameClass
Proof state before:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₁ ≤ₛ L₂

case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₂ ≤ₛ L₁
Tactic:
. apply reducible_of_subset_axiomSetFrameClass hs₁;
Proof state after:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₂ ≤ₛ L₁
Theorem: LO.Modal.Standard.Kripke.equiv_of_eq_axiomSetFrameClass
Proof state before:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₂ ≤ₛ L₁
Tactic:
. apply reducible_of_subset_axiomSetFrameClass hs₂;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_eq_axiomSetFrameClass
Proof state before:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₁ ≤ₛ L₂
Tactic:
apply reducible_of_subset_axiomSetFrameClass hs₁
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_eq_axiomSetFrameClass
Proof state before:
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₂ ≤ₛ L₁
Tactic:
apply reducible_of_subset_axiomSetFrameClass hs₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ =ₛ L₂
Tactic:
apply System.Equiv.antisymm_iff.mpr
Proof state after:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂ ∧ L₂ ≤ₛ L₁
Theorem: LO.Modal.Standard.Kripke.equiv_of_iff_definability
Proof state before:
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂ ∧ L₂ ≤ₛ L₁
Tactic:
constructor
Proof state after:
case left
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₁ ≤ₛ L₂

case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
h : ∀ {F : Frame}, P₁ F ↔ P₂ F
⊢ L₂ ≤ₛ L₁