# A conjecture about product order and logic

**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 )?

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).