Cf: Functional Logic • Inquiry and Analogy • 21
https://inquiryintoinquiry.com/2022/06/09/functional-logic-inquiry-and-analogy-21/
Inquiry and Analogy • Generalized Umpire Operators
https://oeis.org/wiki/Functional_Logic_%E2%80%A2_Inquiry_and_Analogy#Gen_Ump_Ops
All,
To get a better handle on the space of higher order propositions
and continue developing our functional approach to quantification
theory, we’ll need a number of specialized tools. To begin, we
define a higher order operator Υ, called the “umpire operator”,
which takes 1, 2, or 3 propositions as arguments and returns a
single truth value as the result. Operators with optional numbers
of arguments are called “multigrade operators”, typically defined
as unions over function types. Expressing Υ in that form gives
the following formula.
• Υ : ⋃_{ℓ = 1, 2, 3} ((B^k → B)^ℓ → B).
In contexts of application, that is, where a multigrade operator
is actually being applied to arguments, the number of arguments in
the argument list tells which of the optional types is “operative”.
In the case of Υ, the first and last arguments appear as indices,
the one in the middle serving as the main argument while the other
two arguments serve to modify the sense of the operation in question.
Thus, we have the following forms.
• Υₚ^r q = Υ(p, q, r)
• Υₚ^r : (B^k → B) → B
The operation Υₚ^r q = Υ(p, q, r) evaluates the proposition q
on each model of the proposition p and combines the results
according to the method indicated by the connective parameter r.
In principle, the index r may specify any logical connective on
as many as 2^k arguments but in practice we usually have a much
simpler form of combination in mind, typically either products
or sums. By convention, each of the accessory indices p, r is
assigned a default value understood to be in force when the
corresponding argument place is left blank, specifically, the
constant proposition 1 : B^k → B for the lower index p and the
continued conjunction or continued product operation ∏ for the
upper index r. Taking the upper default value gives license to
the following readings.
• Υₚ(q) = Υ(p, q) = Υ(p, q, ∏).
• Υₚ = Υ(p, _, ∏) : (B^k → B) → B.
This means Υₚ(q) = 1 if and only if q holds for all models of p.
In propositional terms, this is tantamount to the assertion that
p ⇒ q, or that ¬(p ¬(q)) = 1.
Throwing in the lower default value permits the following abbreviations.
• Υq = Υ(q) = Υ₁(q) = Υ(1, q, ∏).
• Υ = Υ(1, _, ∏) : (B^k → B) → B.
This means Υq = 1 if and only if q holds for the whole universe of discourse in
question, that is, if and only q is the constantly true proposition 1 : B^k → B.
The ambiguities of this usage are not a problem so long as we distinguish the
context of definition from the context of application and restrict all shorthand
notations to the latter.
Resources
=========
Multigrade Operators (
https://oeis.org/wiki/Multigrade_operator )
Parametric Operators (
https://oeis.org/wiki/Parametric_operator )
Regards,
Jon