Theorem: LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory (Logic/Propositional/Classical/Basic/Completeness.lean)

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT
Tactic:
by_contra A
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
⊢ False

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
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

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)
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

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]
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

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)
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals