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

Product order ${\prod \mathfrak{A}}$ of posets ${\mathfrak{A}_i}$ (for ${i \in n}$ where ${n}$ is some index subset) is defined by the formula ${a \leq b \Leftrightarrow \forall i \in n : a_i \leq b_i}$. (By the way, it is a product in the category ${\mathbf{Pos}}$ of posets.)

By definition the lambda-function ${\lambda x \in D : F (x) = \left\{ (x ; F (x)) \mid x \in D \right\}}$ for a form ${F}$ depended on variable ${x}$.

It is easy to show that for a product of distributive lattices with least elements we have lattice-theoretic difference ${a \setminus b = \lambda i \in n : a_i \setminus b_i}$ whenever every ${a_i \setminus b_i}$ is defined. Compare also ${a \sqcup b = \lambda i \in n : a_i \sqcup b_i}$ (where ${\sqcup}$ denotes supremum of two elements), whenever every ${a_i \sqcup b_i}$ is defined.

I conjecture that this equality can be generalized to a relatively wide class of functions ${F}$ of a finite number of elements: ${F (x_0, \ldots, x_k) = \lambda i \in n : F (x_{0, i}, \ldots, x_{k, i})}$.

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 ${A}$, ${B}$, ${C}$, … and two binary relations ${=}$ and ${\leq}$ including at least the following axioms:

• ${A = A}$; ${A = B \Rightarrow B = A}$; ${A = B \wedge B = C \Rightarrow A = C}$ (equality axioms);
• ${A \leq A}$; ${A \leq B \wedge B \leq C \Rightarrow A \leq C}$; ${A \leq B \wedge B \leq A \Rightarrow A = B}$ (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 ${P_0 (y, x_0, \ldots, x_{k_0})}$, ${P_1 (y, x_0, \ldots, x_{k_1})}$, ${P_2 (y, x_0, \ldots, x_{k_2})}$, … such that it can be proved that ${y}$ is unambiguously determined by ${x_0}$, …, ${x_{k_0}}$, ${x_0}$, …, ${x_{k_1}}$, ${x_0}$, …, ${x_{k_2}}$, …

For example, the function ${\sqcup}$ is defined by the formula:

• ${A \sqcup B \leq C \Leftrightarrow A \leq C \wedge B \leq C}$.

That this definition of ${\sqcup}$ 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 ${A \setminus B}$, boolean lattice complement and even co-brouwerian pseudodifference ${A \setminus^{\ast} B}$.

Conjecture: For every partial axiomatic function we have ${F (x_0, \ldots, x_k) = \lambda i \in n : F (x_{0, i}, \ldots, x_{k, i})}$ whenever every ${F (x_{0, i}, \ldots, x_{k, i})}$ is defined (Is it equivalent to ${F (x_0, \ldots, x_k)}$ 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 ${\sup x = \lambda i \in n : \sup x_i}$ (where ${\sup}$ 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 ${\mathbf{Pos}}$)?