Basis3
Difficulty: moderate — 4 definitions, 0 abbreviations, 2 lemmas, 2 theorems, 1 examples.
Popper’s Basis III: deducibility taken as a primitive relation between single objects, from which the many-premise relation of Basis I is recovered.
Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: end of section 4.7 (Basis III). Popper (1948a) introduces Basis III; Popper (1949a) adopts two-place deducibility as the sole primitive notion.
Popper.Basis3
Basis III. A primitive relation between single objects (Popper’s \(a / b\), read “\(b\) is deducible from \(a\)”), characterised as a preorder. This is Popper’s final basis: it avoids the schematic transitivity rule of Basis I by taking the two-place relation as fundamental and defining every many-premise notion from it.
Popper.Basis3 : Type 1
Show details
| Popper.Basis3.mk : (Obj : Type) → (Deduce : Obj → Obj → Prop) → (∀ (a : Obj), Deduce a a) → (∀ {a b c : Obj}, Deduce a b → Deduce b c → Deduce a c) → Popper.Basis3
Outer dependencies: (none)
Popper.Basis3.NDeduce
The many-premise deducibility of Basis I, defined from Basis III’s two-place deducibility: an object is deducible from a list of premises exactly when every object that deduces each of those premises also deduces it. This is the definition through which Basis I is recovered below.
Popper.Basis3.NDeduce (B : Popper.Basis3) (P : List B.Obj) (b : B.Obj) : Prop
Show details
fun B P b => ∀ (c : B.Obj), (∀ a ∈ P, B.Deduce c a) → B.Deduce c b
Complexity: 57 (size of the value term)
Outer dependencies: Popper.Basis3
Lean core dependencies: List
Used by: Popper.Basis3.deduce_iff_ndeduce_singleton, Popper.Basis3.ndeduce_rg, Popper.Basis3.ndeduce_tg, Popper.Basis3.toBasis1, Propositional.Formula.and_isConjunction, Propositional.Formula.neg_isClassicalNegation, Propositional.Formula.or_isDisjunction, Propositional.Formula.provable_imp_iff_semanticDerive, Propositional.Formula.provable_imp_iff_syntacticDerive
Popper.Basis3.deduce_iff_ndeduce_singleton
Two-place deducibility is exactly the one-premise case of the defined many-premise relation. The forward direction is transitivity; the backward direction is reflexivity.
Popper.Basis3.deduce_iff_ndeduce_singleton (B : Popper.Basis3) (a b : B.Obj) : B.Deduce b a ↔ B.NDeduce [b] a
Show details
fun B a b => { mp := fun hba c hc => B.trans (hc 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))))) hba, mpr := fun h => h b fun x hx => Eq.ndrec (motive := fun b => B.NDeduce [b] a → B.Deduce b x) (fun h => B.refl x) (Eq.mp (congrArg (fun _a => _a) (propext List.mem_singleton)) hx) h }
Complexity: 675 (size of the value term)
Dependencies: Popper.Basis3, Popper.Basis3.NDeduce
Popper.Basis3.ndeduce_rg
Generalised reflexivity for the defined many-premise relation.
Popper.Basis3.ndeduce_rg (B : Popper.Basis3) (P : List B.Obj) (a : B.Obj) (h : a ∈ P) : B.NDeduce P a
Show details
fun B P a h x hc => hc a h
Complexity: 77 (size of the value term)
Dependencies: Popper.Basis3, Popper.Basis3.NDeduce
Lean core dependencies: List
Popper.Basis3.ndeduce_tg
Generalised transitivity for the defined many-premise relation.
Popper.Basis3.ndeduce_tg (B : Popper.Basis3) (P Q : List B.Obj) (c : B.Obj) (h1 : ∀ b ∈ Q, B.NDeduce P b) (h2 : B.NDeduce Q c) : B.NDeduce P c
Show details
fun B P Q c h1 h2 x hx => h2 x fun b hb => h1 b hb x hx
Complexity: 137 (size of the value term)
Dependencies: Popper.Basis3, Popper.Basis3.NDeduce
Lean core dependencies: List
Popper.Basis3.toBasis1
Basis I follows from Basis III. The many-premise deducibility defined from a Basis III’s two-place deducibility satisfies generalised reflexivity and transitivity, so it is itself a Basis I.
Popper.Basis3.toBasis1 (B : Popper.Basis3) : Popper.Basis1
Show details
fun B => { Obj := B.Obj, Deduce := B.NDeduce, rg := ⋯, tg := ⋯ }
Complexity: 19 (size of the value term)
Outer dependencies: Popper.Basis1, Popper.Basis3
Inner dependencies: Popper.Basis3.NDeduce, Popper.Basis3.ndeduce_rg, Popper.Basis3.ndeduce_tg
Popper.Basis3.Derive
Relative demonstrability for Basis III: the demonstrability turnstile of the Basis I that Basis III recovers.
Popper.Basis3.Derive (B : Popper.Basis3) (P Q : List B.Obj) : Prop
Show details
fun B P Q => B.toBasis1.Derive P Q
Complexity: 23 (size of the value term)
Outer dependencies: Popper.Basis3
Inner dependencies: Popper.Basis1.Derive, Popper.Basis3.toBasis1
Lean core dependencies: List
Used by: Popper.Basis3.cut
Popper.Basis3.cut
Cut for Basis III’s relative demonstrability, inherited from the Cut of the recovered Basis I.
Popper.Basis3.cut (B : Popper.Basis3) (P Q : List B.Obj) (e : B.Obj) (A : B.Derive P (Q ++ [e])) (B' : B.Derive (e :: P) Q) : B.Derive P Q
Show details
fun B P Q e A B' => Popper.Basis1.cut B.toBasis1 P Q e A B'
Complexity: 105 (size of the value term)
Dependencies: Popper.Basis3, Popper.Basis3.Derive
Proof dependencies: Popper.Basis1.cut, Popper.Basis3.toBasis1
Lean core dependencies: List
Used by: (none)
Popper.totalPreorderBasis3
A Popper.Basis3 exists: the total preorder on any type, where every object deduces every other.
Popper.totalPreorderBasis3 : Popper.Basis3
Show details
{ Obj := ℕ, Deduce := fun x x_1 => True, refl := ⋯, trans := ⋯ }
Complexity: 25 (size of the value term)
Outer dependencies: Popper.Basis3
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.