Advertisements
Skip to content
November 7, 2019 / porton

Every Pointfree Funcoid on a Semilattice is an Algebraic Structure

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:

  • x \leq x
  • x \leq y \land y \leq z \Rightarrow x \leq z
  • x \leq y \land y \leq x \Rightarrow x=y
  • \bot \leq y
  • \lnot(\bot [f] y)
  • \lnot(x [f] \bot)
  • x \cup y \leq z \Leftrightarrow x \leq z \land y \leq z
  • i\cup j[f]k \Leftrightarrow i[f]k\lor j[f]k
  • k[f]i\cup j \Leftrightarrow k[f]i\lor k[f]j

(Here [f] 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.

Advertisements

2 Comments

Leave a Comment
  1. porton / Nov 7 2019 13:46

    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!

    Like

  2. porton / Nov 7 2019 14:18

    The above can be generalized for arbitrary posets: Instead of the symbol \bot use the unary predicate symbol \mathrm{Least}(x) that “determines” if x 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.

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: