Demonstrability

Difficulty: hard — 5 definitions, 0 abbreviations, 4 lemmas, 3 theorems, 0 examples.

definition lemma theorem
legend

Relative demonstrability: a second relation, sitting on top of a basis, that allows several conclusions at once rather than only one.

Deducibility asks whether one conclusion follows from a list of premises. Demonstrability asks whether, given the premises, at least one of several conclusions must hold. Reading the two sides that way, four familiar properties are just the cases where one side is empty: a statement that holds outright, a list of statements that cannot all fail, a statement that cannot hold, and a list of statements that cannot all hold.

The definition threads an arbitrary further list of statements, a context, through both sides. That is what makes Cut hold: the simpler context-free version of the definition does not support it.

Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: section 4.2 (complementarity and demonstrability), section 4.3 (contradictoriness and refutability), section 4.4 (relative demonstrability, the definitions \(D\vdash_2\) and \(D\vdash_3\)), section 4.5 (Cut, Theorems 4.7-4.9).

Relative demonstrability (Popper’s \(P \vdash Q\), between a list of premises and a list of conclusions): for every statement and every context, if each conclusion together with that context deduces the statement, then so do the premises together with the same context. Threading a context through both sides is what makes Cut hold below; the simpler context-free definition does not.

relative-demonstrability
def Logic.Popper.Basis1.Demonstrate {Obj : Type} (S : Logic.Popper.Basis1 Obj) (P Q : List Obj) : Prop
Show details 
| S.Demonstrate P Q =
  ∀ (c : Obj) (D : List Obj),
    (∀ b ∈ Q, Logic.Popper.Basis1.Deduce ⟪b, D⟫ c) → Logic.Popper.Basis1.Deduce ⟪P, D⟫ c

Complexity: 155 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: instToSeq, instToSeqList

Lean core dependencies: List

Used by: Logic.Popper.Basis1.Complementary, Logic.Popper.Basis1.Contradictory, Logic.Popper.Basis1.Demonstrable, Logic.Popper.Basis1.IsClassicalNegation, Logic.Popper.Basis1.IsConjunction, Logic.Popper.Basis1.IsDisjunction, Logic.Popper.Basis1.IsImplication, Logic.Popper.Basis1.IsIntuitionisticNegation, Logic.Popper.Basis1.Refutable, Logic.Popper.Basis1.contradictory_of_isClassicalNegation, Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation, Logic.Popper.Basis1.cut, Logic.Popper.Basis1.demonstrate_congr_conclusion, Logic.Popper.Basis1.demonstrate_congr_premise, Logic.Popper.Basis1.demonstrate_cons_of_isConjunction, Logic.Popper.Basis1.demonstrate_cons_of_isDisjunction, Logic.Popper.Basis1.demonstrate_mono, Logic.Popper.Basis1.demonstrate_mp, Logic.Popper.Basis1.demonstrate_of_contradictory, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.demonstrate_singleton, Logic.Popper.Basis1.isClassicalNegation_congr, Logic.Popper.Basis1.isClassicalNegation_unique, Logic.Popper.Basis1.isConjunction_congr, Logic.Popper.Basis1.isConjunction_unique, Logic.Popper.Basis1.isDisjunction_congr, Logic.Popper.Basis1.isDisjunction_unique, Logic.Popper.Basis1.isImplication_congr, Logic.Popper.Basis1.isImplication_unique, Logic.Popper.Basis1.isIntuitionisticNegation_congr, Logic.Popper.Basis1.isIntuitionisticNegation_unique, Logic.Popper.Basis1.mutual_of_demonstrate, Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons, Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons, Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.Formula.syntactic_iff_provable, Logic.PropositionalLogic.semanticConnectives, Logic.PropositionalLogic.syntacticConnectives

Cut. If the premises demonstrate the conclusions together with some extra statement, and that statement together with the premises demonstrates the conclusions, then the premises alone already demonstrate the conclusions: the extra statement need not survive on either side.

cut
theorem Logic.Popper.Basis1.cut {Obj : Type} (S : Logic.Popper.Basis1 Obj) (P Q : List Obj) (e : Obj)
  (A : S.Demonstrate P ⟪Q, e⟫) (B : S.Demonstrate ⟪e, P⟫ Q) : S.Demonstrate P Q
Show details 
fun {Obj} S P Q e A B c D HQ =>
  have Be := B c D HQ;
  have hA := fun b hb =>
    Or.casesOn (List.mem_append.mp hb)
      (fun hbq =>
        Logic.Popper.Basis1.mono S
          (fun x hx =>
            Or.casesOn (List.mem_cons.mp hx) (fun h => List.mem_cons.mpr (Or.inl h)) fun h =>
              List.mem_cons.mpr (Or.inr (List.mem_append.mpr (Or.inr h))))
          (HQ b hbq))
      fun hbe =>
      have hbe' := List.mem_singleton.mp hbe;
      Eq.ndrec (motive := fun e =>
        S.Demonstrate P ⟪Q, e⟫ →
          S.Demonstrate ⟪e, P⟫ Q →
            Logic.Popper.Basis1.Deduce (e :: (P ++ D)) c →
              b ∈ Q ++ [e] → b ∈ [e] → Logic.Popper.Basis1.Deduce (b :: (P ++ D)) c)
        (fun A B Be hb hbe => Be) hbe' A B Be hb hbe;
  have hPP := A c (P ++ D) hA;
  Logic.Popper.Basis1.mono S
    (fun x hx =>
      Or.casesOn (List.mem_append.mp hx) (fun h => List.mem_append.mpr (Or.inl h)) fun h => h)
    hPP

Complexity: 3159 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.mono

Lean core dependencies: Eq, List, List.append, List.mem_append, List.mem_cons, List.mem_singleton, Or

Used by: (none)

Demonstrability depends on its two sides only through membership: growing either list can only make a demonstrability claim easier to establish.

theorem Logic.Popper.Basis1.demonstrate_mono {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {P P' Q Q' : List Obj} (hP : ∀ a ∈ P, a ∈ P') (hQ : ∀ a ∈ Q, a ∈ Q') (h : S.Demonstrate P Q) :
  S.Demonstrate P' Q'
Show details 
fun {Obj} S {P P' Q Q'} hP hQ h c D hD =>
  Logic.Popper.Basis1.mono S
    (fun x hx =>
      Or.casesOn (List.mem_append.mp hx) (fun hx => List.mem_append.mpr (Or.inl (hP x hx)))
        fun hx => List.mem_append.mpr (Or.inr hx))
    (h c D fun b hb => hD b (hQ b hb))

Complexity: 1239 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate

Proof dependencies: Logic.Popper.Basis1.mono, instToSeq, instToSeqList

Lean core dependencies: List, List.mem_append, Or

Used by: Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation, Logic.Popper.Basis1.demonstrate_of_contradictory, Logic.Popper.Basis1.isClassicalNegation_unique

A statement occurring on both sides settles the claim outright, with no further assumption on the basis. This is what lets a longer list stand in for a shorter one whenever the extra members are already implied both ways.

theorem Logic.Popper.Basis1.demonstrate_of_mem {Obj : Type} (S : Logic.Popper.Basis1 Obj) {P Q : List Obj}
  {a : Obj} (hP : a ∈ P) (hQ : a ∈ Q) : S.Demonstrate P Q
Show details 
fun {Obj} S {P Q} {a} hP hQ c D hD =>
  Logic.Popper.Basis1.tg (P ++ D) (a :: D) c
    (fun x hx =>
      Or.casesOn (List.mem_cons.mp hx)
        (fun heq =>
          Eq.mpr (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce (P ++ D) _a) heq))
            (Logic.Popper.Basis1.rg (P ++ D) a (List.mem_append.mpr (Or.inl hP))))
        fun hx => Logic.Popper.Basis1.rg (P ++ D) x (List.mem_append.mpr (Or.inr hx)))
    (hD a hQ)

Complexity: 899 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate

Proof dependencies: instToSeq, instToSeqList

Lean core dependencies: Eq, Eq.mpr, List, List.mem_append, List.mem_cons, Or, congrArg, id

Used by: Logic.Popper.Basis1.contradictory_of_isClassicalNegation, Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation, Logic.Popper.Basis1.demonstrate_cons_of_isConjunction, Logic.Popper.Basis1.demonstrate_cons_of_isDisjunction, Logic.Popper.Basis1.demonstrate_mp, Logic.Popper.Basis1.isClassicalNegation_unique, Logic.Popper.Basis1.isConjunction_unique, Logic.Popper.Basis1.isDisjunction_unique, Logic.Popper.Basis1.isImplication_unique, Logic.Popper.Basis1.isIntuitionisticNegation_unique

Between a single premise and a single conclusion, demonstrability is just deducibility: threading a context through a single pair adds nothing.

theorem Logic.Popper.Basis1.demonstrate_singleton {Obj : Type} (S : Logic.Popper.Basis1 Obj) {a b : Obj} :
  S.Demonstrate ⟪a⟫ ⟪b⟫ ↔ S.Follows a b
Show details 
fun {Obj} S {a b} =>
  {
    mp := fun h =>
      have this :=
        h b [] fun x hx =>
          Eq.ndrec (motive := fun {b} =>
            S.Demonstrate ⟪a⟫ ⟪b⟫ → Logic.Popper.Basis1.Deduce ⟪x, []⟫ b)
            (fun h =>
              Logic.Popper.Basis1.rg ⟪x⟫ x
                (of_eq_true
                  (Eq.trans List.mem_cons._simp_1
                    (Eq.trans (congr (congrArg Or (eq_self x)) List.not_mem_nil._simp_1)
                      (or_false True)))))
            (Eq.mp Logic.Popper.Basis1.demonstrate_singleton._simp_1_1 hx) h;
      id
        (id (Eq.mp (congrFun' (congrArg Logic.Popper.Basis1.Deduce (List.append_nil [a])) b) this)),
    mpr := fun h c D hD =>
      Logic.Popper.Basis1.tg ⟪a, D⟫ ⟪b, D⟫ c
        (fun x hx =>
          Or.casesOn (List.mem_cons.mp hx)
            (fun h_1 =>
              Eq.ndrec (motive := fun {b} =>
                S.Follows a b →
                  (∀ b_1 ∈ ⟪b⟫, Logic.Popper.Basis1.Deduce ⟪b_1, D⟫ c) →
                    x ∈ ⟪b, D⟫ → Logic.Popper.Basis1.Deduce ⟪a, D⟫ x)
                (fun h hD hx =>
                  Logic.Popper.Basis1.mono S
                    (fun y hy => List.mem_cons.mpr (Or.inl (List.mem_singleton.mp hy))) h)
                h_1 h hD hx)
            fun hx => Logic.Popper.Basis1.rg (a :: D) x (List.mem_cons.mpr (Or.inr hx)))
        (hD b
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans (congr (congrArg Or (eq_self b)) List.not_mem_nil._simp_1)
                (or_false True))))) }

Complexity: 2538 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Follows, instToSeq

Proof dependencies: Logic.Popper.Basis1.mono, instToSeqList

Lean core dependencies: Eq, Eq.mp, Eq.trans, False, Iff, List, List.append, List.append_nil, List.mem_cons, List.mem_singleton, Or, True, congr, congrArg, congrFun', eq_self, id, of_eq_true, or_false

Used by: Logic.Popper.Basis1.mutual_of_demonstrate, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.Formula.syntactic_iff_provable

Replacing a premise by one mutually deducible with it leaves a demonstrability claim standing.

theorem Logic.Popper.Basis1.demonstrate_congr_premise {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {P Q R : List Obj} {a b : Obj} (h : S.Mutual a b) (hd : S.Demonstrate ⟪P, a, Q⟫ R) :
  S.Demonstrate ⟪P, b, Q⟫ R
Show details 
fun {Obj} S {P Q R} {a b} h hd c D hD =>
  have key :=
    have h1 := hd c D hD;
    Eq.mp (congrArg (fun _a => Logic.Popper.Basis1.Deduce (P ++ (_a ++ D)) c) List.cons_append)
      (Eq.mp
        (congrArg (fun _a => Logic.Popper.Basis1.Deduce _a c) (List.append_assoc P ([a] ++ Q) D))
        h1);
  have h2 :=
    (Logic.Popper.Basis1.substitutivity S
          (List.rel_append (Logic.Popper.Basis1.forall₂_mutual_refl S P)
            (List.Forall₂.cons h (Logic.Popper.Basis1.forall₂_mutual_refl S (Q ++ D))))
          ⟨Logic.Popper.Basis1.follows_refl S c, Logic.Popper.Basis1.follows_refl S c⟩).mp
      key;
  have h3 := h2;
  id
    (Eq.mp
      (congrArg (fun _a => Logic.Popper.Basis1.Deduce _a c)
        (Eq.symm (List.append_assoc P (b :: Q) D)))
      (Eq.mp
        (congrArg (fun _a => Logic.Popper.Basis1.Deduce (P ++ _a) c) (Eq.symm List.cons_append))
        h3))

Complexity: 2833 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Mutual, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.follows_refl, Logic.Popper.Basis1.forall₂_mutual_refl, Logic.Popper.Basis1.substitutivity

Mathlib dependencies: List.rel_append

Lean core dependencies: Eq.mp, Eq.symm, List, List.append_assoc, List.cons_append, congrArg, id

Used by: Logic.Popper.Basis1.isClassicalNegation_congr, Logic.Popper.Basis1.isConjunction_congr

Replacing a conclusion by one mutually deducible with it leaves a demonstrability claim standing.

theorem Logic.Popper.Basis1.demonstrate_congr_conclusion {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {P Q R : List Obj} {a b : Obj} (h : S.Mutual a b) (hd : S.Demonstrate P ⟪Q, a, R⟫) :
  S.Demonstrate P ⟪Q, b, R⟫
Show details 
fun {Obj} S {P Q R} {a b} h hd c D hD =>
  hd c D fun x hx =>
    Or.casesOn (List.mem_append.mp hx) (fun hx => hD x (List.mem_append.mpr (Or.inl hx)))
      fun hx_1 =>
      Or.casesOn (List.mem_cons.mp hx_1)
        (fun h_1 =>
          Eq.ndrec (motive := fun {a} =>
            S.Mutual a b →
              S.Demonstrate P ⟪Q, a, R⟫ →
                x ∈ ⟪Q, a, R⟫ → x ∈ ⟪a, R⟫ → Logic.Popper.Basis1.Deduce ⟪x, D⟫ c)
            (fun h hd hx hx_2 =>
              have hb := hD b (List.mem_append.mpr (Or.inr List.mem_cons_self));
              Logic.Popper.Basis1.tg (x :: D) (b :: D) c
                (fun y hy =>
                  Or.casesOn (List.mem_cons.mp hy)
                    (fun h_2 =>
                      Eq.ndrec (motive := fun {b} =>
                        (∀ b_1 ∈ ⟪Q, b, R⟫, Logic.Popper.Basis1.Deduce ⟪b_1, D⟫ c) →
                          S.Mutual x b →
                            Logic.Popper.Basis1.Deduce (b :: D) c →
                              y ∈ b :: D → Logic.Popper.Basis1.Deduce (x :: D) y)
                        (fun hD h hb hy =>
                          Logic.Popper.Basis1.mono S
                            (fun z hz => Eq.symm (List.mem_singleton.mp hz) ▸ List.mem_cons_self)
                            h.left)
                        h_2 hD h hb hy)
                    fun hy => Logic.Popper.Basis1.rg (x :: D) y (List.mem_cons.mpr (Or.inr hy)))
                hb)
            h_1 h hd hx hx_1)
        fun hx => hD x (List.mem_append.mpr (Or.inr (List.mem_cons.mpr (Or.inr hx))))

Complexity: 4202 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Mutual, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.mono

Lean core dependencies: Eq, Eq.symm, List, List.append, List.mem_append, List.mem_cons, List.mem_cons_self, List.mem_singleton, Or

Used by: Logic.Popper.Basis1.isDisjunction_congr, Logic.Popper.Basis1.isImplication_congr, Logic.Popper.Basis1.isIntuitionisticNegation_congr

\(a\) is demonstrable: it holds no matter what, so it follows from any statement whatsoever. The case of demonstrability with no premises and a single conclusion.

demonstrable
def Logic.Popper.Basis1.Demonstrable {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a : Obj) : Prop
Show details 
| S.Demonstrable a = S.Demonstrate [] ⟪a⟫

Complexity: 29 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq

Used by: (none)

\(Q\) is complementary: its members exhaust the possibilities, so at least one of them holds. The case of demonstrability with no premises.

complementarity
def Logic.Popper.Basis1.Complementary {Obj : Type} (S : Logic.Popper.Basis1 Obj) (Q : List Obj) : Prop
Show details 
| S.Complementary Q = S.Demonstrate [] Q

Complexity: 21 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate

Lean core dependencies: List

Used by: (none)

\(a\) is refutable: it fails no matter what, so any statement at all follows from it. The case of demonstrability with a single premise and no conclusions.

refutable
def Logic.Popper.Basis1.Refutable {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a : Obj) : Prop
Show details 
| S.Refutable a = S.Demonstrate ⟪a⟫ []

Complexity: 29 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq

Used by: (none)

\(P\) is contradictory: its members cannot all hold together. The case of demonstrability with no conclusions.

contradictory
def Logic.Popper.Basis1.Contradictory {Obj : Type} (S : Logic.Popper.Basis1 Obj) (P : List Obj) : Prop
Show details 
| S.Contradictory P = S.Demonstrate P []

Complexity: 21 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate

Lean core dependencies: List

Used by: Logic.Popper.Basis1.contradictory_of_isClassicalNegation, Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation, Logic.Popper.Basis1.demonstrate_of_contradictory

Premises that cannot all hold demonstrate whatever one likes: with nothing left to conclude, any list of conclusions will do.

theorem Logic.Popper.Basis1.demonstrate_of_contradictory {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {P : List Obj} (h : S.Contradictory P) (Q : List Obj) : S.Demonstrate P Q
Show details 
fun {Obj} S {P} h Q =>
  Logic.Popper.Basis1.demonstrate_mono S (fun x hx => hx)
    (fun x hx =>
      absurd hx (of_eq_true (Eq.trans (congrArg Not List.not_mem_nil._simp_1) not_false_eq_true)))
    h

Complexity: 205 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Contradictory, Logic.Popper.Basis1.Demonstrate

Proof dependencies: Logic.Popper.Basis1.demonstrate_mono

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

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