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 (firstname.lastname@example.org) 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 (email@example.com) 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 )?