Of what kind of complemented bounded poset are the structures in my quasi-variety?

I feel that my question is very basic, but, somewhat suprisingly, nobody was able to give me an answer so far:

Let

$\mathbf{M} := \langle \{ 0,1 \}, 0, 1, \leq, \neg \rangle$

be the structure with the obvious definitions for the relation $\leq$ and the unary mapping $\neg$.

Let us consider all elements in the quasi-variety $\mathbb{ISP}(\mathbf{M})$ (that is, all isomorphic copies of substructures of direct powers of $\mathbf{M}$).

What is a characterization of the structures among $\mathbb{ISP}(\mathbf{M})$?

I can see that they are bounded posets that are somehow complemented. However, the complement operation is not only an order-reversing involution but it also requires $x \nleq \neg x$ for all $x \neq 0$. In other words, I think the complement operation acts like the complement-operation on sets.

My guess is the following:

Characterization: $\mathbf{X} = \langle X, 0,1,\leq,\neg \rangle$ is in the above quasi-variety if and only if $\langle X,0,1,\leq \rangle$ is a bounded poset (with minimum element $0$ and maximum element $1$), and $\neg$ is an order-reversing involution such that $x \leq \neg x$ implies $x=0$.

However, this is only a guess. Since the structure seems natural, I guess that it is well-known in some mathematical area. However, I have not found this area yet as even people that have rather deep knowledge in the fields of lattice theory and ordered sets could not instantly provide an answer.

Can anybody of you provide me with some insight?

By the way: My interest in this quasi-variety comes from the fact that the category formed by the finite structures among $\mathbb{ISP}(\mathbf{M})$ (with the structure-preserving mappings as morphisms) is dually equivalent to the category of finite median algebras. Actually, one does not need to restrict this to the finite structures, but if you don't do this, you need to equip the quasi-variety from above with a discrete topology and only consider topologically closed substructures. For those that are interested, this is was done by Isbell and is (in a much more general fashion) explained in Clark und Daveys book "Natural dualities for the working algebraist"). However, my researach only touches the finite structures, so you don't find the topology above.

Update

In the comments blow, Gerhard aks whether the order relation in a given structure of my quasi-variety is necessarily a lattice-order (i.e., one can define join and meet with this order relation). The following example shows that this is not the case.

Let $S = \{a,b,c,d\}$.

and consider

$\langle \{ \emptyset, \{a\}, \{b\}, \{c\}, \{d\}, S \setminus \{a\}, S \setminus \{b\}, S \setminus \{c\}, S \setminus \{d\}, S\}, \emptyset, S, \subseteq, (-)^c \rangle$

with $(-)^c$ being the set-theoretical complement operation.

Clearly, this structure is in my qausi-variety, but $\subseteq$ is not a lattice-order, since, for example, the meet of $S \setminus \{a\}$ and $S \setminus \{b\}$ cannot be defined.

-
Comment 1: Can you define join and meet from this structure? IF so, you may actually be dealing with distributive lattices with complement. If you can exhibit a structure that is not so interpreted, then it is clear that join and meet cannot be so defined. Gerhard "Ask Me About System Design" Paseman, 2011.01.18 – Gerhard Paseman Jan 18 '11 at 23:53
Comment 2: Do you know much about the congruences of this structure? Including it in an appropriate variety may allow you to apply theorems that say stuff about congruence-modular and congruence-distributive classes. It may lead in a different direction, but that direction may be fruitful to you. Gerhard "Ask Me About System Design" Paseman, 2011.01.18 – Gerhard Paseman Jan 18 '11 at 23:56
@Gerhard: Congruence identities are useful in dealing with varieties, not quasi-varieties. The question is about a basis of quasi-identities of certain quasivariety. Congruence identities are of little help for such questions. – Mark Sapir Jan 19 '11 at 0:50
Indeed, Mark. For over 3 years I programmed myself to think "finite basis" = "finite basis in equational logic" = "finite basis of identities" towards a problem I was studying. My 2nd comment came from thinking of results for congruence-modular (and stronger) conditions on varieties and not remembering which results applied to more general classes. Gerhard "Time To Unlearn Some Things" Paseman, 2011.01.18 – Gerhard Paseman Jan 19 '11 at 1:55
@Gerhard No, one cannot define join and meet in general. I edited my posting above such that it now contains a counterexample to this. – Niemi Jan 19 '11 at 10:17

Here is a suggestion which favors your characterization. Assuming you characterization is correct, the main problem is to take any appropriate self-dual bounded poset with no fixed points from the involution, and show it isomorphic to a subalgebra of a power of your structure. The idea is to use some set X such as the order ideals for the poset ( or look at something which looks like the join-irreducibles in a lattice ) and map the poset into 2^X in such a way that the desired isomorphism becomes apparent. Again, the ideas come from analyzing the subdirect irreducible algebras in certain varieties (semilattices and lattices), and in results similar to the Stone representation theorem, so you may be able to borrow much from the literature.

Update: Also see Rautenberg, Wolfgang $2$-element matrices. Studia Logica 40 (1981), no. 4, 315–353 (1982).It is about a general theory of 2-element algebras including their quasi-identities.