internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
⊢ ∀ {F : Frame' α}, F ∈ 𝔽(Ax(𝓓)) → F ⊧ p
Tactic:
intro F hF
Proof state after:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ p
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ p
Tactic:
induction d with
| eaxm h => exact validOnAxiomSetFrameClass_axiom h hF;
| mdp _ _ ihpq ihp => exact ValidOnFrame.mdp ihpq ihp;
| _ =>
  intros;
  first
  | apply ValidOnFrame.verum
  | apply ValidOnFrame.imply₁
  | apply ValidOnFrame.imply₂
  | apply ValidOnFrame.disj₁
  | apply ValidOnFrame.disj₂
  | apply ValidOnFrame.disj₃
  | apply ValidOnFrame.conj₁
  | apply ValidOnFrame.conj₂
  | apply ValidOnFrame.conj₃
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case eaxm
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ : Formula α
h : p✝ ∈ Ax(𝓓)
⊢ F ⊧ p✝
Tactic:
exact validOnAxiomSetFrameClass_axiom h hF
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case mdp
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
a✝¹ : Deduction 𝓓 (p✝ ⟶ q✝)
a✝ : Deduction 𝓓 p✝
ihpq : F ⊧ p✝ ⟶ q✝
ihp : F ⊧ p✝
⊢ F ⊧ q✝
Tactic:
exact ValidOnFrame.mdp ihpq ihp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case disj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
first
| apply ValidOnFrame.verum
| apply ValidOnFrame.imply₁
| apply ValidOnFrame.imply₂
| apply ValidOnFrame.disj₁
| apply ValidOnFrame.disj₂
| apply ValidOnFrame.disj₃
| apply ValidOnFrame.conj₁
| apply ValidOnFrame.conj₂
| apply ValidOnFrame.conj₃
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case verum
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ ⊤
Tactic:
apply ValidOnFrame.verum
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case imply₁
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply ValidOnFrame.imply₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case imply₂
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply ValidOnFrame.imply₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case disj₁
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply ValidOnFrame.disj₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case disj₂
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply ValidOnFrame.disj₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case disj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply ValidOnFrame.disj₃
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case conj₁
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply ValidOnFrame.conj₁
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case conj₂
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply ValidOnFrame.conj₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.sound
Proof state before:
case conj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ : Formula α
⊢ F ⊧ p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply ValidOnFrame.conj₃
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Kripke.unprovable_bot
Proof state before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
ne : IsNonempty 𝔽(Ax(𝓓))
⊢ 𝓓 ⊬! ⊥
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
ne : IsNonempty 𝔽(Ax(𝓓))
h : 𝓓 ⊢! ⊥
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.unprovable_bot
Proof state before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
ne : IsNonempty 𝔽(Ax(𝓓))
h : 𝓓 ⊢! ⊥
⊢ False
Tactic:
obtain ⟨F, hF⟩ := ne
Proof state after:
case mk.intro
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
h : 𝓓 ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(𝓓))
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Kripke.unprovable_bot
Proof state before:
case mk.intro
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
h : 𝓓 ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(𝓓))
⊢ False
Tactic:
simpa using sound! h hF
Proof state after:
no goals
Theorem: LO.FirstOrder.completeness_of_encodable
Proof state before:
L : Language
T : Theory L
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
σ : Sentence L
h : T ⊨ σ
⊢ T ⊢! σ
Tactic:
have : T ⊢'' [Rew.emb.hom σ] :=
  Disjconseq.completeness_of_encodable (T := T) (Γ := {σ}) (fun M i s hM ↦ ⟨σ, List.mem_of_mem_head? rfl, h hM⟩)
Proof state after:
L : Language
T : Theory L
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
σ : Sentence L
h : T ⊨ σ
this : T ⊢'' [Rew.emb.hom σ]
⊢ T ⊢! σ
Theorem: LO.FirstOrder.completeness_of_encodable
Proof state before:
L : Language
T : Theory L
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
σ : Sentence L
h : T ⊨ σ
this : T ⊢'' [Rew.emb.hom σ]
⊢ T ⊢! σ
Tactic:
exact ⟨toProof this⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
⊢ T ⊢! σ
Tactic:
letI := Classical.typeDecidableEq
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ T ⊢! σ
Tactic:
have : ∃ u : Finset (Sentence L), ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable (u : Theory L) := by
  simpa using (compact (T := insert (~σ) T)).not.mp (Semantics.consequence_iff_not_satisfiable.mp h)
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
this : ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
this : ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
Tactic:
choose u hu using this
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
hu : ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
hu : ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
Tactic:
rcases hu with ⟨ssu, hu⟩
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
⊢ T ⊢! σ
Tactic:
haveI : ∀ k, Encodable ((languageFinset u).Func k) := fun _ ↦ Fintype.toEncodable _
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this : (k : ℕ) → Encodable ((languageFinset u).Func k)
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this : (k : ℕ) → Encodable ((languageFinset u).Func k)
⊢ T ⊢! σ
Tactic:
haveI : ∀ k, Encodable ((languageFinset u).Rel k) := fun _ ↦ Fintype.toEncodable _
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
⊢ T ⊢! σ
Tactic:
let u' : Finset (Sentence (languageFinset u)) := Finset.imageOfFinset u (fun _ hσ ↦ toSubLanguageFinsetSelf hσ)
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ T ⊢! σ
Tactic:
have image_u' : u'.image (Semiformula.lMap L.ofSubLanguage) = u := by
  ext τ; simp [u', Finset.mem_imageOfFinset_iff]
  exact ⟨by rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩; simp[hτ],
    by intro hτ; exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩⟩
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ T ⊢! σ
Tactic:
have : ¬Satisfiable (u' : Theory (languageFinset u)) := by
  intro h
  have : Satisfiable (u : Theory L) := by
    rw[←image_u']
    simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
  contradiction
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this : ¬Satisfiable ↑u'
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this : ¬Satisfiable ↑u'
⊢ T ⊢! σ
Tactic:
have : System.Inconsistent (u' : Theory (languageFinset u)) := Complete.inconsistent_of_unsatisfiable this
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ T ⊢! σ
Tactic:
have : System.Inconsistent (u : Theory L) := by rw[←image_u']; simpa using System.inconsistent_lMap L.ofSubLanguage this
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁴ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝² : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝¹ : ¬Satisfiable ↑u'
this✝ : System.Inconsistent ↑u'
this : System.Inconsistent ↑u
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁴ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝² : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝¹ : ¬Satisfiable ↑u'
this✝ : System.Inconsistent ↑u'
this : System.Inconsistent ↑u
⊢ T ⊢! σ
Tactic:
have : System.Inconsistent (insert (~σ) T) := this.of_supset ssu
Proof state after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁵ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝⁴ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝² : ¬Satisfiable ↑u'
this✝¹ : System.Inconsistent ↑u'
this✝ : System.Inconsistent ↑u
this : System.Inconsistent (insert (~σ) T)
⊢ T ⊢! σ
Theorem: LO.FirstOrder.complete
Proof state before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁵ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝⁴ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝² : ¬Satisfiable ↑u'
this✝¹ : System.Inconsistent ↑u'
this✝ : System.Inconsistent ↑u
this : System.Inconsistent (insert (~σ) T)
⊢ T ⊢! σ
Tactic:
exact Gentzen.provable_iff_inconsistent.mpr this
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
Tactic:
simpa using (compact (T := insert (~σ) T)).not.mp (Semantics.consequence_iff_not_satisfiable.mp h)
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
Tactic:
ext τ
Proof state after:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ τ ∈ Finset.image (⇑(lMap L.ofSubLanguage)) u' ↔ τ ∈ u
Theorem: LO.FirstOrder.complete
Proof state before:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ τ ∈ Finset.image (⇑(lMap L.ofSubLanguage)) u' ↔ τ ∈ u
Tactic:
simp [u', Finset.mem_imageOfFinset_iff]
Proof state after:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ (∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ) ↔ τ ∈ u
Theorem: LO.FirstOrder.complete
Proof state before:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ (∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ) ↔ τ ∈ u
Tactic:
exact ⟨by rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩; simp[hτ],
  by intro hτ; exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ (∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ) → τ ∈ u
Tactic:
rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩
Proof state after:
case intro.intro.intro.intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Sentence L
hτ : τ ∈ u
⊢ (lMap L.ofSubLanguage) (toSubLanguageFinsetSelf hτ) ∈ u
Theorem: LO.FirstOrder.complete
Proof state before:
case intro.intro.intro.intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Sentence L
hτ : τ ∈ u
⊢ (lMap L.ofSubLanguage) (toSubLanguageFinsetSelf hτ) ∈ u
Tactic:
simp[hτ]
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ τ ∈ u → ∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ
Tactic:
intro hτ
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
hτ : τ ∈ u
⊢ ∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ