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

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
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ Consistent (insert (~p) T) → Semantics.Satisfiable (Valuation α) (insert (~p) T)

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
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
consis : Consistent (insert (~p) T)
⊢ Semantics.Satisfiable (Valuation α) (insert (~p) T)

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

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

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

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

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

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

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

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

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

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

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

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