Bounded first-order quantifiers as set operations: \(\exists\) is non-emptiness of a comprehension, \(\forall\) its \(\neg\exists\neg\) dual. More...
#include <type_traits>#include <utility>import dedekind.sets:computability;import dedekind.category;
Namespaces | |
| namespace | dedekind::sets |
Concepts | |
| concept | dedekind::sets::IsWhereClause |
| Quantifiers over a finite carrier, decided by type through the finite quotient rather than by enumeration. | |
Functions | |
| template<typename L> | |
| constexpr L::Ω | dedekind::sets::in_species (auto v) |
A verdict in the species L: an == that answers in L::Ω passes through, one that answers bool (a sized or structural equality) is lifted to ⊥ / ⊤. | |
| template<dedekind::category::IsLSet S, IsWhereClause< S > P> | |
| constexpr S::logic_species::Ω | dedekind::sets::exists (const S &s, P p) |
|
template<dedekind::category::IsLSet S, IsWhereClause< S > P> requires HasDecidableMembership<S> || dedekind::category::IsBoundaryObject<S> | |
| constexpr S::logic_species::Ω | dedekind::sets::forall (const S &s, P p) |
Bounded \(\forall\) over a decidable S (its χ in 𝔹: the Δ grade, HasDecidableMembership) or a boundary in any species (χ constant). There the identity \(\forall x \in S.\,P \iff (S|P = S)\) holds in L, because for two-valued \(\chi_S\) the internal equality \((\chi_S \wedge \chi_P \Leftrightarrow \chi_S)\) coincides with the implication \(\chi_S \Rightarrow \chi_P\). In a Heyting algebra that is a theorem for every \(\chi_S\); Ω here is a De Morgan chain (#901) whose material implication is not a residuum, so over an L-valued S the bounded \(\forall = \bigwedge (\chi_S \Rightarrow \chi_P)\) needs the chain's residuated implication, which is #980's remainder. | |
Detailed Description
Bounded first-order quantifiers as set operations: \(\exists\) is non-emptiness of a comprehension, \(\forall\) its \(\neg\exists\neg\) dual.
@partition :quantifier
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
quantifier__The_Definition
A quantifier is a set operation (the Bourbaki / structural reading). We take that literally as the definition, not merely as a characterisation:
\[ \exists x \in S.\,P(x) \;:\equiv\; \{x\in S \mid P(x)\} \neq \varnothing, \qquad \forall x \in S.\,P(x) \;:\equiv\; \neg\,\exists x \in S.\,\neg P(x). \]
In code the comprehension is the meet S & P (#826): exists is !(Ø{} == (S | P)) and forall is S == (S | P). There is no separate fold; the reduction lives entirely in the == the comprehension's fragment supplies, and the Rice boundary is therefore a type check (an operand with no suitable == overload is a compile error) rather than hand-waved prose.
quantifier__L_Valued
The set-level forms take any L-set (Goguen) and answer in its L: with == the internal logic's equality \(\bigwedge_x (\chi \Leftrightarrow
\chi')\), \(\exists = \neg(\varnothing = S|P) = \bigvee (\chi_S \wedge
\chi_P)\) by De Morgan, and \(\forall = ((S|P) = S) = \bigwedge \chi_P\) on a decidable S (HasDecidableMembership, or a boundary in any species). So Unknown is a verdict, not a failure, and there is still no separate fold: whatever == a fragment supplies (on a chain, the run lists of dedekind.order) is the quantifier. Boolean sets answer bool as before.
@build_order after :cardinality @dependency :category
