[Inquiry] Re: Functional Logic

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

FL.  Note 3

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

2.1.3.  Umpire Operators

In order to get a handle on the space of higher order propositions and
eventually to carry out a functional approach to quantification theory,
it serves to construct some specialized tools.  Specifically, I define
a higher order operator !Y!, called the "umpire operator", which takes
up to three propositions as arguments and returns a single truth value
as the result.  Formally, this so-called "multi-grade" property of !Y!
can be expressed as a union of function types, in the following manner:

   !Y! : |_|^(m = 1, 2, 3) ((B^k -> B)^m -> B).

In contexts of application the intended sense can be discerned by
the number of arguments that actually appear in the argument list.
Often, the first and last arguments appear as indices, the one in
the middle being treated as the main argument while the other two
arguments serve to modulate the sense of the operator in question.

Accordingly, the employment of umpires may be
contingent on the following application forms:

   !Y!_p^r <q>  =  !Y!<p, q, r>

   !Y!_p^r : (B^k -> B) -> B

The intention of this operator is that we evaluate the proposition q
on each model of the proposition p and combine the results according
to the method indicated by the connective parameter r.  In principle,
the index r might specify any connective on as many as 2^k arguments,
but usually we have in mind a much simpler form of combination, most
often either collective products or collective sums.  By convention,
each of the accessory indices p, r is assigned a default value that
is understood to apply when the corresponding place is left blank,
specifically, the constant proposition 1 : B^k -> B for the lower
index p, and the continued conjunction or continued product ]^[
for the upper index r.  Taking the upper default value gives
license to the following readings:

   1.  !Y!_p <q>  =  !Y!<p, q>  =  !Y!<p, q, product>

   2.  !Y!_p      =  !Y!<p, _, product> : (B^k -> B) -> B

This means that !Y!_p <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 licences the
following abbreviations:

   3.  !Y!q  =  !Y!<q>  =  !Y!_1 q  =  !Y!<1, q, product)

   4.  !Y!   =  !Y!<1, _, product> : (B^k -> B) -> B

This means that !Y!q = 1 if and only if q holds true over the entire
universe of discourse in question, in other words, if and only if q
is the constant true proposition 1 : B^k -> B.  The ambiguities of
this trial usage will not be a problem so long as we distinguish
the context of definition from the context of application and
restrict all shorthand notations to the latter.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o