Continuing this blog post: The set of all pointfree funcoids on upper semilattices with least elements is exactly a certain algebraic structure defined by propositional formulas.
Really just add the identities defining a pointfree funcoid to the identities of an upper semilattice with least element.
I will list the exact list of identities defining a pointfree funcoid on a poset with least element:
(Here is a single relational symbol.)
This can be even generalized for upper semilattices with no requirement to have the least element, if we allow the least element constant symbol to be a partial function.
Note that for the general case of a pointfree funcoid between two upper semilattices, we have a partial algebraic structure because the operations are different for each of the two upper semilattices.
I am curious what are applications of this curious fact.
There may be a (non-fatal) error in the above: It seems that the above bijectively correspond to such pointfree funcoids only in special cases like if our semilattice is a boolean algebra. The construction is interesting nevertheless!
The above can be generalized for arbitrary posets: Instead of the symbol
use the unary predicate symbol
that “determines” if
is the least element and use the definition of free star in terms of arbitrary posets, as in the definition of staroids. In fact this way we would define 2-staroids, not pointfree funcoids, but that’s also interesting. I am going to tell this in details in a later blog post.