Hilbert

Difficulty: optional — 4 definitions, 0 abbreviations, 12 lemmas, 1 theorems, 0 examples.

definition lemma theorem

legend

A Hilbert-style proof system for classical propositional logic: a fixed set of axiom schemas, closed under modus ponens. Since negation is a primitive connective here rather than one derived from implication and falsehood, the axioms governing it (reductio and double-negation elimination, both cases of Propositional.Formula.Provable below) are specific to this system.

On top of the raw axioms, a small toolkit of derived rules: that every formula implies itself, that every formula is either true or its negation is (excluded middle, derived rather than assumed), and that a case split on a formula’s truth value is enough to settle a shared conclusion.

NotePropositional.Formula.Provable

Provability in the Hilbert system: a formula is provable exactly when it has a derivation from the axioms below via modus ponens.

Propositional.Formula.Provable {α : Type} : Propositional.Formula α → Prop

Show details

| Propositional.Formula.Provable.mp : ∀ {α : Type} {φ ψ : Propositional.Formula α}, (φ.imp ψ).Provable → φ.Provable → ψ.Provable
| Propositional.Formula.Provable.k : ∀ {α : Type} {φ ψ : Propositional.Formula α}, (φ.imp (ψ.imp φ)).Provable
| Propositional.Formula.Provable.s : ∀ {α : Type} {φ ψ χ : Propositional.Formula α},
  ((φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ))).Provable
| Propositional.Formula.Provable.andElim1 : ∀ {α : Type} {φ ψ : Propositional.Formula α}, ((φ.and ψ).imp φ).Provable
| Propositional.Formula.Provable.andElim2 : ∀ {α : Type} {φ ψ : Propositional.Formula α}, ((φ.and ψ).imp ψ).Provable
| Propositional.Formula.Provable.andIntro : ∀ {α : Type} {φ ψ : Propositional.Formula α}, (φ.imp (ψ.imp (φ.and ψ))).Provable
| Propositional.Formula.Provable.orIntro1 : ∀ {α : Type} {φ ψ : Propositional.Formula α}, (φ.imp (φ.or ψ)).Provable
| Propositional.Formula.Provable.orIntro2 : ∀ {α : Type} {φ ψ : Propositional.Formula α}, (ψ.imp (φ.or ψ)).Provable
| Propositional.Formula.Provable.orElim : ∀ {α : Type} {φ ψ χ : Propositional.Formula α},
  ((φ.imp χ).imp ((ψ.imp χ).imp ((φ.or ψ).imp χ))).Provable
| Propositional.Formula.Provable.negIntro : ∀ {α : Type} {φ ψ : Propositional.Formula α}, ((φ.imp ψ).imp ((φ.imp ψ.neg).imp φ.neg)).Provable
| Propositional.Formula.Provable.dne : ∀ {α : Type} {φ : Propositional.Formula α}, (φ.neg.neg.imp φ).Provable

Outer dependencies: Propositional.Formula

Used by: Propositional.Formula.Derivable, Propositional.Formula.Derivable.deduction_aux, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.Derivable.weaken, Propositional.Formula.SyntacticEntails, Propositional.Formula.case_split, Propositional.Formula.completeness, Propositional.Formula.provable_contrapose, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_explosion, Propositional.Formula.provable_imp_iff_semanticDerive, Propositional.Formula.provable_imp_iff_syntacticDerive, Propositional.Formula.provable_lem, Propositional.Formula.provable_self_imp, Propositional.Formula.soundness

NotePropositional.Notation.«term⊢_»

\(\vdash \varphi\): \(\varphi\) is provable in the Hilbert system.

Propositional.Notation.«term⊢_» : ParserDescr

Show details

ParserDescr.node `Propositional.Notation.«term⊢_» 1024
  (ParserDescr.binary `andthen (ParserDescr.symbol "⊢ ") (ParserDescr.cat `term 0))

Complexity: 45 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.Name.mkStr3, Lean.ParserDescr, Nat

Used by: (none)

NotePropositional.Notation.«term⊨_»

\(\vDash \varphi\): \(\varphi\) is a tautology.

Propositional.Notation.«term⊨_» : ParserDescr

Show details

ParserDescr.node `Propositional.Notation.«term⊨_» 1024
  (ParserDescr.binary `andthen (ParserDescr.symbol "⊨ ") (ParserDescr.cat `term 0))

Complexity: 45 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.Name.mkStr3, Lean.ParserDescr, Nat

Used by: (none)

TipPropositional.Formula.soundness

Soundness. Every provable formula is a tautology.

Propositional.Formula.soundness {α : Type} {φ : Propositional.Formula α} (h : φ.Provable) :
  φ.Tautology

Show details

fun {α} {φ} h =>
  Propositional.Formula.Provable.rec
    (fun {φ ψ} a a_1 ihpq ihp v =>
      have hpq := ihpq v;
      have hp := ihp v;
      Eq.mp
        (congrFun'
          (congrArg Eq
            (Eq.trans
              (congrFun' (congrArg or (Eq.trans (congrArg not hp) Bool.not_true))
                (Propositional.Formula.val v ψ))
              (Bool.false_or (Propositional.Formula.val v ψ))))
          true)
        hpq)
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ ψ χ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ) (Propositional.Formula.val v χ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ ψ χ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ) (Propositional.Formula.val v χ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ)
          (Propositional.Formula.val v ψ)))
    (fun {φ} v => id (of_decide_eq_true (id (Eq.refl true)) (Propositional.Formula.val v φ))) h

Complexity: 3741 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable, Propositional.Formula.Tautology

Proof dependencies: Propositional.Formula.val, Propositional.Valuation

Lean core dependencies: Bool, Bool.and, Bool.false_or, Bool.not, Bool.not_true, Bool.or, Decidable.decide, Eq, Eq.mp, Eq.trans, congrArg, congrFun', id, of_decide_eq_true

Used by: Propositional.Formula.provable_imp_iff_semanticDerive

NotePropositional.Formula.Derivable

Provability of \(\varphi\) from a list of hypotheses: each step either invokes an unconditional axiom, assumes something already in the list, or combines two earlier steps by modus ponens.

Propositional.Formula.Derivable {α : Type} (Γ : List (Propositional.Formula α)) :
  Propositional.Formula α → Prop

Show details

| Propositional.Formula.Derivable.assumption : ∀ {α : Type} {Γ : List (Propositional.Formula α)} {φ : Propositional.Formula α},
  φ ∈ Γ → Propositional.Formula.Derivable Γ φ
| Propositional.Formula.Derivable.ax : ∀ {α : Type} {Γ : List (Propositional.Formula α)} {φ : Propositional.Formula α},
  φ.Provable → Propositional.Formula.Derivable Γ φ
| Propositional.Formula.Derivable.mp : ∀ {α : Type} {Γ : List (Propositional.Formula α)} {φ ψ : Propositional.Formula α},
  Propositional.Formula.Derivable Γ (φ.imp ψ) →
    Propositional.Formula.Derivable Γ φ → Propositional.Formula.Derivable Γ ψ

Outer dependencies: Propositional.Formula

Inner dependencies: Propositional.Formula.Provable

Lean core dependencies: List

Used by: Propositional.Formula.Derivable.case_split, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.deduction_aux, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.Derivable.weaken, Propositional.Formula.completeness, Propositional.Formula.eliminate, Propositional.Formula.kalmar, Propositional.Formula.provable_contrapose, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_explosion, Propositional.Formula.provable_lem

TipPropositional.Formula.provable_self_imp

Every formula implies itself — the classic combinator identity \(SKK = I\), specialised to implication.

Propositional.Formula.provable_self_imp {α : Type} (φ : Propositional.Formula α) :
  (φ.imp φ).Provable

Show details

fun {α} φ =>
  Propositional.Formula.Provable.mp
    (Propositional.Formula.Provable.mp Propositional.Formula.Provable.s
      Propositional.Formula.Provable.k)
    Propositional.Formula.Provable.k

Complexity: 119 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Used by: Propositional.Formula.Derivable.deduction_aux, Propositional.Formula.SyntacticEntails.refl, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_lem

TipPropositional.Formula.Derivable.deduction_aux

Auxiliary form of the Deduction Theorem below, with the extended context named as a plain equality hypothesis rather than a literal cons pattern — this is what lets induction on the derivation go through cleanly.

Propositional.Formula.Derivable.deduction_aux {α : Type} {φ ψ : Propositional.Formula α}
  {Δ : List (Propositional.Formula α)} (h : Propositional.Formula.Derivable Δ ψ)
  (Γ : List (Propositional.Formula α)) : Δ = φ :: Γ → Propositional.Formula.Derivable Γ (φ.imp ψ)

Show details

fun {α} {φ ψ} {Δ} h =>
  Propositional.Formula.Derivable.rec (motive := fun {ψ} h =>
    ∀ (Γ : List (Propositional.Formula α)),
      Δ = φ :: Γ → Propositional.Formula.Derivable Γ (φ.imp ψ))
    (fun {χ} hmem Γ hΔ =>
      Eq.ndrec (motive := fun {Δ} => χ ∈ Δ → Propositional.Formula.Derivable Γ (φ.imp χ))
        (fun hmem =>
          Or.casesOn (List.mem_cons.mp hmem)
            (fun h =>
              Eq.ndrec (motive := fun {φ} =>
                χ ∈ φ :: Γ → Propositional.Formula.Derivable Γ (φ.imp χ))
                (fun hmem =>
                  Propositional.Formula.Derivable.ax (Propositional.Formula.provable_self_imp χ))
                h hmem)
            fun hmem =>
            Propositional.Formula.Derivable.mp
              (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k)
              (Propositional.Formula.Derivable.assumption hmem))
        (Eq.symm hΔ) hmem)
    (fun {χ} hχ Γ a =>
      Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k)
        (Propositional.Formula.Derivable.ax hχ))
    (fun {χ₁ χ₂} a a_1 ih1 ih2 Γ hΔ =>
      Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.mp
          (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.s) (ih1 Γ hΔ))
        (ih2 Γ hΔ))
    h

Complexity: 973 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Derivable

Proof dependencies: Propositional.Formula.Provable, Propositional.Formula.provable_self_imp

Lean core dependencies: Eq, Eq.symm, List, List.mem_cons, Or

Used by: Propositional.Formula.Derivable.deduction

TipPropositional.Formula.Derivable.deduction

The Deduction Theorem. If \(\psi\) is derivable from some hypotheses together with \(\varphi\), then \(\varphi \to \psi\) is derivable from those hypotheses alone. This is what turns “assume \(\varphi\), derive \(\psi\)” reasoning into an ordinary axiom-and-modus-ponens proof, and is the standard reason Hilbert systems are usable at all.

Propositional.Formula.Derivable.deduction {α : Type} {Γ : List (Propositional.Formula α)}
  {φ ψ : Propositional.Formula α} (h : Propositional.Formula.Derivable (φ :: Γ) ψ) :
  Propositional.Formula.Derivable Γ (φ.imp ψ)

Show details

fun {α} {Γ} {φ ψ} h => Propositional.Formula.Derivable.deduction_aux h Γ rfl

Complexity: 71 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Derivable

Proof dependencies: Propositional.Formula.Derivable.deduction_aux

Lean core dependencies: List, rfl

Used by: Propositional.Formula.SyntacticEntails.trans, Propositional.Formula.eliminate, Propositional.Formula.kalmar, Propositional.Formula.provable_contrapose, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_explosion, Propositional.Formula.provable_lem

TipPropositional.Formula.Derivable.provable_of_nil

A derivation from no hypotheses at all is just a proof.

Propositional.Formula.Derivable.provable_of_nil {α : Type} {ψ : Propositional.Formula α}
  (h : Propositional.Formula.Derivable [] ψ) : ψ.Provable

Show details

fun {α} {ψ} h =>
  Propositional.Formula.Derivable.rec (fun {φ} hmem => absurd hmem List.not_mem_nil)
    (fun {φ} hψ => hψ) (fun {φ ψ} a a_1 ih1 ih2 => Propositional.Formula.Provable.mp ih1 ih2) h

Complexity: 207 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Derivable, Propositional.Formula.Provable

Lean core dependencies: List, List.not_mem_nil, absurd

Used by: Propositional.Formula.SyntacticEntails.trans, Propositional.Formula.case_split, Propositional.Formula.completeness, Propositional.Formula.provable_contrapose, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_explosion, Propositional.Formula.provable_lem

TipPropositional.Formula.provable_lem

Excluded middle, derived (not assumed) from the raw axioms via the deduction theorem and double-negation elimination.

Propositional.Formula.provable_lem {α : Type} (φ : Propositional.Formula α) : (φ.or φ.neg).Provable

Show details

fun {α} φ =>
  have step1 := Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orIntro1;
  have step2 :=
    Propositional.Formula.Derivable.deduction
      (Propositional.Formula.Derivable.assumption
        (of_eq_true
          (Eq.trans List.mem_cons._simp_1
            (Eq.trans
              (congrArg (Or ((φ.or φ.neg).neg = φ))
                (Eq.trans List.mem_cons._simp_1
                  (Eq.trans
                    (congr (congrArg Or (eq_self (φ.or φ.neg).neg)) List.not_mem_nil._simp_1)
                    (or_false True))))
              (or_true ((φ.or φ.neg).neg = φ))))));
  have step3 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.negIntro) step1)
      step2;
  have step4 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orIntro2) step3;
  have hNXX :=
    Propositional.Formula.Derivable.provable_of_nil
      (Propositional.Formula.Derivable.deduction step4);
  have hNXNX := Propositional.Formula.provable_self_imp (φ.or φ.neg).neg;
  have hNNX :=
    Propositional.Formula.Provable.mp
      (Propositional.Formula.Provable.mp Propositional.Formula.Provable.negIntro hNXX) hNXNX;
  Propositional.Formula.Provable.mp Propositional.Formula.Provable.dne hNNX

Complexity: 2168 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Proof dependencies: Propositional.Formula.Derivable, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.provable_self_imp

Lean core dependencies: Eq, Eq.trans, False, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false, or_true

Used by: Propositional.Formula.Derivable.case_split

TipPropositional.Formula.Derivable.case_split

A case split, relative to a shared list of hypotheses: if a conclusion follows from some formula and also follows from its negation, then it holds outright given those hypotheses.

Propositional.Formula.Derivable.case_split {α : Type} {Γ : List (Propositional.Formula α)}
  {p X : Propositional.Formula α} (hA : Propositional.Formula.Derivable Γ (p.imp X))
  (hB : Propositional.Formula.Derivable Γ (p.neg.imp X)) : Propositional.Formula.Derivable Γ X

Show details

fun {α} {Γ} {p X} hA hB =>
  Propositional.Formula.Derivable.mp
    (Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orElim) hA)
      hB)
    (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_lem p))

Complexity: 245 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Derivable

Proof dependencies: Propositional.Formula.provable_lem

Lean core dependencies: List

Used by: Propositional.Formula.case_split, Propositional.Formula.eliminate

ImportantPropositional.Formula.case_split

The same case split with no hypotheses at all: the Γ = ∅ specialisation of Propositional.Formula.Derivable.case_split.

Propositional.Formula.case_split {α : Type} {p X : Propositional.Formula α}
  (hA : (p.imp X).Provable) (hB : (p.neg.imp X).Provable) : X.Provable

Show details

fun {α} {p X} hA hB =>
  Propositional.Formula.Derivable.provable_of_nil
    (Propositional.Formula.Derivable.case_split (Propositional.Formula.Derivable.ax hA)
      (Propositional.Formula.Derivable.ax hB))

Complexity: 101 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Proof dependencies: Propositional.Formula.Derivable.case_split, Propositional.Formula.Derivable.provable_of_nil

Used by: (none)

TipPropositional.Formula.Derivable.weaken

Adding more hypotheses never breaks a derivation.

Propositional.Formula.Derivable.weaken {α : Type} {Γ Γ' : List (Propositional.Formula α)}
  (hsub : Γ ⊆ Γ') {φ : Propositional.Formula α} (h : Propositional.Formula.Derivable Γ φ) :
  Propositional.Formula.Derivable Γ' φ

Show details

fun {α} {Γ Γ'} hsub {φ} h =>
  Propositional.Formula.Derivable.rec
    (fun {φ} hmem => Propositional.Formula.Derivable.assumption (hsub hmem))
    (fun {φ} hφ => Propositional.Formula.Derivable.ax hφ)
    (fun {φ ψ} a a_1 ih1 ih2 => Propositional.Formula.Derivable.mp ih1 ih2) h

Complexity: 199 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Derivable

Proof dependencies: Propositional.Formula.Provable

Lean core dependencies: List

Used by: Propositional.Formula.kalmar

TipPropositional.Formula.provable_dni

Double-negation introduction: the converse of the double-negation-elimination case of Propositional.Formula.Provable, derived rather than assumed.

Propositional.Formula.provable_dni {α : Type} (φ : Propositional.Formula α) :
  (φ.imp φ.neg.neg).Provable

Show details

fun {α} φ =>
  have h1 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k)
      (Propositional.Formula.Derivable.assumption
        (of_eq_true
          (Eq.trans List.mem_cons._simp_1
            (Eq.trans (congr (congrArg Or (eq_self φ)) List.not_mem_nil._simp_1)
              (or_false True)))));
  have h2 := Propositional.Formula.Derivable.ax (Propositional.Formula.provable_self_imp φ.neg);
  have h3 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.negIntro) h1)
      h2;
  Propositional.Formula.Derivable.provable_of_nil (Propositional.Formula.Derivable.deduction h3)

Complexity: 738 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Proof dependencies: Propositional.Formula.Derivable, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.provable_self_imp

Lean core dependencies: Eq, Eq.trans, False, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false

Used by: Propositional.Formula.kalmar

TipPropositional.Formula.provable_explosion

Explosion: from a formula and its negation, anything follows.

Propositional.Formula.provable_explosion {α : Type} (φ X : Propositional.Formula α) :
  (φ.imp (φ.neg.imp X)).Provable

Show details

fun {α} φ X =>
  have hφ :=
    Propositional.Formula.Derivable.assumption
      (of_eq_true
        (Eq.trans List.mem_cons._simp_1
          (Eq.trans
            (congrArg (Or (φ = φ.neg))
              (Eq.trans List.mem_cons._simp_1
                (Eq.trans (congr (congrArg Or (eq_self φ)) List.not_mem_nil._simp_1)
                  (or_false True))))
            (or_true (φ = φ.neg)))));
  have hnφ :=
    Propositional.Formula.Derivable.assumption
      (of_eq_true
        (Eq.trans List.mem_cons._simp_1
          (Eq.trans
            (congr (congrArg Or (eq_self φ.neg))
              (Eq.trans List.mem_cons._simp_1
                (Eq.trans (congrArg (Or (φ.neg = φ)) List.not_mem_nil._simp_1)
                  (or_false (φ.neg = φ)))))
            (true_or (φ.neg = φ)))));
  have h1 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k) hφ;
  have h2 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k) hnφ;
  have h3 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.negIntro) h1)
      h2;
  have h4 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.dne) h3;
  have h5 := Propositional.Formula.Derivable.deduction h4;
  Propositional.Formula.Derivable.provable_of_nil (Propositional.Formula.Derivable.deduction h5)

Complexity: 2220 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Proof dependencies: Propositional.Formula.Derivable, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.provable_of_nil

Lean core dependencies: Eq, Eq.trans, False, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false, or_true, true_or

Used by: Propositional.Formula.kalmar, Propositional.Formula.provable_deMorgan_or

TipPropositional.Formula.provable_contrapose

Contraposition: if one formula proves another, the second’s negation proves the first’s.

Propositional.Formula.provable_contrapose {α : Type} {p q : Propositional.Formula α}
  (h : (p.imp q).Provable) : (q.neg.imp p.neg).Provable

Show details

fun {α} {p q} h =>
  have h1 := Propositional.Formula.Derivable.ax h;
  have h2 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k)
      (Propositional.Formula.Derivable.assumption
        (of_eq_true
          (Eq.trans List.mem_cons._simp_1
            (Eq.trans (congr (congrArg Or (eq_self q.neg)) List.not_mem_nil._simp_1)
              (or_false True)))));
  have h3 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.negIntro) h1)
      h2;
  Propositional.Formula.Derivable.provable_of_nil (Propositional.Formula.Derivable.deduction h3)

Complexity: 818 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Proof dependencies: Propositional.Formula.Derivable, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.provable_of_nil

Lean core dependencies: Eq, Eq.trans, False, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false

Used by: Propositional.Formula.kalmar

TipPropositional.Formula.provable_deMorgan_or

De Morgan, the direction needed below: if two formulas are both false, so is their disjunction.

Propositional.Formula.provable_deMorgan_or {α : Type} (φ ψ : Propositional.Formula α) :
  (φ.neg.imp (ψ.neg.imp (φ.or ψ).neg)).Provable

Show details

fun {α} φ ψ =>
  have h1 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax
          (Propositional.Formula.provable_explosion φ (φ.or ψ).neg))
        (Propositional.Formula.Derivable.assumption
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans
                (congr (congrArg Or (eq_self φ))
                  (Eq.trans List.mem_cons._simp_1
                    (congrArg (Or (φ = ψ.neg))
                      (Eq.trans List.mem_cons._simp_1
                        (Eq.trans (congrArg (Or (φ = φ.neg)) List.not_mem_nil._simp_1)
                          (or_false (φ = φ.neg)))))))
                (true_or (φ = ψ.neg ∨ φ = φ.neg)))))))
      (Propositional.Formula.Derivable.assumption
        (of_eq_true
          (Eq.trans List.mem_cons._simp_1
            (Eq.trans
              (congrArg (Or (φ.neg = φ))
                (Eq.trans List.mem_cons._simp_1
                  (Eq.trans
                    (congr (congrArg Or (Propositional.Formula.neg.injEq φ ψ))
                      (Eq.trans List.mem_cons._simp_1
                        (Eq.trans (congr (congrArg Or (eq_self φ.neg)) List.not_mem_nil._simp_1)
                          (or_false True))))
                    (or_true (φ = ψ)))))
              (or_true (φ.neg = φ))))));
  have h1d := Propositional.Formula.Derivable.deduction h1;
  have h2 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax
          (Propositional.Formula.provable_explosion ψ (φ.or ψ).neg))
        (Propositional.Formula.Derivable.assumption
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans
                (congr (congrArg Or (eq_self ψ))
                  (Eq.trans List.mem_cons._simp_1
                    (congrArg (Or (ψ = ψ.neg))
                      (Eq.trans List.mem_cons._simp_1
                        (Eq.trans (congrArg (Or (ψ = φ.neg)) List.not_mem_nil._simp_1)
                          (or_false (ψ = φ.neg)))))))
                (true_or (ψ = ψ.neg ∨ ψ = φ.neg)))))))
      (Propositional.Formula.Derivable.assumption
        (of_eq_true
          (Eq.trans List.mem_cons._simp_1
            (Eq.trans
              (congrArg (Or (ψ.neg = ψ))
                (Eq.trans List.mem_cons._simp_1
                  (Eq.trans
                    (congr (congrArg Or (eq_self ψ.neg))
                      (Eq.trans List.mem_cons._simp_1
                        (Eq.trans
                          (congr (congrArg Or (Propositional.Formula.neg.injEq ψ φ))
                            List.not_mem_nil._simp_1)
                          (or_false (ψ = φ)))))
                    (true_or (ψ = φ)))))
              (or_true (ψ.neg = ψ))))));
  have h2d := Propositional.Formula.Derivable.deduction h2;
  have h3 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orElim) h1d)
      h2d;
  have h4 :=
    Propositional.Formula.Derivable.mp
      (Propositional.Formula.Derivable.mp
        (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.negIntro)
        (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_self_imp (φ.or ψ))))
      h3;
  Propositional.Formula.Derivable.provable_of_nil
    (Propositional.Formula.Derivable.deduction (Propositional.Formula.Derivable.deduction h4))

Complexity: 6085 (size of the value term)

Dependencies: Propositional.Formula, Propositional.Formula.Provable

Proof dependencies: Propositional.Formula.Derivable, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.provable_explosion, Propositional.Formula.provable_self_imp

Lean core dependencies: Eq, Eq.trans, False, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false, or_true, true_or

Used by: Propositional.Formula.kalmar

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency

legend