The considerations below were with an error, see the comment.
Product order $latex {\prod \mathfrak{A}}&fg=000000$ of posets $latex {\mathfrak{A}_i}&fg=000000$ (for $latex {i \in n}&fg=000000$ where $latex {n}&fg=000000$ is some index subset) is defined by the formula $latex {a \leq b \Leftrightarrow \forall i \in n : a_i \leq b_i}&fg=000000$. (By the way, it is a product in the category $latex {\mathbf{Pos}}&fg=000000$ of posets.)
By definition the lambda-function $latex {\lambda x \in D : F (x) = \left\{ (x ; F (x)) \mid x \in D \right\}}&fg=000000$ for a form $latex {F}&fg=000000$ depended on variable $latex {x}&fg=000000$.
It is easy to show that for a product of distributive lattices with least elements we have lattice-theoretic difference $latex {a \setminus b = \lambda i \in n : a_i \setminus b_i}&fg=000000$ whenever every $latex {a_i \setminus b_i}&fg=000000$ is defined. Compare also $latex {a \sqcup b = \lambda i \in n : a_i \sqcup b_i}&fg=000000$ (where $latex {\sqcup}&fg=000000$ denotes supremum of two elements), whenever every $latex {a_i \sqcup b_i}&fg=000000$ is defined.
I conjecture that this equality can be generalized to a relatively wide class of functions $latex {F}&fg=000000$ of a finite number of elements: $latex {F (x_0, \ldots, x_k) = \lambda i \in n : F (x_{0, i}, \ldots, x_{k, i})}&fg=000000$.
I do not hold the claim of originality of this conjecture. Moreover, I ask you to notify me ([email protected]) 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 $latex {A}&fg=000000$, $latex {B}&fg=000000$, $latex {C}&fg=000000$, … and two binary relations $latex {=}&fg=000000$ and $latex {\leq}&fg=000000$ including at least the following axioms:
- $latex {A = A}&fg=000000$; $latex {A = B \Rightarrow B = A}&fg=000000$; $latex {A = B \wedge B = C \Rightarrow A = C}&fg=000000$ (equality axioms);
- $latex {A \leq A}&fg=000000$; $latex {A \leq B \wedge B \leq C \Rightarrow A \leq C}&fg=000000$; $latex {A \leq B \wedge B \leq A \Rightarrow A = B}&fg=000000$ (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 $latex {P_0 (y, x_0, \ldots, x_{k_0})}&fg=000000$, $latex {P_1 (y, x_0, \ldots, x_{k_1})}&fg=000000$, $latex {P_2 (y, x_0, \ldots, x_{k_2})}&fg=000000$, … such that it can be proved that $latex {y}&fg=000000$ is unambiguously determined by $latex {x_0}&fg=000000$, …, $latex {x_{k_0}}&fg=000000$, $latex {x_0}&fg=000000$, …, $latex {x_{k_1}}&fg=000000$, $latex {x_0}&fg=000000$, …, $latex {x_{k_2}}&fg=000000$, …
For example, the function $latex {\sqcup}&fg=000000$ is defined by the formula:
- $latex {A \sqcup B \leq C \Leftrightarrow A \leq C \wedge B \leq C}&fg=000000$.
That this definition of $latex {\sqcup}&fg=000000$ 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 $latex {A \setminus B}&fg=000000$, boolean lattice complement and even co-brouwerian pseudodifference $latex {A \setminus^{\ast} B}&fg=000000$.
Conjecture: For every partial axiomatic function we have $latex {F (x_0, \ldots, x_k) = \lambda i \in n : F (x_{0, i}, \ldots, x_{k, i})}&fg=000000$ whenever every $latex {F (x_{0, i}, \ldots, x_{k, i})}&fg=000000$ is defined (Is it equivalent to $latex {F (x_0, \ldots, x_k)}&fg=000000$ to be defined?).
Please notify me ([email protected]) if you know a solution of this conjecture.
Further generalization may be interesting. For example, our above consideration does not consider the formula $latex {\sup x = \lambda i \in n : \sup x_i}&fg=000000$ (where $latex {\sup}&fg=000000$ 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 $latex {\mathbf{Pos}}&fg=000000$)?
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).