internlm/Lean-Github huggingface dataset:
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
s2 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ →' ⊥'
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Tactic:
have s3 := MP s2 s1
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
s2 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ →' ⊥'
s3 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
s2 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ →' ⊥'
s3 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ ⊥'
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.DNI
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ
⊢ Γ ∪ {φ} ∪ {φ →' ⊥'} ⊢ φ →' ⊥'
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ⊢ (φ →' ¬'φ) →' ¬'φ
Tactic:
simp [deduction]
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥' := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s3 := MP s1 s2
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
s3 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
s3 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s4 := MP s3 s2
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
s3 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' ⊥'
s4 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
s2 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
s3 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' ⊥'
s4 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.CM₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ →' φ →' ⊥'
⊢ Γ ∪ {φ →' φ →' ⊥'} ∪ {φ} ⊢ φ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.RAA
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ⊢ (φ →' ⊥') →' ¬'φ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ⊢ (φ →' ψ) →' ¬'ψ →' ¬'φ
Tactic:
simp [deduction]
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥' := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s4 := MP s2 s1
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
have s5 := MP s3 s4
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
s5 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
s3 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ
s5 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ⊥'
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₁
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ φ →' ψ
⊢ Γ ∪ {φ →' ψ} ∪ {ψ →' ⊥'} ∪ {φ} ⊢ ψ →' ⊥'
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ⊢ (φ →' ¬'ψ) →' ψ →' ¬'φ
Tactic:
simp [deduction]
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥' := by simp;
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s4 := MP s3 s1
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
have s5 := MP s4 s2
Proof state after:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
s5 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
s3 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
s4 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ →' ⊥'
s5 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ⊥'
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM₀.Con₂
Proof state before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Context L
φ ψ χ : L
s1 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ
s2 : Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ ψ
⊢ Γ ∪ {φ →' ψ →' ⊥'} ∪ {ψ} ∪ {φ} ⊢ φ →' ψ →' ⊥'
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.stronger
Proof state before:
L : Type u
inst✝⁷ : DecidableEq L
inst✝⁶ : HilbertSystem L
inst✝⁵ : HasBot L
inst✝⁴ : HasArrow L
inst✝³ : HasLnot L
inst✝² : HasLor L
inst✝¹ : HasLand L
inst✝ : HasLiff L
⊢ HPJ L → HPK L
Tactic:
admit
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.IDisj₁
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
⊢ (Γ ⊢ φ₁) → (Γ ⊢ φ₁ ∨' φ₂)
Tactic:
intro h
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₁
⊢ Γ ⊢ φ₁ ∨' φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.IDisj₁
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₁
⊢ Γ ⊢ φ₁ ∨' φ₂
Tactic:
exact MP (axiomIDisj₁ _ _ _) h
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.IDisj₂
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
⊢ (Γ ⊢ φ₂) → (Γ ⊢ φ₁ ∨' φ₂)
Tactic:
intro h
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₂
⊢ Γ ⊢ φ₁ ∨' φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.IDisj₂
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₂
⊢ Γ ⊢ φ₁ ∨' φ₂
Tactic:
exact MP (axiomIDisj₂ _ _ _) h
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.EDisj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
χ φ ψ : L
⊢ (Γ ⊢ φ →' χ) → (Γ ⊢ ψ →' χ) → (Γ ⊢ φ ∨' ψ →' χ)
Tactic:
intro hφ hψ
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
χ φ ψ : L
hφ : Γ ⊢ φ →' χ
hψ : Γ ⊢ ψ →' χ
⊢ Γ ⊢ φ ∨' ψ →' χ
Theorem: PropositionalLogic.HilbertSystem.HPM.EDisj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
χ φ ψ : L
hφ : Γ ⊢ φ →' χ
hψ : Γ ⊢ ψ →' χ
⊢ Γ ⊢ φ ∨' ψ →' χ
Tactic:
exact MP (MP (axiomEDisj _ _ _ _) hφ) hψ
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.IConj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ ψ : L
⊢ (Γ ⊢ φ) → (Γ ⊢ ψ) → (Γ ⊢ φ ∧' ψ)
Tactic:
intro hφ hψ
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ ψ : L
hφ : Γ ⊢ φ
hψ : Γ ⊢ ψ
⊢ Γ ⊢ φ ∧' ψ
Theorem: PropositionalLogic.HilbertSystem.HPM.IConj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ ψ : L
hφ : Γ ⊢ φ
hψ : Γ ⊢ ψ
⊢ Γ ⊢ φ ∧' ψ
Tactic:
exact MP (MP (axiomIConj _ _ _) hφ) hψ
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.EConj₁
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
⊢ (Γ ⊢ φ₁ ∧' φ₂) → (Γ ⊢ φ₁)
Tactic:
intro h
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₁ ∧' φ₂
⊢ Γ ⊢ φ₁
Theorem: PropositionalLogic.HilbertSystem.HPM.EConj₁
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₁ ∧' φ₂
⊢ Γ ⊢ φ₁
Tactic:
exact MP (axiomEConj₁ _ _ _) h
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.EConj₂
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
⊢ (Γ ⊢ φ₁ ∧' φ₂) → (Γ ⊢ φ₂)
Tactic:
intro h
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₁ ∧' φ₂
⊢ Γ ⊢ φ₂
Theorem: PropositionalLogic.HilbertSystem.HPM.EConj₂
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
Γ : Finset L
φ₁ φ₂ : L
h : Γ ⊢ φ₁ ∧' φ₂
⊢ Γ ⊢ φ₂
Tactic:
exact MP (axiomEConj₂ _ _ _) h
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.lnc
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
⊢ ∅ ⊢ ¬'(φ ∧' ¬'φ)
Tactic:
simp [deduction]
Proof state after:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ : L
⊢ {φ ∧' (φ →' ⊥')} ⊢ ⊥'