Basis1
Difficulty: easy — 2 definitions, 0 abbreviations, 2 lemmas, 1 theorems, 0 examples.
Popper’s Basis I: the primitive many-premise deducibility relation, the demonstrability turnstile defined on top of it, and Cut for that turnstile.
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.4 (demonstrability, definitions \(D\vdash_2\) and \(D\vdash_3\)), section 4.5 (Cut, Theorems 4.7-4.9).
Popper.Basis1
Basis I. A conclusion is deducible from a finite list of premises (Popper’s \(a_1, \dots, a_n / b\)). Axiomatised by two closure conditions: every premise deduces itself (generalised reflexivity), and a chain of deductions composes (generalised transitivity).
Popper.Basis1 : Type 1
Show details
| Popper.Basis1.mk : (Obj : Type) → (Deduce : List Obj → Obj → Prop) → (∀ (P : List Obj), ∀ a ∈ P, Deduce P a) → (∀ (P B : List Obj) (c : Obj), (∀ b ∈ B, Deduce P b) → Deduce B c → Deduce P c) → Popper.Basis1
Outer dependencies: (none)
Popper.Basis1.mono
Premise monotonicity: enlarging, reordering, or contracting the premises never breaks a deduction. This follows from reflexivity and transitivity alone.
Popper.Basis1.mono (S : Popper.Basis1) {P P' : List S.Obj} {c : S.Obj} (h : ∀ a ∈ P, a ∈ P') (hc : S.Deduce P c) : S.Deduce P' c
Show details
fun S {P P'} {c} h hc => S.tg P' P c (fun b hb => S.rg P' b (h b hb)) hc
Complexity: 125 (size of the value term)
Dependencies: Popper.Basis1
Lean core dependencies: List
Popper.Basis1.Derive
Relative demonstrability (Popper’s turnstile \(P \vdash Q\), between a list of premises and a list of conclusions), defined from Basis I’s deducibility via \(D\vdash_3\): for every object and every finite context, if each conclusion together with that context deduces the object, then so do the premises together with the same context. Threading an arbitrary context through the premises is what makes Cut hold below; the simpler, context-free definition \(D\vdash_2\) does not validate Cut.
Popper.Basis1.Derive (S : Popper.Basis1) (P Q : List S.Obj) : Prop
Show details
fun S P Q => ∀ (c : S.Obj) (D : List S.Obj), (∀ b ∈ Q, S.Deduce (b :: D) c) → S.Deduce (P ++ D) c
Complexity: 109 (size of the value term)
Outer dependencies: Popper.Basis1
Lean core dependencies: List
Used by: Popper.Basis1.IsClassicalNegation, Popper.Basis1.IsConjunction, Popper.Basis1.IsDisjunction, Popper.Basis1.cut, Popper.Basis1.derive_singleton, Popper.Basis3.Derive, 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.Basis1.cut
Cut, from Basis I alone. If the premises derive the conclusions together with some extra object, and that object together with the premises derives the conclusions, then the premises alone already derive the conclusions: the extra object need not survive on either side.
Popper.Basis1.cut (S : Popper.Basis1) (P Q : List S.Obj) (e : S.Obj) (A : S.Derive P (Q ++ [e])) (B : S.Derive (e :: P) Q) : S.Derive P Q
Show details
fun 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 => 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.Derive P (Q ++ [e]) → S.Derive (e :: P) Q → S.Deduce (e :: (P ++ D)) c → b ∈ Q ++ [e] → b ∈ [e] → S.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; 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: 3449 (size of the value term)
Dependencies: Popper.Basis1, Popper.Basis1.Derive
Proof dependencies: Popper.Basis1.mono
Lean core dependencies: Eq, List, List.mem_append, List.mem_cons, List.mem_singleton, Or
Used by: Popper.Basis3.cut
Popper.Basis1.derive_singleton
Demonstrability between a single premise and a single conclusion is just deducibility between them: threading an extra context through a single pair adds nothing.
Popper.Basis1.derive_singleton (S : Popper.Basis1) {a b : S.Obj} : S.Derive [a] [b] ↔ S.Deduce [a] b
Show details
fun S {a b} => { mp := fun h => have this := h b [] fun x hx => List.mem_singleton.mp hx ▸ Eq.symm (List.mem_singleton.mp hx) ▸ S.rg [b] b (List.mem_singleton_self b); Eq.mp (congrFun' (congrArg S.Deduce (List.append_nil [a])) b) this, mpr := fun h c D hD => S.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.Deduce [a] b → (∀ b_1 ∈ [b], S.Deduce (b_1 :: D) c) → x ∈ b :: D → S.Deduce (a :: D) x) (fun h hD hx => 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 => S.rg (a :: D) x (List.mem_cons.mpr (Or.inr hx))) (hD b (List.mem_singleton_self b)) }
Complexity: 1688 (size of the value term)
Dependencies: Popper.Basis1, Popper.Basis1.Derive
Proof dependencies: Popper.Basis1.mono
Lean core dependencies: Eq, Eq.mp, Eq.symm, Iff, List, List.append_nil, List.mem_cons, List.mem_singleton, List.mem_singleton_self, Or, congrArg, congrFun'
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.