Quantification
Difficulty: moderate — 4 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 4 examples.
Popper’s theory of quantification (editors’ introduction §9.3): the universal and existential quantifiers, defined inferentially from a basis’s own deducibility together with substitution, rather than taken as new primitive connectives requiring their own separate treatment.
Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: section 9.3, rules (C7.1) and (C7.2).
Logic.Popper.Basis1.IsUniversal
\(m\) is the universal quantification of \(b\) over the name \(x\) (Popper’s \(Axb\)): for a suitably fresh name \(y\) that \(b\) does not depend on, and for every \(c\) that also does not depend on \(y\), \(c\) derives \(m\) exactly when \(c\) derives \(b\) with \(y\) substituted for \(x\).
def Logic.Popper.Basis1.IsUniversal {Obj name : Type} (B : Logic.Popper.Basis1 Obj) (SUB : Obj → name → name → Obj) (x : name) (b m : Obj) : Prop
Show details
| B.IsUniversal SUB x b m = ∃ y, Logic.Popper.NonDep B.Mutual SUB b y ∧ ∀ (c : Obj), Logic.Popper.NonDep B.Mutual SUB c y → (B.Follows c m ↔ B.Follows c (SUB b x y))
Complexity: 95 (size of the value term)
Outer dependencies: Logic.Popper.Basis1
Inner dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.Mutual, Logic.Popper.NonDep
Logic.Popper.Basis1.IsExistential
\(m\) is the existential quantification of \(b\) over the name \(x\) (Popper’s \(Exb\)): dual to Popper.Basis1.IsUniversal, with the direction of deducibility reversed.
def Logic.Popper.Basis1.IsExistential {Obj name : Type} (B : Logic.Popper.Basis1 Obj) (SUB : Obj → name → name → Obj) (x : name) (b m : Obj) : Prop
Show details
| B.IsExistential SUB x b m = ∃ y, Logic.Popper.NonDep B.Mutual SUB b y ∧ ∀ (c : Obj), Logic.Popper.NonDep B.Mutual SUB c y → (B.Follows m c ↔ B.Follows (SUB b x y) c)
Complexity: 95 (size of the value term)
Outer dependencies: Logic.Popper.Basis1
Inner dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.Mutual, Logic.Popper.NonDep
Logic.Popper.Basis1.HasUniversal
A basis \(B\), together with a substitution operation \(S\) over it, equipped with a distinguished universal quantifier, witnessed by actually satisfying Popper’s characterizing property for it. Takes \(B\) and \(S\) as explicit parameters, matching Popper.Basis1.HasConjunction and its siblings, so that a logic wanting both quantifiers and connectives never risks each independently picking its own underlying basis or substitution operation.
structure Logic.Popper.Basis1.HasUniversal (Obj name : Type) (B : Logic.Popper.Basis1 Obj) (S : Logic.Popper.HasSubstitution Obj name B.Mutual) : Type
all : name → Obj → Obj
all_isUniversal : ∀ (x : name) (b : Obj), B.IsUniversal (Logic.Popper.HasSubstitution.SUB B.Mutual) x b (Logic.Popper.Basis1.HasUniversal.all S x b)
Show details
Outer dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Mutual, Logic.Popper.HasSubstitution
Inner dependencies: Logic.Popper.Basis1.IsUniversal
Logic.Popper.Basis1.HasExistential
A basis \(B\), together with a substitution operation \(S\) over it, equipped with a distinguished existential quantifier, witnessed by actually satisfying Popper’s characterizing property for it.
structure Logic.Popper.Basis1.HasExistential (Obj name : Type) (B : Logic.Popper.Basis1 Obj) (S : Logic.Popper.HasSubstitution Obj name B.Mutual) : Type
ex : name → Obj → Obj
ex_isExistential : ∀ (x : name) (b : Obj), B.IsExistential (Logic.Popper.HasSubstitution.SUB B.Mutual) x b (Logic.Popper.Basis1.HasExistential.ex S x b)
Show details
Outer dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Mutual, Logic.Popper.HasSubstitution
Inner dependencies: Logic.Popper.Basis1.IsExistential
Logic.Popper.Basis1.totalBasis1
The total basis on the naturals, where everything is deducible from anything.
instance Logic.Popper.Basis1.totalBasis1 : Logic.Popper.Basis1 ℕ
Show details
| Logic.Popper.Basis1.totalBasis1 = { Deduce := fun x x_1 => True, rg := ⋯, tg := ⋯ }
Complexity: 69 (size of the value term)
Outer dependencies: Logic.Popper.Basis1
Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1
A trivial witness that Popper.Basis1.HasUniversal and Popper.Basis1.HasExistential are satisfiable: over the total preorder on Nat (where every object deduces every other, so every side condition and every biconditional holds outright), a substitution that ignores its names works, and the quantifier can be taken to just discard its bound name.
instance Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1 : Logic.Popper.HasSubstitution ℕ Unit Logic.Popper.Basis1.totalBasis1.Mutual
Show details
| Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1 = { DIST := fun x x_1 => True, SUB := fun a x x_1 => a, fresh := Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_1, sub_congr := @Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_2, sub_self := Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_3, sub_vacuous := Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_4, sub_comp := Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_5, sub_comm_same := Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_5, sub_comm := Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1._proof_6 }
Complexity: 39 (size of the value term)
Outer dependencies: Logic.Popper.Basis1.Mutual, Logic.Popper.Basis1.totalBasis1, Logic.Popper.HasSubstitution
Inner dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.NonDep
Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual
instance Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual : Logic.Popper.Basis1.HasUniversal ℕ Unit Logic.Popper.Basis1.totalBasis1 inferInstance
Show details
| Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual = { all := fun x b => b, all_isUniversal := Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual._proof_1 }
Complexity: 31 (size of the value term)
Outer dependencies: Logic.Popper.Basis1.HasUniversal, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1, Logic.Popper.Basis1.totalBasis1, Logic.Popper.HasSubstitution
Inner dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.NonDep
Used by: (none)
Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual
instance Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual : Logic.Popper.Basis1.HasExistential ℕ Unit Logic.Popper.Basis1.totalBasis1 inferInstance
Show details
| Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual = { ex := fun x b => b, ex_isExistential := Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual._proof_1 }
Complexity: 31 (size of the value term)
Outer dependencies: Logic.Popper.Basis1.HasExistential, Logic.Popper.Basis1.Mutual, Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1, Logic.Popper.Basis1.totalBasis1, Logic.Popper.HasSubstitution
Inner dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.NonDep
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.