Basis1

Difficulty: hard — 3 definitions, 0 abbreviations, 2 lemmas, 6 theorems, 0 examples.

definition lemma theorem

legend

Popper’s Basis I: deducibility from a list of premises, and the structural rules that come with it.

Basis I has two closure conditions: generalized reflexivity and generalized transitivity. Generalized reflexivity says that every premise is deducible, and generalized transitivity allows a chain of deductions to compose.

Everything else follows from these two conditions: the list of premises can be reordered (exchange), new premises can be added (weaken), or a repeated premise removed (contraction).

Basis III already fixes deducibility between two single statements. Basis I adds the many-premise relation on top. It requires the two-place ‘follows’ relation matches exactly with the single premise deduces. This way, a Basis III always generates a Basis I.

Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: section 3.4 (Basis I), section 4.6 (the rules (Rg) and (Tg)).

Logic.Popper.Basis1

Basis I. Deducibility from a finite list of premises (Popper’s \(a_1, \dots, a_n / b\)), carried on top of a Basis III over the same statements. Two closure conditions axiomatise it: every premise is deducible from the whole list of premises, and a chain of deductions composes. A third condition ties the two relations together, so a basis cannot say one thing about a single premise and something else about that same premise on its own.

basis

structure Logic.Popper.Basis1 (Obj : Type) : Type

\(b\) is deducible from the premises \(P\).
```
Deduce : List Obj → Obj → Prop
```
Generalised reflexivity: each premise is itself deducible from the whole list of premises.
```
rg : ∀ (P : List Obj), ∀ a ∈ P, Logic.Popper.Basis1.Deduce P a
```

Generalised transitivity: if one list of premises deduces every member of a second list, and the second list deduces some conclusion, then so does the first.

tg : ∀ (P B : List Obj) (c : Obj),
(∀ b ∈ B, Logic.Popper.Basis1.Deduce P b) →
  Logic.Popper.Basis1.Deduce B c → Logic.Popper.Basis1.Deduce P c

Show details

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, List, eq_of_heq

Logic.Popper.Basis1.mono

Premise monotonicity: whenever every premise of one deduction also occurs among the premises of another, the conclusion carries over. This is the single fact behind all three structural rules below, and it follows from reflexivity and transitivity alone.

theorem Logic.Popper.Basis1.mono {Obj : Type} (S : Logic.Popper.Basis1 Obj) {P P' : List Obj} {c : Obj}
  (h : ∀ a ∈ P, a ∈ P') (hc : Logic.Popper.Basis1.Deduce P c) : Logic.Popper.Basis1.Deduce P' c

Show details

fun {Obj} S {P P'} {c} h hc =>
  Logic.Popper.Basis1.tg P' P c (fun b hb => Logic.Popper.Basis1.rg P' b (h b hb)) hc

Complexity: 107 (size of the value term)

Dependencies: Logic.Popper.Basis1

Lean core dependencies: List

Used by: Logic.Popper.Basis1.contract, Logic.Popper.Basis1.cut, Logic.Popper.Basis1.demonstrate_congr_conclusion, Logic.Popper.Basis1.demonstrate_mono, Logic.Popper.Basis1.demonstrate_singleton, Logic.Popper.Basis1.exchange, Logic.Popper.Basis1.substitutivity, Logic.Popper.Basis1.weaken

Logic.Popper.Basis1.exchange

Exchange: swapping two neighbouring premises makes no difference. Popper’s rule (2.3), which he lists as a possible component of a basis rather than a consequence of one.

exchange-of-premises

theorem Logic.Popper.Basis1.exchange {Obj : Type} (S : Logic.Popper.Basis1 Obj) {P Q : List Obj}
  {a b c : Obj} (h : Logic.Popper.Basis1.Deduce ⟪P, a, b, Q⟫ c) :
  Logic.Popper.Basis1.Deduce ⟪P, b, a, Q⟫ c

Show details

fun {Obj} S {P Q} {a b c} h =>
  Logic.Popper.Basis1.mono S
    (fun x hx =>
      Eq.mpr
        (id
          (Eq.trans Logic.Popper.Basis1.exchange._simp_1_1
            (congrArg (Or (x ∈ P))
              (Eq.trans Logic.Popper.Basis1.exchange._simp_1_1
                (congr (congrArg Or Logic.Popper.Basis1.exchange._simp_1_2)
                  (Eq.trans Logic.Popper.Basis1.exchange._simp_1_1
                    (congrFun' (congrArg Or Logic.Popper.Basis1.exchange._simp_1_2) (x ∈ Q))))))))
        (Or.casesOn
          (Eq.mp
            (Eq.trans Logic.Popper.Basis1.exchange._simp_1_1
              (congrArg (Or (x ∈ P))
                (Eq.trans Logic.Popper.Basis1.exchange._simp_1_1
                  (congr (congrArg Or Logic.Popper.Basis1.exchange._simp_1_2)
                    (Eq.trans Logic.Popper.Basis1.exchange._simp_1_1
                      (congrFun' (congrArg Or Logic.Popper.Basis1.exchange._simp_1_2) (x ∈ Q)))))))
            hx)
          (fun h => or_iff_not_imp_left.mpr fun a_1 => False.elim (a_1 h)) fun h =>
          Or.casesOn h
            (fun h =>
              or_iff_not_imp_left.mpr fun a_1 =>
                or_iff_not_imp_left.mpr fun a_2 =>
                  or_iff_not_imp_left.mpr fun a => False.elim (a h))
            fun h =>
            Or.casesOn h
              (fun h =>
                or_iff_not_imp_left.mpr fun a_1 =>
                  or_iff_not_imp_left.mpr fun a_2 => False.elim (a_2 h))
              fun h =>
              or_iff_not_imp_left.mpr fun a_1 =>
                or_iff_not_imp_left.mpr fun a_2 => or_iff_not_imp_left.mpr fun a => h))
    h

Complexity: 5331 (size of the value term)

Dependencies: Logic.Popper.Basis1, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.mono

Lean core dependencies: Classical.or_iff_not_imp_left, Eq, Eq.mp, Eq.mpr, Eq.trans, False.elim, List, List.mem_append, List.mem_singleton, Not, Or, congr, congrArg, congrFun', id

Used by: (none)

Logic.Popper.Basis1.weaken

Weakening: further premises, however many and wherever they are used, never spoil a deduction. Popper’s rule (2.2).

weakening-of-premises

theorem Logic.Popper.Basis1.weaken {Obj : Type} (S : Logic.Popper.Basis1 Obj) {P R : List Obj} {c : Obj}
  (h : Logic.Popper.Basis1.Deduce P c) : Logic.Popper.Basis1.Deduce ⟪P, R⟫ c

Show details

fun {Obj} S {P R} {c} h =>
  Logic.Popper.Basis1.mono S (fun x hx => List.mem_append.mpr (Or.inl hx)) h

Complexity: 351 (size of the value term)

Dependencies: Logic.Popper.Basis1, instToSeqList

Proof dependencies: Logic.Popper.Basis1.mono

Lean core dependencies: List, List.mem_append, Or

Used by: (none)

Logic.Popper.Basis1.contract

Contraction: a premise listed twice in a row says no more than the same premise listed once.

contraction-of-premises

theorem Logic.Popper.Basis1.contract {Obj : Type} (S : Logic.Popper.Basis1 Obj) {P Q : List Obj} {a c : Obj}
  (h : Logic.Popper.Basis1.Deduce ⟪P, a, a, Q⟫ c) : Logic.Popper.Basis1.Deduce ⟪P, a, Q⟫ c

Show details

fun {Obj} S {P Q} {a c} h =>
  Logic.Popper.Basis1.mono S
    (fun x hx =>
      Eq.mpr
        (id
          (Eq.trans Logic.Popper.Basis1.contract._simp_1_1
            (congrArg (Or (x ∈ P))
              (Eq.trans Logic.Popper.Basis1.contract._simp_1_1
                (congrFun' (congrArg Or Logic.Popper.Basis1.contract._simp_1_2) (x ∈ Q))))))
        (Or.casesOn
          (Eq.mp
            (Eq.trans Logic.Popper.Basis1.contract._simp_1_1
              (congrArg (Or (x ∈ P))
                (Eq.trans Logic.Popper.Basis1.contract._simp_1_1
                  (congr (congrArg Or Logic.Popper.Basis1.contract._simp_1_2)
                    (Eq.trans Logic.Popper.Basis1.contract._simp_1_1
                      (congrFun' (congrArg Or Logic.Popper.Basis1.contract._simp_1_2) (x ∈ Q)))))))
            hx)
          (fun h => or_iff_not_imp_left.mpr fun a_1 => False.elim (a_1 h)) fun h =>
          Or.casesOn h
            (fun h =>
              or_iff_not_imp_left.mpr fun a_1 => or_iff_not_imp_left.mpr fun a => False.elim (a h))
            fun h =>
            Or.casesOn h
              (fun h =>
                or_iff_not_imp_left.mpr fun a_1 =>
                  or_iff_not_imp_left.mpr fun a => False.elim (a h))
              fun h => or_iff_not_imp_left.mpr fun a_1 => or_iff_not_imp_left.mpr fun a => h))
    h

Complexity: 4185 (size of the value term)

Dependencies: Logic.Popper.Basis1, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.mono

Used by: (none)

Logic.Popper.Basis1.Follows

\(b\) follows from \(a\): the one-premise case of deducibility. Popper writes \(a / b\), and the two readings are the same relation, so nothing has to relate them.

follows

def Logic.Popper.Basis1.Follows {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a b : Obj) : Prop

Show details

| S.Follows a b = Logic.Popper.Basis1.Deduce ⟪a⟫ b

Complexity: 29 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: instToSeq

Logic.Popper.Basis1.follows_refl

Every statement follows from itself.

reflexivity

theorem Logic.Popper.Basis1.follows_refl {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a : Obj) :
  S.Follows a a

Show details

fun {Obj} S a =>
  Logic.Popper.Basis1.rg ⟪a⟫ a
    (of_eq_true
      (Eq.trans List.mem_cons._simp_1
        (Eq.trans (congr (congrArg Or (eq_self a)) List.not_mem_nil._simp_1) (or_false True))))

Complexity: 239 (size of the value term)

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

Proof dependencies: instToSeq

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

Used by: Logic.Popper.Basis1.demonstrate_congr_premise, Logic.Popper.Basis1.forall₂_mutual_refl

Logic.Popper.Basis1.follows_trans

What follows from what follows from \(a\), follows from \(a\).

transitivity

theorem Logic.Popper.Basis1.follows_trans {Obj : Type} (S : Logic.Popper.Basis1 Obj) {a b c : Obj}
  (h1 : S.Follows a b) (h2 : S.Follows b c) : S.Follows a c

Show details

fun {Obj} S {a b c} h1 h2 =>
  Logic.Popper.Basis1.tg ⟪a⟫ ⟪b⟫ c
    (fun x hx =>
      Eq.symm
          (Eq.mp
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans (congrArg (Or (x = b)) List.not_mem_nil._simp_1) (or_false (x = b))))
            hx) ▸
        h1)
    h2

Complexity: 359 (size of the value term)

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

Proof dependencies: instToSeq

Lean core dependencies: Eq, Eq.mp, Eq.symm, Eq.trans, False, List, Or, congrArg, or_false

Used by: (none)

Logic.Popper.Basis1.Mutual

Mutual deducibility: \(a\) and \(b\) each follow from the other. Popper writes \(a \sslash b\) and says the two statements have the same logical force.

mutual-deducibility

def Logic.Popper.Basis1.Mutual {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a b : Obj) : Prop

Show details

| S.Mutual a b = (S.Follows a b ∧ S.Follows b a)

Complexity: 31 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Follows

Lean core dependencies: And

Logic.Popper.Basis1.forall₂_mutual_refl

Every list of statements has the same logical force as itself.

theorem Logic.Popper.Basis1.forall₂_mutual_refl {Obj : Type} (S : Logic.Popper.Basis1 Obj) (P : List Obj) :
  List.Forall₂ S.Mutual P P

Show details

fun {Obj} S P =>
  List.forall₂_same.mpr fun x x_1 =>
    ⟨Logic.Popper.Basis1.follows_refl S x, Logic.Popper.Basis1.follows_refl S x⟩

Complexity: 123 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Mutual

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

Mathlib dependencies: List.forall₂_same

Lean core dependencies: List

Used by: Logic.Popper.Basis1.demonstrate_congr_premise

Logic.Popper.Basis1.substitutivity

Substitutivity: a deduction sees its premises and its conclusion only up to mutual deducibility. Replacing each premise, and the conclusion, by statements of the same logical force leaves the deduction standing, and does so in every position at once.

substitutivity

theorem Logic.Popper.Basis1.substitutivity {Obj : Type} (S : Logic.Popper.Basis1 Obj) {P P' : List Obj}
  {a b : Obj} (hP : List.Forall₂ S.Mutual P P') (hab : S.Mutual a b) :
  Logic.Popper.Basis1.Deduce P a ↔ Logic.Popper.Basis1.Deduce P' b

Show details

fun {Obj} S {P P'} {a b} hP hab =>
  have symm := fun {L L'} h =>
    List.Forall₂.rec List.Forall₂.nil
      (fun {a b} {l₁ l₂} hpq a_1 ih => List.Forall₂.cons ⟨hpq.right, hpq.left⟩ ih) h;
  have key := fun {L L'} {c d} hL hcd h =>
    have hprem :=
      List.Forall₂.rec (motive := fun {L L'} hL => ∀ x ∈ L, Logic.Popper.Basis1.Deduce L' x)
        (fun x hx =>
          List.Mem.casesOn (motive := fun a t => [] = a → hx ≍ t → Logic.Popper.Basis1.Deduce [] x)
            hx (fun as h => False.elim (noConfusion_of_Nat List.ctorIdx h))
            (fun b {as} a h => False.elim (noConfusion_of_Nat List.ctorIdx h)) (Eq.refl [])
            (HEq.refl hx))
        (fun {p q} {L₀ L₀'} hpq a ih x hx =>
          Or.casesOn (List.mem_cons.mp hx)
            (fun h =>
              Eq.ndrec (motive := fun {p} =>
                S.Mutual p q → x ∈ p :: L₀ → Logic.Popper.Basis1.Deduce (q :: L₀') x)
                (fun hpq hx =>
                  Logic.Popper.Basis1.tg (q :: L₀') ⟪q⟫ x
                    (fun y hy =>
                      List.mem_singleton.mp hy ▸
                        Eq.symm (List.mem_singleton.mp hy) ▸
                          Logic.Popper.Basis1.rg (q :: L₀') q List.mem_cons_self)
                    hpq.right)
                h hpq hx)
            fun hx =>
            Logic.Popper.Basis1.mono S (fun y hy => List.mem_cons.mpr (Or.inr hy)) (ih x hx))
        hL;
    Logic.Popper.Basis1.tg L' ⟪c⟫ d
      (fun y hy => Eq.symm (List.mem_singleton.mp hy) ▸ Logic.Popper.Basis1.tg L' L c hprem h)
      hcd.left;
  { mp := key hP hab, mpr := key (symm hP) ⟨hab.right, hab.left⟩ }

Complexity: 1910 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Mutual

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

Lean core dependencies: Eq, Eq.symm, False.elim, HEq, Iff, List, List.Mem, List.mem_cons, List.mem_cons_self, List.mem_singleton, Or, noConfusion_of_Nat

Used by: Logic.Popper.Basis1.demonstrate_congr_premise

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