internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.satisfiable_iff
Proof state before:
case intro.intro.intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M✝ : Type u_1
inst✝ : Nonempty M✝
s✝ : Structure L M✝
T U : Theory L
M : Type v
i : Nonempty M
s : Structure L M
hT : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T
Tactic:
exact ⟨s.toStruc, hT⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_lMap
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ : Language
L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L₁ μ n
⊢ (Eval s₂ e ε) ((lMap Φ) p) ↔ (Eval (Structure.lMap Φ s₂) e ε) p
Tactic:
induction p using rec' <;>
simp [*, Semiterm.val_lMap, lMap_rel, lMap_nrel, eval_rel, eval_nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.models_lMap
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ : Language
L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
n : ℕ
e : Fin n → M
ε : μ → M
σ : Sentence L₁
⊢ s₂.toStruc ⊧ (lMap Φ) σ ↔ (Structure.lMap Φ s₂).toStruc ⊧ σ
Tactic:
simp [Semantics.Realize, Evalf, eval_lMap]
Proof state after:
no goals
Theorem: LO.FirstOrder.lMap_models_lMap
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
⊢ Theory.lMap Φ T ⊨[Struc L₂] (Semiformula.lMap Φ) σ
Tactic:
intro s hM
Proof state after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
⊢ s ⊧ (Semiformula.lMap Φ) σ
Theorem: LO.FirstOrder.lMap_models_lMap
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
⊢ s ⊧ (Semiformula.lMap Φ) σ
Tactic:
have : (s.struc.lMap Φ).toStruc ⊧ σ :=
  h ⟨fun _ hq => Semiformula.models_lMap.mp <| hM.realize (Set.mem_image_of_mem _ hq)⟩
Proof state after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
this : (Structure.lMap Φ s.struc).toStruc ⊧ σ
⊢ s ⊧ (Semiformula.lMap Φ) σ
Theorem: LO.FirstOrder.lMap_models_lMap
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
this : (Structure.lMap Φ s.struc).toStruc ⊧ σ
⊢ s ⊧ (Semiformula.lMap Φ) σ
Tactic:
exact Semiformula.models_lMap.mpr this
Proof state after:
no goals
Theorem: LO.FirstOrder.ModelsTheory.add_iff
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U : Theory L
⊢ M ⊧ₘ* T + U ↔ M ⊧ₘ* T ∧ M ⊧ₘ* U
Tactic:
simp [Theory.add_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Theory.modelsTheory_onTheory₁
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
T₁ : Theory L₁
⊢ M ⊧ₘ* lMap Φ T₁ ↔ M ⊧ₘ* T₁
Tactic:
simp [Semiformula.models_lMap, Theory.lMap, modelsTheory_iff, @modelsTheory_iff (T := T₁)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.mem_theory_iff
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
σ : Sentence L
⊢ σ ∈ theory L M ↔ M ⊧ₘ σ
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ : Sequent α
⊢  ⊢¹ Δ → Semantics.Valid (Valuation α) (List.disj Δ)
Tactic:
intro d v
Proof state after:
α : Type u_1
Δ : Sequent α
d :  ⊢¹ Δ
v : Valuation α
⊢ v ⊧ List.disj Δ
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ : Sequent α
d :  ⊢¹ Δ
v : Valuation α
⊢ v ⊧ List.disj Δ
Tactic:
induction d
Proof state after:
case axL
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
a✝ : α
⊢ v ⊧ (Formula.atom a✝ :: Formula.natom a✝ :: Δ✝).disj

case verum
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj

case or
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ q✝ : Formula α
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
a_ih✝ : v ⊧ (p✝ :: q✝ :: Δ✝).disj
⊢ v ⊧ (p✝ ⋎ q✝ :: Δ✝).disj

case and
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ q✝ : Formula α
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
a_ih✝¹ : v ⊧ (p✝ :: Δ✝).disj
a_ih✝ : v ⊧ (q✝ :: Δ✝).disj
⊢ v ⊧ (p✝ ⋏ q✝ :: Δ✝).disj

case wk
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ Γ✝ : Sequent α
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
a_ih✝ : v ⊧ List.disj Δ✝
⊢ v ⊧ List.disj Γ✝

case cut
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ : Formula α
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
a_ih✝¹ : v ⊧ (p✝ :: Δ✝).disj
a_ih✝ : v ⊧ (~p✝ :: Δ✝).disj
⊢ v ⊧ Δ✝.disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v ⊧ (Formula.atom a :: Formula.natom a :: Δ).disj
Tactic:
case axL Δ a =>
  simp[List.map_disj]
  by_cases v a <;> simp[*]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj
Tactic:
case verum => simp[List.map_disj]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
d : Derivation (p :: q :: Δ)
ih : v ⊧ (p :: q :: Δ).disj
⊢ v ⊧ (p ⋎ q :: Δ).disj
Tactic:
case or Δ p q d ih =>
  simpa[or_assoc] using ih
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ v ⊧ List.disj Γ
Tactic:
case wk Δ Γ _ ss ih =>
  have : ∃ p ∈ Δ, v ⊧ p := by simpa [List.map_disj] using ih
  rcases this with ⟨p, hp, hvp⟩
  simp [List.map_disj]; exact ⟨p, ss hp, hvp⟩
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v ⊧ (Formula.atom a :: Formula.natom a :: Δ).disj
Tactic:
simp[List.map_disj]
Proof state after:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v.val a ∨ ¬v.val a ∨ ∃ p ∈ Δ, v ⊧ p
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v.val a ∨ ¬v.val a ∨ ∃ p ∈ Δ, v ⊧ p
Tactic:
by_cases v a <;> simp[*]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj
Tactic:
simp[List.map_disj]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
by_cases hv : v ⊧ Δ.disj
Proof state after:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj

case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
simp[hv]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
have : v ⊧ p := by simpa[hv] using ihp
Proof state after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ (p ⋏ q :: Δ).disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
have : v ⊧ q := by simpa[hv] using ihq
Proof state after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : v ⊧ q
⊢ v ⊧ (p ⋏ q :: Δ).disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : v ⊧ q
⊢ v ⊧ (p ⋏ q :: Δ).disj
Tactic:
simp[*]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ p
Tactic:
simpa[hv] using ihp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ q
Tactic:
simpa[hv] using ihq
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
d : Derivation (p :: q :: Δ)
ih : v ⊧ (p :: q :: Δ).disj
⊢ v ⊧ (p ⋎ q :: Δ).disj
Tactic:
simpa[or_assoc] using ih
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ v ⊧ List.disj Γ
Tactic:
have : ∃ p ∈ Δ, v ⊧ p := by simpa [List.map_disj] using ih
Proof state after:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
this : ∃ p ∈ Δ, v ⊧ p
⊢ v ⊧ List.disj Γ
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
this : ∃ p ∈ Δ, v ⊧ p
⊢ v ⊧ List.disj Γ
Tactic:
rcases this with ⟨p, hp, hvp⟩
Proof state after:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ v ⊧ List.disj Γ
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ v ⊧ List.disj Γ
Tactic:
simp [List.map_disj]
Proof state after:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ ∃ p ∈ Γ, v ⊧ p
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case intro.intro
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
p : Formula α
hp : p ∈ Δ
hvp : v ⊧ p
⊢ ∃ p ∈ Γ, v ⊧ p
Tactic:
exact ⟨p, ss hp, hvp⟩
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ ∃ p ∈ Δ, v ⊧ p
Tactic:
simpa [List.map_disj] using ih
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
⊢ v ⊧ Δ.disj
Tactic:
by_cases hv : v ⊧ Δ.disj
Proof state after:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ Δ.disj

case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ Δ.disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case pos
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : v ⊧ Δ.disj
⊢ v ⊧ Δ.disj
Tactic:
simp[hv]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ Δ.disj
Tactic:
have : v ⊧ p := by simpa[hv] using ihp
Proof state after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ Δ.disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ Δ.disj
Tactic:
have : ¬v ⊧ p := by simpa[hv] using ihn
Proof state after:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ v ⊧ Δ.disj
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ v ⊧ Δ.disj
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
⊢ v ⊧ p
Tactic:
simpa[hv] using ihp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.sound
Proof state before:
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (~p :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihn : v ⊧ (~p :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ ¬v ⊧ p
Tactic:
simpa[hv] using ihn
Proof state after:
no goals
Theorem: LO.Propositional.Classical.soundness
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
⊢ T ⊢! p → T ⊨[Valuation α] p
Tactic:
rintro ⟨Γ, hΓ, d⟩ v hT
Proof state after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
⊢ v ⊧ p
Theorem: LO.Propositional.Classical.soundness
Proof state before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
⊢ v ⊧ p
Tactic:
by_contra hv
Proof state after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ False
Theorem: LO.Propositional.Classical.soundness
Proof state before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ False
Tactic:
have : ∀ v : Valuation α, v ⊧ p ∨ ∃ q ∈ Γ, ¬(v ⊧ q) := by
  simpa [Semantics.Valid, List.map_disj] using Derivation.sound (Tait.ofConsRight d)
Proof state after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ False
Theorem: LO.Propositional.Classical.soundness
Proof state before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ False
Tactic:
have : ∃ q ∈ Γ, ¬v ⊧ q := by simpa [hv] using this v
Proof state after:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
this : ∃ q ∈ Γ, ¬v ⊧ q
⊢ False
Theorem: LO.Propositional.Classical.soundness
Proof state before:
case intro.mk
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
this : ∃ q ∈ Γ, ¬v ⊧ q
⊢ False
Tactic:
rcases this with ⟨q, hqΓ, hq⟩
Proof state after:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
⊢ False
Theorem: LO.Propositional.Classical.soundness
Proof state before:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
⊢ False
Tactic:
have : v ⊧ q := hT.realize (hΓ q hqΓ)
Proof state after:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
this : v ⊧ q
⊢ False
Theorem: LO.Propositional.Classical.soundness
Proof state before:
case intro.mk.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this✝ : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
q : Formula α
hqΓ : q ∈ Γ
hq : ¬v ⊧ q
this : v ⊧ q
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Classical.soundness
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
Tactic:
simpa [Semantics.Valid, List.map_disj] using Derivation.sound (Tait.ofConsRight d)
Proof state after:
no goals
Theorem: LO.Propositional.Classical.soundness
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ ∃ q ∈ Γ, ¬v ⊧ q
Tactic:
simpa [hv] using this v
Proof state after:
no goals
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ⋃₀ c ∈ {U | Consistent U}
Tactic:
simp
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ Consistent (⋃₀ c)
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ Consistent (⋃₀ c)
Tactic:
by_contra A
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
⊢ False
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
⊢ False
Tactic:
rcases System.inconsistent_compact.mp (System.not_consistent_iff_inconsistent.mp A) with ⟨𝓕, h𝓕, fin, 𝓕_consis⟩
Proof state after:
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
𝓕 : Theory α
h𝓕 : 𝓕 ⊆ ⋃₀ c
fin : Collection.Finite 𝓕
𝓕_consis : Inconsistent 𝓕
⊢ False
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
𝓕 : Theory α
h𝓕 : 𝓕 ⊆ ⋃₀ c
fin : Collection.Finite 𝓕
𝓕_consis : Inconsistent 𝓕
⊢ False
Tactic:
rcases Set.subset_mem_chain_of_finite c hnc chain (s := 𝓕) fin h𝓕 with ⟨U, hUc, hsU⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
𝓕 : Theory α
h𝓕 : 𝓕 ⊆ ⋃₀ c
fin : Collection.Finite 𝓕
𝓕_consis : Inconsistent 𝓕
U : Set (Formula α)
hUc : U ∈ c
hsU : 𝓕 ⊆ U
⊢ False