Cf: Functional Logic • Inquiry and Analogy • 14
https://inquiryintoinquiry.com/2022/05/17/functional-logic-inquiry-and-anal…
Umpire Operators (Part 1 of 2)
https://oeis.org/wiki/Functional_Logic_%E2%80%A2_Inquiry_and_Analogy#Umpire…
All,
[Note. Please follow the first link above for better math formatting.]
The 2¹⁶ measures of type (B × B → B) → B present a formidable array of
propositions about propositions about 2-dimensional universes of discourse.
The early entries in their standard ordering define universes too amorphous
to detain us for long on a first pass but as we turn toward the high end of
the ordering we begin to recognize familiar structures worth examining from
new angles.
Instrumental to our study we define a couple of higher order operators,
• Υ : (B × B → B)² → B
and
• Υ₁ : (B × B → B) → B,
referred to as the relative and absolute “umpire operators”,
respectively. If either operator is defined in terms of more
primitive notions then the remaining operator can be defined
in terms of the one first established.
Let X = ⟨u, v⟩ be a 2-dimensional boolean space, X ≅ B × B,
generated by 2 boolean variables or logical features u and v.
Given an ordered pair of propositions e, f : ⟨u, v⟩ → B as arguments,
the relative umpire operator reports the value 1 if the first implies
the second, otherwise it reports the value 0.
• Υ(e, f) = 1 if and only if e ⇒ f
Expressing it another way:
• Υ(e, f) = 1 ⇔ ¬( e ¬( f )) = 1
In writing this, however, it is important to observe that the 1
appearing on the left side and the 1 appearing on the right side
of the logical equivalence have different meanings. Filling in
the details, we have the following.
• Υ(e, f) = 1 ∈ B ⇔ ¬( e ¬( f )) = 1 : ⟨u, v⟩ → B
Writing types as subscripts and using the fact that X = ⟨u, v⟩,
it is possible to express this a little more succinctly as follows.
• Υ(e, f) = 1_B ⇔ ¬( e ¬( f )) = 1_{X → B}
Finally, it is often convenient to write the first argument
as a subscript. Thus we have the following equation.
• (Υ_e)(f) = Υ(e, f).
Regards,
Jon