# Do sole sufficient operators have to abbreviate existing functions?

I'm wondering whether a sole sufficient operator needs to be an abbreviation of existing functions or not.

More concretely, consider an equational theory $$E$$ in which the sole function is a binary function symbol $$\to$$ consisting of all equations $$\varphi(\vec{x}) = \psi(\vec{x})$$ such that $$\varphi(\vec{x}) \leftrightarrow \psi(\vec{x})$$ is a theorem of classical propositional calculus.

$$\to$$ is certainly a sole sufficient operator for $$E$$.

I'm wondering whether $$\barwedge$$ is a sole sufficient operator for $$E$$.

$$x \to y$$ is certainly equivalent to $$x \barwedge (y \barwedge y)$$, but $$\barwedge$$ is much more powerful.

The $$\to$$-fragment of classical propositional logic is not capable of expressing an outright contradiction, but with $$\barwedge$$ we can express it as $$a \barwedge (a \barwedge a)$$. This observation proves that $$\barwedge$$ is not an abbreviation for some expression containing only $$\to$$ as functions.

However, the fact that $$a \barwedge (a \barwedge a)$$ is a contradiction in the ur-semantics is not strictly speaking a problem. We can take our original theory $$E$$, go through, and replace all occurrences of $$\to$$ with its $$\barwedge$$-encoding and get a new theory $$E^\barwedge$$. $$E^\barwedge$$ is merely not a complete theory.

So I guess my question is:

1. Can you call $$\barwedge$$ a sole sufficient operator?
2. If (1), is there a way to distinguish $$\barwedge$$ from SSO's that are definable in terms of the existing functions? If not (1), what do you call the type of thing that $$\barwedge$$ is?