Aggregation of Truth3 Lists by Projection Type

@cite{barwise-cooper-1981}

Universal vs existential aggregation as the ⊓/⊔ projections of the ∃ ⊣ Δ ⊣ ∀ adjunction, parameterized by ProjectionType (declared in Truth3.lean).

§ 1. Truth3 Aggregation

• aggregate (d : ProjectionType) : List Truth3 → Truth3 — fold by projection type. Conjunctive: ⊓-fold from ⊤. Disjunctive: ⊔-fold from ⊥.

§ 2. Prop-valued Quantifier Projection

The Prop-valued counterparts of existsAny/forallAll are just ∃/∀ from Lean core. De Morgan duality uses not_forall/not_exists from Mathlib.

def Core.Duality.aggregate (d : ProjectionType) (l : List Truth3) : Truth3

Aggregate a list according to projection type. Conjunctive (∀-like): ⊓-fold from ⊤. Disjunctive (∃-like): ⊔-fold from ⊥.

Equations

• Core.Duality.aggregate Core.Duality.ProjectionType.disjunctive l = List.foldl (fun (x1 x2 : Core.Duality.Truth3) => max x1 x2) ⊥ l
• Core.Duality.aggregate Core.Duality.ProjectionType.conjunctive l = List.foldl (fun (x1 x2 : Core.Duality.Truth3) => min x1 x2) ⊤ l

def Core.Duality.existsAny (l : List Truth3) : Truth3

Existential (disjunctive) aggregation: true if ANY true.

Equations

• Core.Duality.existsAny l = Core.Duality.aggregate Core.Duality.ProjectionType.disjunctive l

def Core.Duality.forallAll (l : List Truth3) : Truth3

Universal (conjunctive) aggregation: true only if ALL true.

Equations

• Core.Duality.forallAll l = Core.Duality.aggregate Core.Duality.ProjectionType.conjunctive l

theorem Core.Duality.foldl_sup_of_true (l : List Truth3) : List.foldl (fun (x1 x2 : Truth3) => max x1 x2) Truth3.true l = Truth3.true

theorem Core.Duality.foldl_inf_of_false (l : List Truth3) : List.foldl (fun (x1 x2 : Truth3) => min x1 x2) Truth3.false l = Truth3.false

theorem Core.Duality.foldl_sup_mem_true (l : List Truth3) (acc : Truth3) (h : Truth3.true ∈ l) : List.foldl (fun (x1 x2 : Truth3) => max x1 x2) acc l = Truth3.true

theorem Core.Duality.foldl_inf_mem_false (l : List Truth3) (acc : Truth3) (h : Truth3.false ∈ l) : List.foldl (fun (x1 x2 : Truth3) => min x1 x2) acc l = Truth3.false

theorem Core.Duality.existential_robust (l : List Truth3) (h : (l.any fun (x : Truth3) => x == Truth3.true) = true) : existsAny l = Truth3.true

theorem Core.Duality.universal_fragile (l : List Truth3) (h : (l.any fun (x : Truth3) => x == Truth3.false) = true) : forallAll l = Truth3.false

def Core.Duality.const {α : Type u_1} (t : Truth3) : α → Truth3

Equations

• Core.Duality.const t x✝ = t

def Core.Duality.exists' {α : Type u_1} (P : α → Truth3) (l : List α) : Truth3

Equations

• Core.Duality.exists' P l = Core.Duality.existsAny (List.map P l)

def Core.Duality.forall' {α : Type u_1} (P : α → Truth3) (l : List α) : Truth3

Equations

• Core.Duality.forall' P l = Core.Duality.forallAll (List.map P l)

The aggregation operators defined in § 1 are List.foldl over the Truth3 lattice. Their behavior is determined by two algebraic facts:

1. **Idempotency** (`sup_idem`, `inf_idem`): every element of a
   lattice is a fixed point of `⊔` and `⊓`. With initial accumulator
   `⊥` (resp. `⊤`), folding `⊔` (resp. `⊓`) over `List.replicate n
   .indet` gets absorbed by `.indet` after the first step (identity
   element transition).

2. **Lattice homomorphism** (`Truth3.ofBoolHom`): `ofBool` embeds
   `Bool` into the `{⊥, ⊤}` sublattice of `Truth3`, preserving both
   `⊔` and `⊓`. Folding lattice operations over `bs.map ofBool`
   reduces to folding the corresponding Boolean operations
   (`||`/`&&`) over `bs` — which is always definite, so the
   aggregation result avoids `.indet`.

These two facts are the algebraic basis for the architectural
distinction in trivalent semantics for quantified counterfactuals
(@cite{ramotowska-marty-romoli-santorio-2025}) and deontic modality
(@cite{agha-jeretic-2022} §4.2): inputs containing `.indet`
propagate it through aggregation regardless of duality type, while
inputs lifted from `Bool` always commit to a definite truth value. 

theorem Core.Duality.aggregate_replicate_indet (d : ProjectionType) (n : ℕ) (hn : n > 0) : aggregate d (List.replicate n Truth3.indet) = Truth3.indet

Aggregation over List.replicate n .indet collapses to .indet regardless of duality type. The duality type is invisible: this is the algebraic reason "local-scope" trivalent semantics erases quantifier strength.

theorem Core.Duality.aggregate_existential_map_ofBool (bs : List Bool) : aggregate ProjectionType.disjunctive (List.map Truth3.ofBool bs) = Truth3.ofBool (bs.any id)

Existential aggregation through Truth3.ofBool reduces to Boolean disjunction. Witness of the lattice-homomorphism property of Truth3.ofBoolHom propagating through fold.

theorem Core.Duality.aggregate_universal_map_ofBool (bs : List Bool) : aggregate ProjectionType.conjunctive (List.map Truth3.ofBool bs) = Truth3.ofBool (bs.all id)

Universal aggregation through Truth3.ofBool reduces to Boolean conjunction.

theorem Core.Duality.aggregate_map_ofBool_ne_indet (d : ProjectionType) (bs : List Bool) : aggregate d (List.map Truth3.ofBool bs) ≠ Truth3.indet

Aggregation through Truth3.ofBool never produces .indet — Boolean inputs leave the gap-free sublattice {⊥, ⊤} invariant. The algebraic basis for "global-scope" trivalent semantics where the quantifier sees only Boolean values.

theorem Core.Duality.aggregate_map_ofBool_mixed (bs : List Bool) (h_some_true : bs.any id = true) (h_some_false : (bs.any fun (x : Bool) => !x) = true) : aggregate ProjectionType.disjunctive (List.map Truth3.ofBool bs) = Truth3.true ∧ aggregate ProjectionType.conjunctive (List.map Truth3.ofBool bs) = Truth3.false

Mixed Boolean inputs (some true, some false) split the duality types: existential aggregation gives .true, universal gives .false. This IS the strength effect — algebraic reason selectional-architecture trivalent semantics predicts the quantifier-strength contrast on mixed scenarios.

The dist operator is finite-domain Boolean supervaluation: given a Finset s and a Boolean predicate P, classify (s, P) as super-true (P holds at every element), super-false (P fails at every element of nonempty s), or indeterminate (mixed). This is the construction introduced by @cite{van-fraassen-1966} (Definition 10, p. 487) for free logic with non-denoting names and named "super-truth" by @cite{fine-1975} (§3, p. 273) when applied to vagueness via specification spaces.

In linguistic semantics the same operation is @cite{schwarzschild-1996}'s
**DIST** operator for distributive plural predication (the source of
the name `dist`); @cite{kriz-2016} and @cite{kriz-spector-2021}
formalize the modern trivalent-homogeneity treatment.

Reachable cases on a Finset `s : Finset α` and predicate `P : α → Prop`
with `[DecidablePred P]`:
| `∀ a ∈ s, P a` | `∃ a ∈ s, P a` | meaning              | `dist s P` |
|----------------|----------------|----------------------|------------|
| `true`         | `true`         | nonempty, all P      | `.true`    |
| `true`         | `false`        | empty (vacuous)      | `.true`    |
| `false`        | `true`         | mixed                | `.indet`   |
| `false`        | `false`        | nonempty, no P       | `.false`   |

def Core.Duality.dist {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] : Truth3

Trivalent classifier (Fine super-truth, finite-Boolean specialization). dist s P is .true if P holds at every element of s (vacuously on ∅), .false if P fails at every element of nonempty s, .indet (mixed) otherwise. The supervaluation's universal/existential decision pair (∀, ∃) is the kernel; the if-chain classifies it into Truth3.

Equations

• Core.Duality.dist s P = if ∀ a ∈ s, P a then Core.Duality.Truth3.true else if ∃ a ∈ s, P a then Core.Duality.Truth3.indet else Core.Duality.Truth3.false

def Core.Duality.distList {α : Type u_1} (l : List α) (P : α → Prop) [DecidablePred P] : Truth3

List variant of dist — direct definition over ∀/∃ on a List, no [DecidableEq α] required. Same trichotomy: .true on (vacuously or genuinely) all-P, .false on nonempty-but-no-P, .indet mixed. Agrees with dist l.toFinset P when [DecidableEq α] is available.

Equations

• Core.Duality.distList l P = if ∀ a ∈ l, P a then Core.Duality.Truth3.true else if ∃ a ∈ l, P a then Core.Duality.Truth3.indet else Core.Duality.Truth3.false

@[simp]

theorem Core.Duality.dist_empty {α : Type u_1} (P : α → Prop) [DecidablePred P] : dist ∅ P = Truth3.true

dist is .true on the empty Finset (vacuous super-truth).

@[simp]

theorem Core.Duality.dist_singleton {α : Type u_1} [DecidableEq α] (a : α) (P : α → Prop) [DecidablePred P] : dist {a} P = if P a then Truth3.true else Truth3.false

dist on a singleton: .true if P a holds, .false otherwise.

@[simp]

theorem Core.Duality.dist_const_true {α : Type u_1} (s : Finset α) : (dist s fun (x : α) => True) = Truth3.true

dist is .true on the constantly-true predicate.

@[simp]

theorem Core.Duality.distList_nil {α : Type u_1} (P : α → Prop) [DecidablePred P] : distList [] P = Truth3.true

distList is .true on the empty list (vacuous super-truth).

@[simp]

theorem Core.Duality.distList_singleton {α : Type u_1} (a : α) (P : α → Prop) [DecidablePred P] : distList [a] P = if P a then Truth3.true else Truth3.false

distList on a singleton: .true if P a holds, .false otherwise.

@[simp]

theorem Core.Duality.distList_const_true {α : Type u_1} (l : List α) : (distList l fun (x : α) => True) = Truth3.true

distList is .true on the constantly-true predicate.

The Truth3 aggregation above (§ 1) is the decidable/three-valued version of quantifier projection. The classical Prop-valued counterparts are just ∃ and ∀ from Lean core — the left and right adjoints to the diagonal in the adjunction ∃ ⊣ Δ ⊣ ∀.

Many parameterized semantic theories (comparison classes, precisifications,
accessible worlds, variable assignments) project out a hidden index
via one of these two operations:

| Theory                 | Index I              | ∃-projection       | ∀-projection    | Mathlib hook                           |
|------------------------|----------------------|--------------------|-----------------|----------------------------------------|
| @cite{klein-1980}      | comparison class C   | comparative (more) | at-least-as     | `measureDelineation_mono_in_class`     |
| @cite{fine-1975}       | precisification      | sub-truth          | super-truth     | `Preorder SpecSpace`, stability        |
| @cite{caie-2023}       | comp. context        | disjunctive update | —               | `disjunctiveUpdate_mono_interp`        |
| @cite{kratzer-1981}    | accessible world     | ◇ (possibility)    | □ (necessity)   | `GaloisConnection` (Proposition.lean)  |
| @cite{kamp-1975}       | completion           | strict comparative | at-least-as     | `Antitone` in S (via `kampPreorder`)   |

The projections themselves are just `∃`/`∀`. De Morgan duality uses
`not_forall` / `not_exists` from Lean core. The deeper Mathlib
connections are on the **parameter spaces**: `Monotone`/`Antitone`
for how the projections vary as the parameter space changes,
`IsLeast`/`IsGreatest` for monotone collapse, and `GaloisConnection`
for the extension/intension adjunction.

See `ParameterizedUpdate.lean` for the shared framework (monotone
collapse via `IsLeast`/`IsGreatest` + `Antitone`, borderline region
characterization, sequential update with pruning).