A conjecture about product order and logic

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



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

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

Leave a Reply