Hilbert

Difficulty: optional — 6 definitions, 0 abbreviations, 14 lemmas, 17 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, relative to a list of hypotheses. 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 PropositionalLogic.Formula.Derivable below) are specific to this system.

Provability outright (PropositionalLogic.Formula.Provable) is the special case of derivability with no hypotheses at all: it is not a second, separate notion, just PropositionalLogic.Formula.Derivable with an empty list.

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.

NoteLogic.PropositionalLogic.Formula.Derivable

Derivability 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. Every axiom is available regardless of which hypotheses are around, since an axiom needs none of its own.

inductive Logic.PropositionalLogic.Formula.Derivable {α : Type}
  (Γ : List (Logic.PropositionalLogic.Formula α)) : Logic.PropositionalLogic.Formula α → Prop

• assumption : ∀ {φ : Logic.PropositionalLogic.Formula α}, φ ∈ Γ → Logic.PropositionalLogic.Formula.Derivable Γ φ

• Modus ponens: the only inference rule.

  mp : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp ψ) →
    Logic.PropositionalLogic.Formula.Derivable Γ φ → Logic.PropositionalLogic.Formula.Derivable Γ ψ

• k : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp (ψ.imp φ))

• s : ∀ {φ ψ χ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ ((φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ)))

• andElim1 : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ ((φ.and ψ).imp φ)

• andElim2 : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ ((φ.and ψ).imp ψ)

• andIntro : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp (ψ.imp (φ.and ψ)))

• orIntro1 : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp (φ.or ψ))

• orIntro2 : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ (ψ.imp (φ.or ψ))

• orElim : ∀ {φ ψ χ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ ((φ.imp χ).imp ((ψ.imp χ).imp ((φ.or ψ).imp χ)))

• Reductio: from \(\varphi \to \psi\) and \(\varphi \to \lnot\psi\), conclude \(\lnot\varphi\).

  negIntro : ∀ {φ ψ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ ((φ.imp ψ).imp ((φ.imp ψ.neg).imp φ.neg))

• Double-negation elimination: what makes this system classical rather than intuitionistic.

  dne : ∀ {φ : Logic.PropositionalLogic.Formula α},
  Logic.PropositionalLogic.Formula.Derivable Γ (φ.neg.neg.imp φ)

Show details

Outer dependencies: Logic.PropositionalLogic.Formula

Lean core dependencies: List

Used by: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.case_split, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Derivable.toProofSystem, Logic.PropositionalLogic.Formula.Derivable.weaken, Logic.PropositionalLogic.Formula.Provable, Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.lift_provable, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem, Logic.PropositionalLogic.Formula.soundness

NoteLogic.PropositionalLogic.Formula.Provable

Provability in the Hilbert system: a formula is provable exactly when it is derivable from no hypotheses at all.

def Logic.PropositionalLogic.Formula.Provable {α : Type} (φ : Logic.PropositionalLogic.Formula α) : Prop

Show details

| φ.Provable = Logic.PropositionalLogic.Formula.Derivable [] φ

Complexity: 17 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula

Inner dependencies: Logic.PropositionalLogic.Formula.Derivable

Used by: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.andElim1, Logic.PropositionalLogic.Formula.Provable.andElim2, Logic.PropositionalLogic.Formula.Provable.andIntro, Logic.PropositionalLogic.Formula.Provable.dne, Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.mp, Logic.PropositionalLogic.Formula.Provable.negIntro, Logic.PropositionalLogic.Formula.Provable.orElim, Logic.PropositionalLogic.Formula.Provable.orIntro1, Logic.PropositionalLogic.Formula.Provable.orIntro2, Logic.PropositionalLogic.Formula.Provable.s, Logic.PropositionalLogic.Formula.SyntacticEntails, Logic.PropositionalLogic.Formula.case_split, Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic, Logic.PropositionalLogic.Formula.lift_provable, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem, Logic.PropositionalLogic.Formula.provable_self_imp, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.Formula.soundness, Logic.PropositionalLogic.Formula.syntactic_iff_provable

NoteLogic.PropositionalLogic.Notation.«term⊢_»

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

def Logic.PropositionalLogic.Notation.«term⊢_» : ParserDescr

Show details

| Logic.PropositionalLogic.Notation.«term⊢_» =
  ParserDescr.node `Logic.PropositionalLogic.Notation.«term⊢_» 1024
    (ParserDescr.binary `andthen (ParserDescr.symbol "⊢ ") (ParserDescr.cat `term 0))

Complexity: 47 (size of the value term)

Outer dependencies: (none)

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

Used by: (none)

NoteLogic.PropositionalLogic.Notation.«term⊨_»

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

def Logic.PropositionalLogic.Notation.«term⊨_» : ParserDescr

Show details

| Logic.PropositionalLogic.Notation.«term⊨_» =
  ParserDescr.node `Logic.PropositionalLogic.Notation.«term⊨_» 1024
    (ParserDescr.binary `andthen (ParserDescr.symbol "⊨ ") (ParserDescr.cat `term 0))

Complexity: 47 (size of the value term)

Outer dependencies: (none)

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

Used by: (none)

TipLogic.PropositionalLogic.Formula.soundness

Soundness. Every provable formula is a tautology.

theorem Logic.PropositionalLogic.Formula.soundness {α : Type} {φ : Logic.PropositionalLogic.Formula α}
  (h : φ.Provable) : φ.Tautology

Show details

fun {α} {φ} h =>
  Logic.PropositionalLogic.Formula.Derivable.rec (fun {φ} hmem => absurd hmem List.not_mem_nil)
    (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))
                (Logic.PropositionalLogic.Formula.val v ψ))
              (Bool.false_or (Logic.PropositionalLogic.Formula.val v ψ))))
          true)
        hpq)
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ ψ χ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ) (Logic.PropositionalLogic.Formula.val v χ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ ψ χ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ) (Logic.PropositionalLogic.Formula.val v χ)))
    (fun {φ ψ} v =>
      id
        (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)
          (Logic.PropositionalLogic.Formula.val v ψ)))
    (fun {φ} v =>
      id (of_decide_eq_true (id (Eq.refl true)) (Logic.PropositionalLogic.Formula.val v φ)))
    h

Complexity: 3833 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable, Logic.PropositionalLogic.Formula.Tautology

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

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

Used by: Logic.PropositionalLogic.Formula.semantic_iff_provable

TipLogic.PropositionalLogic.Formula.Derivable.weaken

Adding more hypotheses never breaks a derivation. Every axiom case is immediate, since an axiom needs no hypotheses to begin with.

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

Show details

fun {α} {Γ Γ'} hsub {φ} h =>
  Logic.PropositionalLogic.Formula.Derivable.rec
    (fun {φ} hmem => Logic.PropositionalLogic.Formula.Derivable.assumption (hsub hmem))
    (fun {φ ψ} a a_1 ih1 ih2 => Logic.PropositionalLogic.Formula.Derivable.mp ih1 ih2)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.k)
    (fun {φ ψ χ} => Logic.PropositionalLogic.Formula.Derivable.s)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.andElim1)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.andElim2)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.andIntro)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.orIntro1)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.orIntro2)
    (fun {φ ψ χ} => Logic.PropositionalLogic.Formula.Derivable.orElim)
    (fun {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.negIntro)
    (fun {φ} => Logic.PropositionalLogic.Formula.Derivable.dne) h

Complexity: 365 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable

Lean core dependencies: List

Used by: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.kalmar

TipLogic.PropositionalLogic.Formula.Derivable.ax

A proof outright weakens to a derivation from any hypotheses at all: an axiom, or a proof built from them, needs none of its own.

theorem Logic.PropositionalLogic.Formula.Derivable.ax {α : Type}
  {Γ : List (Logic.PropositionalLogic.Formula α)} {φ : Logic.PropositionalLogic.Formula α}
  (h : φ.Provable) : Logic.PropositionalLogic.Formula.Derivable Γ φ

Show details

fun {α} {Γ} {φ} h => Logic.PropositionalLogic.Formula.Derivable.weaken (List.nil_subset Γ) h

Complexity: 41 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.weaken

Lean core dependencies: List, List.nil_subset

Used by: Logic.PropositionalLogic.Formula.Derivable.case_split, Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.SyntacticEntails.trans, Logic.PropositionalLogic.Formula.case_split, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.lift_provable, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem

ImportantLogic.PropositionalLogic.Formula.Provable.mp

Modus ponens for outright provability, the \(\Gamma = \emptyset\) case of derivability’s own modus ponens rule.

theorem Logic.PropositionalLogic.Formula.Provable.mp {α : Type} {φ ψ : Logic.PropositionalLogic.Formula α}
  (h1 : (φ.imp ψ).Provable) (h2 : φ.Provable) : ψ.Provable

Show details

fun {α} {φ ψ} h1 h2 => Logic.PropositionalLogic.Formula.Derivable.mp h1 h2

Complexity: 45 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.provable_lem, Logic.PropositionalLogic.Formula.provable_self_imp

ImportantLogic.PropositionalLogic.Formula.Provable.k

theorem Logic.PropositionalLogic.Formula.Provable.k {α : Type} {φ ψ : Logic.PropositionalLogic.Formula α} :
  (φ.imp (ψ.imp φ)).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.k

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.lift_provable, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_self_imp

ImportantLogic.PropositionalLogic.Formula.Provable.s

theorem Logic.PropositionalLogic.Formula.Provable.s {α : Type}
  {φ ψ χ : Logic.PropositionalLogic.Formula α} :
  ((φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ))).Provable

Show details

fun {α} {φ ψ χ} => Logic.PropositionalLogic.Formula.Derivable.s

Complexity: 29 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.provable_self_imp

ImportantLogic.PropositionalLogic.Formula.Provable.andElim1

theorem Logic.PropositionalLogic.Formula.Provable.andElim1 {α : Type}
  {φ ψ : Logic.PropositionalLogic.Formula α} : ((φ.and ψ).imp φ).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.andElim1

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.and_entails_left_syntactic, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.kalmar

ImportantLogic.PropositionalLogic.Formula.Provable.andElim2

theorem Logic.PropositionalLogic.Formula.Provable.andElim2 {α : Type}
  {φ ψ : Logic.PropositionalLogic.Formula α} : ((φ.and ψ).imp ψ).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.andElim2

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.and_entails_right_syntactic, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.kalmar

ImportantLogic.PropositionalLogic.Formula.Provable.andIntro

theorem Logic.PropositionalLogic.Formula.Provable.andIntro {α : Type}
  {φ ψ : Logic.PropositionalLogic.Formula α} : (φ.imp (ψ.imp (φ.and ψ))).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.andIntro

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.kalmar

ImportantLogic.PropositionalLogic.Formula.Provable.orIntro1

theorem Logic.PropositionalLogic.Formula.Provable.orIntro1 {α : Type}
  {φ ψ : Logic.PropositionalLogic.Formula α} : (φ.imp (φ.or ψ)).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.orIntro1

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.or_entails_left_syntactic, Logic.PropositionalLogic.Formula.provable_lem

ImportantLogic.PropositionalLogic.Formula.Provable.orIntro2

theorem Logic.PropositionalLogic.Formula.Provable.orIntro2 {α : Type}
  {φ ψ : Logic.PropositionalLogic.Formula α} : (ψ.imp (φ.or ψ)).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.orIntro2

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.or_entails_right_syntactic, Logic.PropositionalLogic.Formula.provable_lem

ImportantLogic.PropositionalLogic.Formula.Provable.orElim

theorem Logic.PropositionalLogic.Formula.Provable.orElim {α : Type}
  {φ ψ χ : Logic.PropositionalLogic.Formula α} :
  ((φ.imp χ).imp ((ψ.imp χ).imp ((φ.or ψ).imp χ))).Provable

Show details

fun {α} {φ ψ χ} => Logic.PropositionalLogic.Formula.Derivable.orElim

Complexity: 29 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.case_split, Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.provable_deMorgan_or

ImportantLogic.PropositionalLogic.Formula.Provable.negIntro

theorem Logic.PropositionalLogic.Formula.Provable.negIntro {α : Type}
  {φ ψ : Logic.PropositionalLogic.Formula α} : ((φ.imp ψ).imp ((φ.imp ψ.neg).imp φ.neg)).Provable

Show details

fun {α} {φ ψ} => Logic.PropositionalLogic.Formula.Derivable.negIntro

Complexity: 23 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem

ImportantLogic.PropositionalLogic.Formula.Provable.dne

theorem Logic.PropositionalLogic.Formula.Provable.dne {α : Type} {φ : Logic.PropositionalLogic.Formula α} :
  (φ.neg.neg.imp φ).Provable

Show details

fun {α} {φ} => Logic.PropositionalLogic.Formula.Derivable.dne

Complexity: 17 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem

TipLogic.PropositionalLogic.Formula.provable_self_imp

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

theorem Logic.PropositionalLogic.Formula.provable_self_imp {α : Type}
  (φ : Logic.PropositionalLogic.Formula α) : (φ.imp φ).Provable

Show details

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

Complexity: 119 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.mp, Logic.PropositionalLogic.Formula.Provable.s

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

TipLogic.PropositionalLogic.Formula.lift_provable

Lifting an axiom (or anything already provable outright) past an extra premise \(\varphi\): the \(K\) axiom turns \(\chi\) into \(\varphi \to \chi\), regardless of what hypotheses are around. Used once per axiom case in PropositionalLogic.Formula.Derivable.deduction_aux below, since every axiom case there has exactly this shape.

theorem Logic.PropositionalLogic.Formula.lift_provable✝ {α : Type} (φ : Logic.PropositionalLogic.Formula α)
  {χ : Logic.PropositionalLogic.Formula α} (hχ : χ.Provable)
  (Γ : List (Logic.PropositionalLogic.Formula α)) :
  Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp χ)

Show details

fun {α} φ {χ} hχ Γ =>
  Logic.PropositionalLogic.Formula.Derivable.mp
    (Logic.PropositionalLogic.Formula.Derivable.ax Logic.PropositionalLogic.Formula.Provable.k)
    (Logic.PropositionalLogic.Formula.Derivable.ax hχ)

Complexity: 75 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Provable.k

Lean core dependencies: List

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction_aux

TipLogic.PropositionalLogic.Formula.Derivable.deduction_aux

Auxiliary form of the Derivation 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.

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

Show details

fun {α} {φ ψ} {Δ} h =>
  Logic.PropositionalLogic.Formula.Derivable.rec (motive := fun {ψ} h =>
    ∀ (Γ : List (Logic.PropositionalLogic.Formula α)),
      Δ = φ :: Γ → Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp ψ))
    (fun {χ} hmem Γ hΔ =>
      Eq.ndrec (motive := fun {Δ} => χ ∈ Δ → Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp χ))
        (fun hmem =>
          Or.casesOn (List.mem_cons.mp hmem)
            (fun h =>
              Eq.ndrec (motive := fun {φ} =>
                χ ∈ φ :: Γ → Logic.PropositionalLogic.Formula.Derivable Γ (φ.imp χ))
                (fun hmem =>
                  Logic.PropositionalLogic.Formula.Derivable.ax
                    (Logic.PropositionalLogic.Formula.provable_self_imp χ))
                h hmem)
            fun hmem =>
            Logic.PropositionalLogic.Formula.Derivable.mp
              (Logic.PropositionalLogic.Formula.Derivable.ax
                Logic.PropositionalLogic.Formula.Provable.k)
              (Logic.PropositionalLogic.Formula.Derivable.assumption hmem))
        (Eq.symm hΔ) hmem)
    (fun {χ₁ χ₂} a a_1 ih1 ih2 Γ hΔ =>
      Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.mp
          (Logic.PropositionalLogic.Formula.Derivable.ax
            Logic.PropositionalLogic.Formula.Provable.s)
          (ih1 Γ hΔ))
        (ih2 Γ hΔ))
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ Logic.PropositionalLogic.Formula.Provable.k
        Γ)
    (fun {χ1 χ2 χ3} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ Logic.PropositionalLogic.Formula.Provable.s
        Γ)
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.andElim1 Γ)
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.andElim2 Γ)
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.andIntro Γ)
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.orIntro1 Γ)
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.orIntro2 Γ)
    (fun {χ1 χ2 χ3} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.orElim Γ)
    (fun {χ1 χ2} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.negIntro Γ)
    (fun {χ1} Γ a =>
      Logic.PropositionalLogic.Formula.lift_provable✝ φ
        Logic.PropositionalLogic.Formula.Provable.dne Γ)
    h

Complexity: 1680 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Provable.andElim1, Logic.PropositionalLogic.Formula.Provable.andElim2, Logic.PropositionalLogic.Formula.Provable.andIntro, Logic.PropositionalLogic.Formula.Provable.dne, Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.negIntro, Logic.PropositionalLogic.Formula.Provable.orElim, Logic.PropositionalLogic.Formula.Provable.orIntro1, Logic.PropositionalLogic.Formula.Provable.orIntro2, Logic.PropositionalLogic.Formula.Provable.s, Logic.PropositionalLogic.Formula.lift_provable, Logic.PropositionalLogic.Formula.provable_self_imp

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

Used by: Logic.PropositionalLogic.Formula.Derivable.deduction

TipLogic.PropositionalLogic.Formula.Derivable.deduction

The Derivation 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.

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

Show details

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

Complexity: 71 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.deduction_aux

Lean core dependencies: List, rfl

Used by: Logic.PropositionalLogic.Formula.SyntacticEntails.trans, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem

TipLogic.PropositionalLogic.Formula.Derivable.provable_of_nil

A derivation from no hypotheses at all is just a proof — immediate, since PropositionalLogic.Formula.Provable is PropositionalLogic.Formula.Derivable with no hypotheses.

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

Show details

fun {α} {ψ} h => h

Complexity: 19 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.SyntacticEntails.trans, Logic.PropositionalLogic.Formula.case_split, Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem

TipLogic.PropositionalLogic.Formula.provable_lem

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

theorem Logic.PropositionalLogic.Formula.provable_lem {α : Type} (φ : Logic.PropositionalLogic.Formula α) :
  (φ.or φ.neg).Provable

Show details

fun {α} φ =>
  have step1 :=
    Logic.PropositionalLogic.Formula.Derivable.ax
      Logic.PropositionalLogic.Formula.Provable.orIntro1;
  have step2 :=
    Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.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 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.negIntro)
        step1)
      step2;
  have step4 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax
        Logic.PropositionalLogic.Formula.Provable.orIntro2)
      step3;
  have hNXX :=
    Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
      (Logic.PropositionalLogic.Formula.Derivable.deduction step4);
  have hNXNX := Logic.PropositionalLogic.Formula.provable_self_imp (φ.or φ.neg).neg;
  have hNNX :=
    Logic.PropositionalLogic.Formula.Provable.mp
      (Logic.PropositionalLogic.Formula.Provable.mp
        Logic.PropositionalLogic.Formula.Provable.negIntro hNXX)
      hNXNX;
  Logic.PropositionalLogic.Formula.Provable.mp Logic.PropositionalLogic.Formula.Provable.dne hNNX

Complexity: 2168 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.dne, Logic.PropositionalLogic.Formula.Provable.mp, Logic.PropositionalLogic.Formula.Provable.negIntro, Logic.PropositionalLogic.Formula.Provable.orIntro1, Logic.PropositionalLogic.Formula.Provable.orIntro2, Logic.PropositionalLogic.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: Logic.PropositionalLogic.Formula.Derivable.case_split

TipLogic.PropositionalLogic.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.

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

Show details

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

Complexity: 245 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Provable.orElim, Logic.PropositionalLogic.Formula.provable_lem

Lean core dependencies: List

Used by: Logic.PropositionalLogic.Formula.case_split, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic

ImportantLogic.PropositionalLogic.Formula.case_split

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

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

Show details

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

Complexity: 101 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.case_split, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil

Used by: (none)

TipLogic.PropositionalLogic.Formula.provable_dni

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

theorem Logic.PropositionalLogic.Formula.provable_dni {α : Type} (φ : Logic.PropositionalLogic.Formula α) :
  (φ.imp φ.neg.neg).Provable

Show details

fun {α} φ =>
  have h1 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax Logic.PropositionalLogic.Formula.Provable.k)
      (Logic.PropositionalLogic.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 :=
    Logic.PropositionalLogic.Formula.Derivable.ax
      (Logic.PropositionalLogic.Formula.provable_self_imp φ.neg);
  have h3 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.negIntro)
        h1)
      h2;
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction h3)

Complexity: 738 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.negIntro, Logic.PropositionalLogic.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: Logic.PropositionalLogic.Formula.kalmar

TipLogic.PropositionalLogic.Formula.provable_explosion

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

theorem Logic.PropositionalLogic.Formula.provable_explosion {α : Type}
  (φ X : Logic.PropositionalLogic.Formula α) : (φ.imp (φ.neg.imp X)).Provable

Show details

fun {α} φ X =>
  have hφ :=
    Logic.PropositionalLogic.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φ :=
    Logic.PropositionalLogic.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 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax Logic.PropositionalLogic.Formula.Provable.k)
      hφ;
  have h2 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax Logic.PropositionalLogic.Formula.Provable.k)
      hnφ;
  have h3 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.negIntro)
        h1)
      h2;
  have h4 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax Logic.PropositionalLogic.Formula.Provable.dne)
      h3;
  have h5 := Logic.PropositionalLogic.Formula.Derivable.deduction h4;
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction h5)

Complexity: 2220 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.dne, Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.negIntro

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: Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.provable_deMorgan_or

TipLogic.PropositionalLogic.Formula.provable_contrapose

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

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

Show details

fun {α} {p q} h =>
  have h1 := Logic.PropositionalLogic.Formula.Derivable.ax h;
  have h2 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax Logic.PropositionalLogic.Formula.Provable.k)
      (Logic.PropositionalLogic.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 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.negIntro)
        h1)
      h2;
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction h3)

Complexity: 818 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.negIntro

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

Used by: Logic.PropositionalLogic.Formula.kalmar

TipLogic.PropositionalLogic.Formula.provable_deMorgan_or

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

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

Show details

fun {α} φ ψ =>
  have h1 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          (Logic.PropositionalLogic.Formula.provable_explosion φ (φ.or ψ).neg))
        (Logic.PropositionalLogic.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)))))))
      (Logic.PropositionalLogic.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 (Logic.PropositionalLogic.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 := Logic.PropositionalLogic.Formula.Derivable.deduction h1;
  have h2 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          (Logic.PropositionalLogic.Formula.provable_explosion ψ (φ.or ψ).neg))
        (Logic.PropositionalLogic.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)))))))
      (Logic.PropositionalLogic.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 (Logic.PropositionalLogic.Formula.neg.injEq ψ φ))
                            List.not_mem_nil._simp_1)
                          (or_false (ψ = φ)))))
                    (true_or (ψ = φ)))))
              (or_true (ψ.neg = ψ))))));
  have h2d := Logic.PropositionalLogic.Formula.Derivable.deduction h2;
  have h3 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.orElim)
        h1d)
      h2d;
  have h4 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.negIntro)
        (Logic.PropositionalLogic.Formula.Derivable.ax
          (Logic.PropositionalLogic.Formula.provable_self_imp (φ.or ψ))))
      h3;
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.deduction h4))

Complexity: 6085 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.negIntro, Logic.PropositionalLogic.Formula.Provable.orElim, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.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: Logic.PropositionalLogic.Formula.kalmar

NoteLogic.PropositionalLogic.HilbertSchema

The schemata of this Hilbert system: modus ponens, which is a simple rule since neither branch discharges anything, and the axioms, which are schemata with no branches at all.

inductive Logic.PropositionalLogic.HilbertSchema {α : Type} :
  Logic.ProofTheory.Schema (Logic.PropositionalLogic.Formula α) → Prop

• mp : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }

• k : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := φ.imp (ψ.imp φ) }

• s : ∀ (φ ψ χ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema
    { premises := [], conclusion := (φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ)) }

• andElim1 : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := (φ.and ψ).imp φ }

• andElim2 : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := (φ.and ψ).imp ψ }

• andIntro : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := φ.imp (ψ.imp (φ.and ψ)) }

• orIntro1 : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := φ.imp (φ.or ψ) }

• orIntro2 : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := ψ.imp (φ.or ψ) }

• orElim : ∀ (φ ψ χ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema
    { premises := [], conclusion := (φ.imp χ).imp ((ψ.imp χ).imp ((φ.or ψ).imp χ)) }

• negIntro : ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema
    { premises := [], conclusion := (φ.imp ψ).imp ((φ.imp ψ.neg).imp φ.neg) }

• dne : ∀ (φ : Logic.PropositionalLogic.Formula α),
  Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := φ.neg.neg.imp φ }

Show details

Outer dependencies: Logic.ProofTheory.Schema, Logic.PropositionalLogic.Formula

Lean core dependencies: List, Prod

Used by: Logic.PropositionalLogic.HilbertSchema.isAxiom_of_ne_mp, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom, Logic.PropositionalLogic.hilbert

NoteLogic.PropositionalLogic.hilbert

This Hilbert system, read as a proof system.

def Logic.PropositionalLogic.hilbert (α : Type) :
  Logic.ProofTheory.ProofSystem (Logic.PropositionalLogic.Formula α)

Show details

| Logic.PropositionalLogic.hilbert α =
  Logic.ProofTheory.Schema.system Logic.PropositionalLogic.HilbertSchema

Complexity: 11 (size of the value term)

Outer dependencies: Logic.ProofTheory.ProofSystem, Logic.PropositionalLogic.Formula

Inner dependencies: Logic.ProofTheory.Schema.system, Logic.PropositionalLogic.HilbertSchema

Used by: Logic.PropositionalLogic.Formula.Derivable.toProofSystem, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom

ImportantLogic.PropositionalLogic.HilbertSchema.isAxiom_of_ne_mp

Every axiom of the system is a schema with no branches.

theorem Logic.PropositionalLogic.HilbertSchema.isAxiom_of_ne_mp {α : Type}
  {s : Logic.ProofTheory.Schema (Logic.PropositionalLogic.Formula α)}
  (h : Logic.PropositionalLogic.HilbertSchema s)
  (hne :
    ∀ (φ ψ : Logic.PropositionalLogic.Formula α),
      s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) :
  s.IsAxiom

Show details

fun {α} {s} h hne =>
  Logic.PropositionalLogic.HilbertSchema.casesOn (motive := fun a t => s = a → h ≍ t → s.IsAxiom) h
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.mp φ ψ → s.IsAxiom)
        (fun h hne h_2 => absurd rfl (hne φ ψ)) (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.k φ ψ → s.IsAxiom)
        (fun h hne h_2 => Eq.refl { premises := [], conclusion := φ.imp (ψ.imp φ) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ χ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.s φ ψ χ → s.IsAxiom)
        (fun h hne h_2 =>
          Eq.refl
            { premises := [],
                conclusion := (φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ)) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.andElim1 φ ψ → s.IsAxiom)
        (fun h hne h_2 => Eq.refl { premises := [], conclusion := (φ.and ψ).imp φ }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.andElim2 φ ψ → s.IsAxiom)
        (fun h hne h_2 => Eq.refl { premises := [], conclusion := (φ.and ψ).imp ψ }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.andIntro φ ψ → s.IsAxiom)
        (fun h hne h_2 =>
          Eq.refl { premises := [], conclusion := φ.imp (ψ.imp (φ.and ψ)) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.orIntro1 φ ψ → s.IsAxiom)
        (fun h hne h_2 => Eq.refl { premises := [], conclusion := φ.imp (φ.or ψ) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.orIntro2 φ ψ → s.IsAxiom)
        (fun h hne h_2 => Eq.refl { premises := [], conclusion := ψ.imp (φ.or ψ) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ χ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.orElim φ ψ χ → s.IsAxiom)
        (fun h hne h_2 =>
          Eq.refl
            { premises := [],
                conclusion := (φ.imp χ).imp ((ψ.imp χ).imp ((φ.or ψ).imp χ)) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ ψ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.negIntro φ ψ → s.IsAxiom)
        (fun h hne h_2 =>
          Eq.refl
            { premises := [], conclusion := (φ.imp ψ).imp ((φ.imp ψ.neg).imp φ.neg) }.premises)
        (Eq.symm h_1) h hne)
    (fun φ h_1 =>
      Eq.ndrec (motive := fun {s} =>
        ∀ (h : Logic.PropositionalLogic.HilbertSchema s),
          (∀ (φ ψ : Logic.PropositionalLogic.Formula α),
              s ≠ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }) →
            h ≍ Logic.PropositionalLogic.HilbertSchema.dne φ → s.IsAxiom)
        (fun h hne h_2 => Eq.refl { premises := [], conclusion := φ.neg.neg.imp φ }.premises)
        (Eq.symm h_1) h hne)
    (Eq.refl s) (HEq.refl h)

Complexity: 9055 (size of the value term)

Dependencies: Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.IsAxiom, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.HilbertSchema

Lean core dependencies: Eq, Eq.symm, HEq, List, Ne, Prod, absurd, rfl

Used by: (none)

ImportantLogic.PropositionalLogic.HilbertSchema.mp_isSimple

Modus ponens is a simple rule: neither branch discharges anything.

theorem Logic.PropositionalLogic.HilbertSchema.mp_isSimple {α : Type}
  (φ ψ : Logic.PropositionalLogic.Formula α) :
  { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }.IsSimpleRule

Show details

fun {α} φ ψ p hp =>
  Or.casesOn (List.mem_cons.mp hp)
    (fun h =>
      Eq.ndrec (motive := fun p =>
        p ∈ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }.premises → p.1 = [])
        (fun hp => Eq.refl ([], φ.imp ψ).1) (Eq.symm h) hp)
    fun hp_1 =>
    Or.casesOn (List.mem_cons.mp hp_1)
      (fun h =>
        Eq.ndrec (motive := fun p =>
          p ∈ { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }.premises →
            p ∈ [([], φ)] → p.1 = [])
          (fun hp hp_2 => Eq.refl ([], φ).1) (Eq.symm h) hp hp_1)
      fun hp =>
      absurd hp (of_eq_true (Eq.trans (congrArg Not List.not_mem_nil._simp_1) not_false_eq_true))

Complexity: 2987 (size of the value term)

Dependencies: Logic.ProofTheory.Schema.IsSimpleRule, Logic.PropositionalLogic.Formula

Lean core dependencies: Eq, Eq.symm, Eq.trans, False, List, List.mem_cons, Not, Or, Prod, True, absurd, congrArg, not_false_eq_true, of_eq_true

Used by: (none)

ImportantLogic.PropositionalLogic.derivation_of_axiom

An axiom of the system yields a deduction against any list of hypotheses at all.

theorem Logic.PropositionalLogic.derivation_of_axiom {α : Type}
  (Γ : List (Logic.PropositionalLogic.Formula α)) (c : Logic.PropositionalLogic.Formula α)
  (h : Logic.PropositionalLogic.HilbertSchema { premises := [], conclusion := c }) :
  Logic.ProofTheory.Derivable (Logic.PropositionalLogic.hilbert α) Γ c

Show details

fun {α} Γ c h =>
  Nonempty.intro
    (Logic.ProofTheory.Derivation.apply ({ premises := [], conclusion := c }.instance Γ)
      (Exists.intro { premises := [], conclusion := c } (Exists.intro Γ ⟨h, rfl⟩))
      Logic.ProofTheory.DerivationsOf.nil)

Complexity: 457 (size of the value term)

Dependencies: Logic.ProofTheory.Derivable, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.HilbertSchema, Logic.PropositionalLogic.hilbert

Proof dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.Derivation, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.instance

Lean core dependencies: And, Eq, Exists, List, Prod, rfl

Used by: Logic.PropositionalLogic.Formula.Derivable.toProofSystem

ImportantLogic.PropositionalLogic.derivable_mp

Modus ponens, as an application of the system’s one simple rule.

theorem Logic.PropositionalLogic.derivable_mp {α : Type} {Γ : List (Logic.PropositionalLogic.Formula α)}
  {φ ψ : Logic.PropositionalLogic.Formula α}
  (h1 : Logic.ProofTheory.Derivable (Logic.PropositionalLogic.hilbert α) Γ (φ.imp ψ))
  (h2 : Logic.ProofTheory.Derivable (Logic.PropositionalLogic.hilbert α) Γ φ) :
  Logic.ProofTheory.Derivable (Logic.PropositionalLogic.hilbert α) Γ ψ

Show details

fun {α} {Γ} {φ ψ} h1 h2 =>
  Nonempty.intro
    (Logic.ProofTheory.Derivation.apply
      ({ premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }.instance Γ)
      (Exists.intro { premises := [([], φ.imp ψ), ([], φ)], conclusion := ψ }
        (Exists.intro Γ ⟨Logic.PropositionalLogic.HilbertSchema.mp φ ψ, rfl⟩))
      (Logic.ProofTheory.DerivationsOf.cons (Nonempty.some h1)
        (Logic.ProofTheory.DerivationsOf.cons (Nonempty.some h2)
          Logic.ProofTheory.DerivationsOf.nil)))

Complexity: 1933 (size of the value term)

Dependencies: Logic.ProofTheory.Derivable, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.hilbert

Proof dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.Derivation, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.instance, Logic.PropositionalLogic.HilbertSchema, instToSeqList

Mathlib dependencies: Nonempty.some

Lean core dependencies: And, Eq, Exists, List, List.map, Prod, rfl

Used by: Logic.PropositionalLogic.Formula.Derivable.toProofSystem

ImportantLogic.PropositionalLogic.Formula.Derivable.toProofSystem

Everything derivable in the inductive presentation is deducible in the proof system.

theorem Logic.PropositionalLogic.Formula.Derivable.toProofSystem {α : Type}
  {Γ : List (Logic.PropositionalLogic.Formula α)} {φ : Logic.PropositionalLogic.Formula α}
  (h : Logic.PropositionalLogic.Formula.Derivable Γ φ) :
  Logic.ProofTheory.Derivable (Logic.PropositionalLogic.hilbert α) Γ φ

Show details

fun {α} {Γ} {φ} h =>
  Logic.PropositionalLogic.Formula.Derivable.rec
    (fun {φ} hmem => Nonempty.intro (Logic.ProofTheory.Derivation.assumption hmem))
    (fun {φ ψ} a a_1 ih1 ih2 => Logic.PropositionalLogic.derivable_mp ih1 ih2)
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ (φ.imp (ψ.imp φ))
        (Logic.PropositionalLogic.HilbertSchema.k φ ψ))
    (fun {φ ψ χ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ
        ((φ.imp (ψ.imp χ)).imp ((φ.imp ψ).imp (φ.imp χ)))
        (Logic.PropositionalLogic.HilbertSchema.s φ ψ χ))
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ ((φ.and ψ).imp φ)
        (Logic.PropositionalLogic.HilbertSchema.andElim1 φ ψ))
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ ((φ.and ψ).imp ψ)
        (Logic.PropositionalLogic.HilbertSchema.andElim2 φ ψ))
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ (φ.imp (ψ.imp (φ.and ψ)))
        (Logic.PropositionalLogic.HilbertSchema.andIntro φ ψ))
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ (φ.imp (φ.or ψ))
        (Logic.PropositionalLogic.HilbertSchema.orIntro1 φ ψ))
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ (ψ.imp (φ.or ψ))
        (Logic.PropositionalLogic.HilbertSchema.orIntro2 φ ψ))
    (fun {φ ψ χ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ
        ((φ.imp χ).imp ((ψ.imp χ).imp ((φ.or ψ).imp χ)))
        (Logic.PropositionalLogic.HilbertSchema.orElim φ ψ χ))
    (fun {φ ψ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ ((φ.imp ψ).imp ((φ.imp ψ.neg).imp φ.neg))
        (Logic.PropositionalLogic.HilbertSchema.negIntro φ ψ))
    (fun {φ} =>
      Logic.PropositionalLogic.derivation_of_axiom Γ (φ.neg.neg.imp φ)
        (Logic.PropositionalLogic.HilbertSchema.dne φ))
    h

Complexity: 633 (size of the value term)

Dependencies: Logic.ProofTheory.Derivable, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.hilbert

Proof dependencies: Logic.ProofTheory.Derivation, Logic.PropositionalLogic.derivable_mp, Logic.PropositionalLogic.derivation_of_axiom

Lean core dependencies: List

Used by: (none)

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