a B-valued quantifier is any function (A→B)→B, so when B is bool quantifiers are the functions that take predicates as input and return bool as output (same for prop). the standard max and min functions on arrays count as real-valued quantifiers for some index set A.
I thought I had seen ∀ as the max of the Prop-valued quantifiers, and exists as the min somewhere, which has a nice mindfeel since forall has this “big” feeling (if you determined for P:A→Prop that ∀P (of which ∀x:A,Px is just syntax sugar since the variable name x is irrelevant) by exhaustive checking, it would cost O(|A|) whereas ∃P would cost O(1) unless the derivation of the witness was dependent on size of domain somehow).
Incidentally however, in differentiable logic it seems forall is the “minimal expectation” and existential is the “maximal expectation”. Page 10 of the LDL paper, where a Emin(g(X)) is the limit as gamma goes to zero of ∫x∈Bγ(ming)p(x)g(x)dx, or the integral with respect to a γ-ball about the min of g rather than about the entire domain of g. os in this sense, the interpretation of a universally quantified prop is a minimal expectation, dual where existentially quantified prop is a maximal expectation.
I didn’t like the way this felt aesthetically, since as I said, forall feels “big” which mood-affiliates toward a max. But that’s notes from barely-remembered category theory I saw once. Anyway, I asked a language model and it said that forall is minimal because it imposes the strictest of “most conservative” requirement. so “max” in the sense of “exists is interpreted to maximal expectation” refers to maximal freedom.
Among monotonic, boolean quantifiers that don’t ignore their input, exists is maximal because it returns true as often as possible; forall is minimal because it returns true as rarely as possible.
a B-valued quantifier is any function (A→B)→B, so when B is bool quantifiers are the functions that take predicates as input and return bool as output (same for prop). the standard
maxandminfunctions on arrays count as real-valued quantifiers for some index set A.I thought I had seen ∀ as the max of the Prop-valued quantifiers, and exists as the min somewhere, which has a nice mindfeel since forall has this “big” feeling (if you determined for P:A→Prop that ∀P (of which ∀x:A,Px is just syntax sugar since the variable name x is irrelevant) by exhaustive checking, it would cost O(|A|) whereas ∃P would cost O(1) unless the derivation of the witness was dependent on size of domain somehow).
Incidentally however, in differentiable logic it seems forall is the “minimal expectation” and existential is the “maximal expectation”. Page 10 of the LDL paper, where a Emin(g(X)) is the limit as gamma goes to zero of ∫x∈Bγ(min g)p(x)g(x)dx, or the integral with respect to a γ-ball about the min of g rather than about the entire domain of g. os in this sense, the interpretation of a universally quantified prop is a minimal expectation, dual where existentially quantified prop is a maximal expectation.
I didn’t like the way this felt aesthetically, since as I said, forall feels “big” which mood-affiliates toward a max. But that’s notes from barely-remembered category theory I saw once. Anyway, I asked a language model and it said that forall is minimal because it imposes the strictest of “most conservative” requirement. so “max” in the sense of “exists is interpreted to maximal expectation” refers to maximal freedom.
I suppose this is fine.
Among monotonic, boolean quantifiers that don’t ignore their input, exists is maximal because it returns true as often as possible; forall is minimal because it returns true as rarely as possible.