Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
⊢ (𝓓)-Consistent (Ax(𝓓), ∅)
Tactic:
intro Γ Δ hΓ hΔ
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : ∀ p ∈ Δ, p ∈ (Ax(𝓓), ∅).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : ∀ p ∈ Δ, p ∈ (Ax(𝓓), ∅).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
replace hΔ : Δ = [] := List.nil_iff.mpr hΔ
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
obtain ⟨q, hq⟩ := h.exists_unprovable
State after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
by_contra hC
State after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False

State before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! q := by
  subst hΔ;
  simp [List.disj'_nil] at hC;
  exact imp_trans! hC efq! ⨀ (by
    apply iff_provable_list_conj.mpr;
    exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩;
  );
State after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! q
⊢ False

State before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! q
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ 𝓓 ⊢! q
Tactic:
subst hΔ
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ [].disj'
⊢ 𝓓 ⊢! q

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ [].disj'
⊢ 𝓓 ⊢! q
Tactic:
simp [List.disj'_nil] at hC
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! q

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! q
Tactic:
exact imp_trans! hC efq! ⨀ (by
  apply iff_provable_list_conj.mpr;
  exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩;
)
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! Γ.conj'
Tactic:
apply iff_provable_list_conj.mpr
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, 𝓓 ⊢! p

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, 𝓓 ⊢! p
Tactic:
exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩
State after:
no goals