internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
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
Tactic:
have : Consistent U := hc hUc
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
this : Consistent U
⊢ False
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
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
this : Consistent U
⊢ False
Tactic:
have : ¬Consistent U := (𝓕_consis.of_supset hsU).not_con
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
this✝ : Consistent U
this : ¬Consistent U
⊢ False
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
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
this✝ : Consistent U
this : ¬Consistent U
⊢ False
Tactic:
contradiction
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
this : ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Tactic:
rcases this with ⟨Z, con, ss, hZ⟩
Proof state after:
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Tactic:
exact ⟨Z, con, ss, by intro U conU ssU; simpa using hZ U conU ssU⟩
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
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Tactic:
intro U conU ssU
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
U : Theory α
conU : Consistent U
ssU : Z ⊆ U
⊢ U = Z
Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
U : Theory α
conU : Consistent U
ssU : Z ⊆ U
⊢ U = Z
Tactic:
simpa using hZ U conU ssU
Proof state after:
no goals
Theorem: LO.Propositional.Classical.theory_maximalConsistentTheory_eq
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
⊢ Consistent (theory (maximalConsistentTheory consisT))
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.theory_maximalConsistentTheory_eq
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
⊢ maximalConsistentTheory consisT ⊆ theory (maximalConsistentTheory consisT)
Tactic:
simpa using System.Axiomatized.axm_subset (maximalConsistentTheory consisT)
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT
Tactic:
by_contra A
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
⊢ False
Tactic:
have hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT := by simpa [not_or] using A
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
⊢ False
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
⊢ False
Tactic:
have : Consistent (insert p (maximalConsistentTheory consisT)) :=
  consistent_insert_iff_not_refutable.mpr
    (show ~p ∉ theory (maximalConsistentTheory consisT) from by simpa using hp.2)
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this : Consistent (insert p (maximalConsistentTheory consisT))
⊢ False
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this : Consistent (insert p (maximalConsistentTheory consisT))
⊢ False
Tactic:
have : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT := by
  simp [hp]
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝ : Consistent (insert p (maximalConsistentTheory consisT))
this : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
⊢ False
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝ : Consistent (insert p (maximalConsistentTheory consisT))
this : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
⊢ False
Tactic:
have : insert p (maximalConsistentTheory consisT) = maximalConsistentTheory consisT :=
  maximalConsistentTheory_maximal _ (by assumption) (by simp)
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝¹ : Consistent (insert p (maximalConsistentTheory consisT))
this✝ : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
this : insert p (maximalConsistentTheory consisT) = maximalConsistentTheory consisT
⊢ False
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝¹ : Consistent (insert p (maximalConsistentTheory consisT))
this✝ : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
this : insert p (maximalConsistentTheory consisT) = maximalConsistentTheory consisT
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
⊢ p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
Tactic:
simpa [not_or] using A
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
⊢ ~p ∉ theory (maximalConsistentTheory consisT)
Tactic:
simpa using hp.2
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this : Consistent (insert p (maximalConsistentTheory consisT))
⊢ insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
Tactic:
simp [hp]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝ : Consistent (insert p (maximalConsistentTheory consisT))
this : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
⊢ Consistent (insert p (maximalConsistentTheory consisT))
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝ : Consistent (insert p (maximalConsistentTheory consisT))
this : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊆ insert p (maximalConsistentTheory consisT)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_iff
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
⊢ p ∈ maximalConsistentTheory consisT
Tactic:
have : p ∈ theory (maximalConsistentTheory consisT) := h
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
this : p ∈ theory (maximalConsistentTheory consisT)
⊢ p ∈ maximalConsistentTheory consisT
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_iff
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
this : p ∈ theory (maximalConsistentTheory consisT)
⊢ p ∈ maximalConsistentTheory consisT
Tactic:
simpa using this
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_consistent'
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∈ maximalConsistentTheory consisT → ~p ∉ maximalConsistentTheory consisT
Tactic:
intro h hn
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ False
Theorem: LO.Propositional.Classical.maximalConsistentTheory_consistent'
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ False
Tactic:
have : Inconsistent (maximalConsistentTheory consisT) :=
  System.inconsistent_iff_provable_bot.mpr
    (by prover [mem_maximalConsistentTheory_iff.mp h, mem_maximalConsistentTheory_iff.mp hn])
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.maximalConsistentTheory_consistent'
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
have := this.not_con
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.maximalConsistentTheory_consistent'
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Classical.maximalConsistentTheory_consistent'
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊢! ⊥
Tactic:
prover [mem_maximalConsistentTheory_iff.mp h, mem_maximalConsistentTheory_iff.mp hn]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∉ maximalConsistentTheory consisT ↔ maximalConsistentTheory consisT ⊢! ~p
Tactic:
by_cases hp : p ∈ maximalConsistentTheory consisT <;> simp[hp]
Proof state after:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
⊢ ¬maximalConsistentTheory consisT ⊢! ~p

case neg
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∉ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊢! ~p
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
⊢ ¬maximalConsistentTheory consisT ⊢! ~p
Tactic:
intro bnp
Proof state after:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
⊢ False
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
⊢ False
Tactic:
have : Inconsistent (maximalConsistentTheory consisT) :=
  System.inconsistent_of_provable (by prover [mem_maximalConsistentTheory_iff.mp hp, bnp])
Proof state after:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
have := this.not_con
Proof state after:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
⊢ maximalConsistentTheory consisT ⊢! ⊥
Tactic:
prover [mem_maximalConsistentTheory_iff.mp hp, bnp]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
case neg
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∉ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊢! ~p
Tactic:
exact mem_maximalConsistentTheory_iff.mp
  (by simpa [hp] using mem_or_neg_mem_maximalConsistentTheory (consisT := consisT) p)
Proof state after:
no goals
Theorem: LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∉ maximalConsistentTheory consisT
⊢ ~p ∈ maximalConsistentTheory consisT
Tactic:
simpa [hp] using mem_or_neg_mem_maximalConsistentTheory (consisT := consisT) p
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_and
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT
Tactic:
have : maximalConsistentTheory consisT ⊢! p ⋏ q := mem_maximalConsistentTheory_iff.mp h
Proof state after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_and
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT
Tactic:
exact ⟨mem_maximalConsistentTheory_iff.mpr (by prover [this]),
       mem_maximalConsistentTheory_iff.mpr (by prover [this])⟩
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_and
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ maximalConsistentTheory consisT ⊢! p
Tactic:
prover [this]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.mem_maximalConsistentTheory_and
Proof state before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ maximalConsistentTheory consisT ⊢! q
Tactic:
prover [this]
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
⊢ p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT
Tactic:
by_contra A
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)
⊢ 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)
⊢ False
Tactic:
have b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q := by
  simpa [not_or, not_mem_maximalConsistentTheory_iff] using A
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
⊢ 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
⊢ False
Tactic:
have : Inconsistent (maximalConsistentTheory consisT) :=
  System.inconsistent_of_provable (by prover [b.1, b.2, mem_maximalConsistentTheory_iff.mp h])
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)
⊢ False