internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_or
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
have := this.not_con
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_or
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_or
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
⊢ maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q
Tactic:
simpa [not_or, not_mem_maximalConsistentTheory_iff] using A
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_or
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q
⊢ maximalConsistentTheory consisT ⊢! ⊥
Tactic:
prover [b.1, b.2, mem_maximalConsistentTheory_iff.mp h]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
⊢ ∀ ⦃f : Formula α⦄,
    f ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ f
Tactic:
intro p hp
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
Tactic:
induction p using Formula.rec' <;> simp
Proof state after:
case hfalsum
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
⊢ False

case hatom
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.atom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∈ maximalConsistentTheory consisT

case hnatom
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.natom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∉ maximalConsistentTheory consisT

case hand
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p✝ q✝ : Formula α
a✝¹ : p✝ ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p✝
a✝ : q✝ ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q✝
hp : p✝ ⋏ q✝ ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p✝ ∧
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q✝

case hor
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p✝ q✝ : Formula α
a✝¹ : p✝ ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p✝
a✝ : q✝ ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q✝
hp : p✝ ⋎ q✝ ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p✝ ∨
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q✝
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.atom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∈ maximalConsistentTheory consisT
Tactic:
case hatom => simpa
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.natom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∉ maximalConsistentTheory consisT
Tactic:
case hnatom =>
  simpa using maximalConsistentTheory_consistent' hp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
⊢ False
Tactic:
case hfalsum =>
  have : Inconsistent (maximalConsistentTheory consisT) := System.inconsistent_of_provable ⟨System.byAxm hp⟩
  have := this.not_con
  simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋏ q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∧
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Tactic:
case hand p q ihp ihq =>
  exact ⟨ihp (mem_maximalConsistentTheory_and hp).1, ihq (mem_maximalConsistentTheory_and hp).2⟩
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.atom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∈ maximalConsistentTheory consisT
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.natom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∉ maximalConsistentTheory consisT
Tactic:
simpa using maximalConsistentTheory_consistent' hp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
⊢ False
Tactic:
have : Inconsistent (maximalConsistentTheory consisT) := System.inconsistent_of_provable ⟨System.byAxm hp⟩
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
have := this.not_con
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋏ q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∧
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Tactic:
exact ⟨ihp (mem_maximalConsistentTheory_and hp).1, ihq (mem_maximalConsistentTheory_and hp).2⟩
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋎ q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∨
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Tactic:
rcases mem_maximalConsistentTheory_or hp with (hp | hq)
Proof state after:
case inl
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp✝ : p ⋎ q ∈ maximalConsistentTheory consisT
hp : p ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∨
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q

case inr
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋎ q ∈ maximalConsistentTheory consisT
hq : q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∨
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
case inl
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp✝ : p ⋎ q ∈ maximalConsistentTheory consisT
hp : p ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∨
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Tactic:
left
Proof state after:
case inl.h
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp✝ : p ⋎ q ∈ maximalConsistentTheory consisT
hp : p ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
case inl.h
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp✝ : p ⋎ q ∈ maximalConsistentTheory consisT
hp : p ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
Tactic:
exact ihp hp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
case inr
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋎ q ∈ maximalConsistentTheory consisT
hq : q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p ∨
    { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Tactic:
right
Proof state after:
case inr.h
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋎ q ∈ maximalConsistentTheory consisT
hq : q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Theorem: LO.Propositional.Classical.maximalConsistentTheory_satisfiable
Proof state before:
case inr.h
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
ihp : p ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ p
ihq : q ∈ maximalConsistentTheory consisT → { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
hp : p ⋎ q ∈ maximalConsistentTheory consisT
hq : q ∈ maximalConsistentTheory consisT
⊢ { val := fun x => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧ q
Tactic:
exact ihq hq
Proof state after:
no goals
Theorem: LO.Propositional.Classical.satisfiable_of_consistent
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT✝ consisT : Consistent T
⊢ T ⊆ maximalConsistentTheory consisT
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ T ⊨[Valuation α] p → T ⊢! p
Tactic:
suffices Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T) by
  contrapose
  intro hp hs
  have : Semantics.Satisfiable (Valuation α) (insert (~p) T) :=
    this (consistent_insert_iff_not_refutable.mpr $ by simpa)
  rcases this with ⟨v, hv⟩
  have : v ⊧* T := Semantics.RealizeSet.of_subset hv (by simp)
  have : v ⊧ p := hs this
  have : ¬v ⊧ p := by simpa using hv.realize (Set.mem_insert (~p) T)
  contradiction
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
Tactic:
intro consis
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
consis : Consistent (insert (~p) T)
⊢ Semantics.Satisfiable (Valuation α) (insert (~p) T)
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
consis : Consistent (insert (~p) T)
⊢ Semantics.Satisfiable (Valuation α) (insert (~p) T)
Tactic:
exact satisfiable_of_consistent consis
Proof state after:
no goals
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ T ⊨[Valuation α] p → T ⊢! p
Tactic:
contrapose
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ ¬T ⊢! p → ¬T ⊨[Valuation α] p
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ ¬T ⊢! p → ¬T ⊨[Valuation α] p
Tactic:
intro hp hs
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
⊢ False
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
⊢ False
Tactic:
have : Semantics.Satisfiable (Valuation α) (insert (~p) T) :=
  this (consistent_insert_iff_not_refutable.mpr $ by simpa)
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
this : Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ False
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
this : Semantics.Satisfiable (Valuation α) (insert (~p) T)
⊢ False
Tactic:
rcases this with ⟨v, hv⟩
Proof state after:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
⊢ False
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
⊢ False
Tactic:
have : v ⊧* T := Semantics.RealizeSet.of_subset hv (by simp)
Proof state after:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this : v ⊧* T
⊢ False
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this : v ⊧* T
⊢ False
Tactic:
have : v ⊧ p := hs this
Proof state after:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝¹ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this✝ : v ⊧* T
this : v ⊧ p
⊢ False
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝¹ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this✝ : v ⊧* T
this : v ⊧ p
⊢ False
Tactic:
have : ¬v ⊧ p := by simpa using hv.realize (Set.mem_insert (~p) T)
Proof state after:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝² : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this✝¹ : v ⊧* T
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ False
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
case intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝² : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this✝¹ : v ⊧* T
this✝ : v ⊧ p
this : ¬v ⊧ p
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
⊢ T ⊬! ~~p
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
⊢ T ⊆ insert (~p) T
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.completeness!
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
this✝¹ : Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)
hp : ¬T ⊢! p
hs : T ⊨[Valuation α] p
v : Valuation α
hv : v ⊧* insert (~p) T
this✝ : v ⊧* T
this : v ⊧ p
⊢ ¬v ⊧ p
Tactic:
simpa using hv.realize (Set.mem_insert (~p) T)
Proof state after:
no goals
Theorem: LO.System.Necessitation.nec!
Proof state before:
F : Type u_1
inst✝⁵ : StandardModalLogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝² : Classical 𝓢
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : Necessitation 𝓢
⊢ 𝓢 ⊢! p → 𝓢 ⊢! □p
Tactic:
rintro ⟨hp⟩
Proof state after:
case intro
F : Type u_1
inst✝⁵ : StandardModalLogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝² : Classical 𝓢
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : Necessitation 𝓢
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! □p
Theorem: LO.System.Necessitation.nec!
Proof state before:
case intro
F : Type u_1
inst✝⁵ : StandardModalLogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝² : Classical 𝓢
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : Necessitation 𝓢
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! □p
Tactic:
exact ⟨nec hp⟩
Proof state after:
no goals
Theorem: LO.System.Necessitation.multinec!
Proof state before:
F : Type u_1
inst✝⁵ : StandardModalLogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝² : Classical 𝓢
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : Necessitation 𝓢
n : ℕ
⊢ 𝓢 ⊢! p → 𝓢 ⊢! □^[n]p
Tactic:
rintro ⟨hp⟩
Proof state after:
case intro
F : Type u_1
inst✝⁵ : StandardModalLogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝² : Classical 𝓢
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : Necessitation 𝓢
n : ℕ
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! □^[n]p