Difficulty: easy — 3 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.
Popper’s relational characterizations of conjunction, disjunction, and classical negation: not connectives built into the syntax of a basis, but properties an object can have, stated purely in terms of relative demonstrability. A basis need not have anything satisfying these properties, and if something does, that is what makes it a conjunction, a disjunction, or a classical negation.
Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: section 5.5 (conjunction and disjunction, rules (C∧) and (C∨)), section 6.1 (classical negation, rules (C¬k1) and (C¬k2)).
\(m\) is a conjunction of \(a\) and \(b\): for every object \(d\), \(m\) alone derives \(d\) exactly when \(a\) and \(b\) together derive \(d\).
Popper.Basis1.IsConjunction (S : Popper.Basis1) (a b m : S.Obj) : Prop
Show details
fun S a b m => ∀ (d : S.Obj), S.Derive [m] [d] ↔ S.Derive [a, b] [d]
Complexity: 91 (size of the value term)
Lean core dependencies: Iff
\(j\) is a disjunction of \(a\) and \(b\): for every object \(d\), \(d\) alone derives \(j\) exactly when \(d\) derives \(a\) or \(b\).
Popper.Basis1.IsDisjunction (S : Popper.Basis1) (a b j : S.Obj) : Prop
Show details
fun S a b j => ∀ (d : S.Obj), S.Derive [d] [j] ↔ S.Derive [d] [a, b]
Complexity: 91 (size of the value term)
Lean core dependencies: Iff
\(n\) is a classical negation of \(a\): for every context \(d\) and every object \(c\), \(d\) together with \(n\) derives \(c\) exactly when \(d\) alone derives \(a\) or \(c\).
Popper.Basis1.IsClassicalNegation (S : Popper.Basis1) (a n : S.Obj) : Prop
Show details
fun S a n => ∀ (d c : S.Obj), S.Derive [d, n] [c] ↔ S.Derive [d] [a, c]
Complexity: 99 (size of the value term)
Lean core dependencies: Iff
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.
definitiondeclared elsewheredependencyproof dependency
legend