Difficulty: moderate — 2 definitions, 0 abbreviations, 0 lemmas, 1 theorems, 0 examples.
Popper’s Basis III: deducibility taken as a primitive relation between two single statements. This is the smallest starting point Popper arrived at, and the one he settled on last (1948a).
A basis fixes a binary relation with two closure conditions it must satisfy, before any particular logic is chosen. The conditions are reflexivity and transitivity.
Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: end of section 4.6 (Basis III). Popper (1948a) introduces Basis III; Popper (1949a) adopts two-place deducibility as the sole primitive notion.
Basis III. A primitive relation between two single statements over a fixed carrier type, characterised as a preorder. Popper writes \(a / b\) and reads it “\(b\) is deducible from \(a\)”, so the premise comes first and the conclusion second. Every many-premise notion is defined from this one primitive relation.
basis
structure Logic.Popper.Basis3 (Obj : Type) : Type
The relation \(a / b\).
Follows : Obj → Obj → Prop
Reflexivity: every statement follows from itself.
refl : ∀ (a : Obj), Logic.Popper.Basis3.Follows a a
Transitivity: what follows from what follows from \(a\), also directly follows from \(a\).
trans : ∀ {a b c : Obj},
Logic.Popper.Basis3.Follows a b →
Logic.Popper.Basis3.Follows b c → Logic.Popper.Basis3.Follows a c
Show details
Outer dependencies: (none)
Basis III generates a Basis I. A statement is deducible from a list of premises exactly when everything the premises all follow from, it follows from too. That relation satisfies generalised reflexivity and generalised transitivity, so nothing beyond a Basis III is needed to obtain a Basis I, and with it everything this chapter proves.
def Logic.Popper.Basis3.toBasis1 {Obj : Type} (B : Logic.Popper.Basis3 Obj) : Logic.Popper.Basis1 Obj
Show details
| B.toBasis1 =
{
Deduce := fun P b =>
∀ (c : Obj), (∀ a ∈ P, Logic.Popper.Basis3.Follows c a) → Logic.Popper.Basis3.Follows c b,
rg := ⋯, tg := ⋯ }
Complexity: 119 (size of the value term)
Lean core dependencies: List
Used by: Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.exists_fresh_ne, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal, Logic.FirstOrderLogic.mutual_of_realize_iff, Logic.FirstOrderLogic.realize_iff_of_mutual, Logic.FirstOrderLogic.realize_nonDep_update, Logic.FirstOrderLogic.realize_update_of_nonDep, Logic.Popper.Basis3.follows_toBasis1, 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
Two-place deducibility is exactly the one-premise case of the relation it generates.
theorem Logic.Popper.Basis3.follows_toBasis1 {Obj : Type} (B : Logic.Popper.Basis3 Obj) (a b : Obj) :
B.toBasis1.Follows a b ↔ Logic.Popper.Basis3.Follows a b
Show details
fun {Obj} B a b =>
{
mp := fun h =>
h a fun x hx =>
Eq.mp
(Eq.trans List.mem_cons._simp_1
(Eq.trans (congrArg (Or (x = a)) List.not_mem_nil._simp_1) (or_false (x = a))))
hx ▸
Eq.symm
(Eq.mp
(Eq.trans List.mem_cons._simp_1
(Eq.trans (congrArg (Or (x = a)) List.not_mem_nil._simp_1) (or_false (x = a))))
hx) ▸
Logic.Popper.Basis3.refl a,
mpr := fun hab c hc =>
Logic.Popper.Basis3.trans
(hc 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)))))
hab }
Complexity: 869 (size of the value term)
Lean core dependencies: Eq, Eq.mp, Eq.symm, Eq.trans, False, Iff, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false
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.
definitiontheoremdeclared elsewheredependencyproof dependency
legend