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

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

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

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

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

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

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

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

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

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⟩
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
have := this.not_con
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False

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

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

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

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

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

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

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