The considerations below were with an error, see the comment.

Product order of posets (for where is some index subset) is defined by the formula . (By the way, it is a product in the category of posets.)

By definition the lambda-function for a form depended on variable .

It is easy to show that for a product of distributive lattices with least elements we have lattice-theoretic difference whenever every is defined. Compare also (where denotes supremum of two elements), whenever every is defined.

I conjecture that this equality can be generalized to a relatively wide class of functions of a finite number of elements: .

I do not hold the claim of originality of this conjecture. Moreover, I ask you to notify me (porton@narod.ru) if you know a work where a similar theory was described.

Now (to formulate the conjecture precisely) it is required to lay some formalistic.

I call an an order logic a set of propositional axioms (without quantifiers) with variables , , , … and two binary relations and including at least the following axioms:

; ; (equality axioms);

; ; (partial order axioms).

By definition a partial axiomatic function for a given order logic is a partial function of a finite number of arguments which is unambigously defined by some set of additional propositional formulas (the definition). I mean that we have some finite set of propositional formulas , , , … such that it can be proved that is unambiguously determined by , …, , , …, , , …, , …

For example, the function is defined by the formula:

.

That this definition of is unambiguous is a well known fact. Note that is general this function of two arguments is partial (as not every order is a semilattice).

Distributive lattices, Heyting algebras, and boolean algebras can be defined as examples of order logics.

Similarly we can define as partial axiomatic functions lattice-theoretic difference , boolean lattice complement and even co-brouwerian pseudodifference .

Conjecture: For every partial axiomatic function we have whenever every is defined (Is it equivalent to to be defined?).

Please notify me (porton@narod.ru) if you know a solution of this conjecture.

Further generalization may be interesting. For example, our above consideration does not consider the formula (where is the supremum on our poset), because supremum is a function of infinite arity, while we considered only finite relations.

Can it also be generalized for categorical product (not only in category )?

It seems that we can define it by interleaved adding new axioms and claiming that a function defined by such axioms is total. That is: we add some axioms, we define a partial function (such as binary join) as conforming to these axioms, then claim that the function is total (for example, for binary joins this means that we are in a join-semilattice), then again add new axioms, etc.

I am not sure whether I will keep thinking about this research idea, my research is mostly different in essence. Feel free to make a research article from this my idea (just notify me that you want to consider my idea).

Well, I seem to mistake. It looks like that join-semilattices cannot be defined as an order logic. The conjecture need to be re-formulated.

It seems that we can define it by interleaved adding new axioms and claiming that a function defined by such axioms is total. That is: we add some axioms, we define a partial function (such as binary join) as conforming to these axioms, then claim that the function is total (for example, for binary joins this means that we are in a join-semilattice), then again add new axioms, etc.

I am not sure whether I will keep thinking about this research idea, my research is mostly different in essence. Feel free to make a research article from this my idea (just notify me that you want to consider my idea).