Lattice theory with operations
A lattice consists of domain D of objects a, b, c, . . .with a relation of partial order a ⩽ b. An equality relation is defined by a = b ≡ a ⩽ b & b ⩽ a. Next we have two operations by which new objects can be constructed:
a ∧ b the meet of a and b
a ∨ b the join of a and b
The axioms are:
I General properties of the basic relation
Reflexivity: a ⩽ a
Transitivity: a ⩽ b & b ⩽ c ⊃ a ⩽ c
II Properties of constructed objects
a ∧ b ⩽ a
a ∧ b ⩽ b
a ⩽ a ∨ b
b ⩽ a ∨ b
III Uniqueness of constructed objects
c ⩽ a & c ⩽ b ⊃ c ⩽ a ∧ b
a ⩽ c & b ⩽ c ⊃ a ∨ b ⩽ c
Relational lattice theory
Relational axiomatizations replace operations with relations. For example, relational lattice theory is based on the idea of adding two three-place relations M(a, b, c), J (a, b, c), read as ‘the meet of a and b is c’ and ‘the join of a and b is c’, and axioms that state the existence of meets and joins:
∀x∀y∃zM(x, y, z)
∀x∀y∃zJ(x, y, z)
There are many more axioms as compared to an axiomatization with operations, but there are no functions:
I General properties of the basic relations
Reflexivity: a ⩽ a
Transitivity: a ⩽ b & b ⩽ c ⊃ a ⩽ c
II Properties of meet and join
M(a, b, c) ⊃ c ⩽ a
M(a, b, c) ⊃ c ⩽ b
J(a, b, c) ⊃ a ⩽ c
J(a, b, c) ⊃ b ⩽ c
III Uniqueness of meet and join
M(a, b, c) & d ⩽ a & d ⩽ b ⊃ d ⩽ c
J(a, b, c) & a ⩽ d & b ⩽ d ⊃ c ⩽ d
Substitution of equals in the meet and join relations needs to be postulated,
with a = b ≡ a ⩽ b & b ⩽ a. The relations have three arguments, so to cut
down the number of axioms, we do as follows:
IV Substitution axioms
M(a, b, c) & a = d & b = e & c = f ⊃ M(d, e, f )
J(a, b, c) & a = d & b = e & c = f ⊃ J(d, e, f )
Substitution in one argument, say d for a in M(a, b, c), is obtained by the
instance M(a, b, c) & a = d & b = b & c = c ⊃ M(d, b, c).
Finally, we have:
V Existence of meets and joins
∀x∀y∃zM(x, y, z)
∀x∀y∃zJ(x, y, z)
Show that derivations in relational lattice theory and lattice theory with operations can be translated to each other.
Below is a clean way to see that the two presentations are definitionally equivalent—so proofs/derivations translate back and forth mechanically.
1) From operations to relations
Add definitions. Work in the language with ≤, ∧, ∨ and define the ternary relations by
$$ M(a,b,c)\;:\iff\; c=a\wedge b,\qquad J(a,b,c)\;:\iff\; c=a\vee b. $$
Because terms always denote, we also have the existence axioms
$$ \forall x\forall y\;\exists z\,M(x,y,z)\quad\text{and}\quad \forall x\forall y\;\exists z\,J(x,y,z) $$
(witnesses are $x\wedge y$ and $x\vee y$).
Relational axioms follow. Using the lattice axioms with operations:
- II(M/J): from $c=a\wedge b$ we get $c\le a$ and $c\le b$; from $c=a\vee b$ we get $a\le c$ and $b\le c$.
- III(M/J): if $c=a\wedge b$ and $d\le a,b$ then $d\le c$ (meet’s defining property), and dually for joins.
- IV (substitution for $M,J$): since $M(a,b,c)$ is just $c=a\wedge b$, substitution for $M$ reduces to substitution into equality and into $\wedge,\vee$. In the lattice theory, equality is a congruence for $\wedge,\vee$ (use monotonicity of $\wedge,\vee$, derivable from II–III, to get: $a=a',b=b'\Rightarrow a\wedge b=a'\wedge b'$; similarly for $\vee$).
Hence every axiom of the relational theory is a theorem of the operational theory under the above definitions. So any derivation that uses $M,J$ can be reproduced by replacing $M(a,b,c)$ with $c=a\wedge b$ and $J(a,b,c)$ with $c=a\vee b$.
How to translate any formula with $\wedge,\vee$ to relational form. To remove function symbols, use the standard term-graph translation. For each term $t$, define a formula $\llbracket t\rrbracket(v)$ (“$v$ is the value of $t$”):
- $\llbracket x\rrbracket(v) \equiv v=x$.
- $\llbracket s\wedge t\rrbracket(v) \equiv \exists u\,\exists w\,(\llbracket s\rrbracket(u)\land \llbracket t\rrbracket(w)\land M(u,w,v))$.
- $\llbracket s\vee t\rrbracket(v) \equiv \exists u\,\exists w\,(\llbracket s\rrbracket(u)\land \llbracket t\rrbracket(w)\land J(u,w,v))$.
Translate an atomic $R(t_1,\dots,t_n)$ by introducing fresh $v_i$ and writing
$$ \exists v_1\cdots\exists v_n\Big(\bigwedge_i\llbracket t_i\rrbracket(v_i)\;\land\;R(v_1,\dots,v_n)\Big), $$
and commute the translation through $\neg,\land,\to,\forall$ in the usual way. With the above definitions of $M,J$, this translation is provably equivalent in the operational theory, so derivations carry over step-by-step.
2) From relations to operations
Unique existence of meets/joins. In the relational theory we can prove
$$ \forall x\forall y\;\exists! z\,M(x,y,z)\qquad\text{and}\qquad \forall x\forall y\;\exists! z\,J(x,y,z). $$
Existence is axiom V. Uniqueness: if $M(a,b,c)$ and $M(a,b,c')$, then by II we have $c\le a,b$ and $c'\le a,b$; by III (meet’s uniqueness) $c\le c'$ and $c'\le c$, hence $c=c'$.
Introduce function symbols definitionally. By unique existence you may conservatively add binary function symbols $\wedge,\vee$ satisfying
$$ \forall x\forall y\,M(x,y,\,x\wedge y)\quad\text{and}\quad \forall x\forall y\forall z\,(M(x,y,z)\to z=x\wedge y), $$
and likewise for $J$ and $\vee$. After this definitional extension, every occurrence of $M(x,y,z)$ is inter-derivable with $z=x\wedge y$ (and similarly for $J$).
Operational axioms follow.
- II: From $M(a,b,a\wedge b)$ and II(M) we get $a\wedge b\le a$ and $a\wedge b\le b$; similarly for joins from II(J).
- III: If $d\le a,b$ and $M(a,b,a\wedge b)$, III(M) gives $d\le a\wedge b$; dually for joins.
- I (≤ reflexive/transitive) are shared verbatim.
Thus the standard lattice axioms with $\wedge,\vee$ are derivable in the relational theory after the definitional introduction of $\wedge,\vee$.
Congruence (substitution) for $\wedge,\vee$. From II–III one derives monotonicity:
$$ a\le a',\;b\le b' \;\Rightarrow\; a\wedge b\le a'\wedge b'\quad\text{and}\quad a\le a',\;b\le b' \;\Rightarrow\; a\vee b\le a'\vee b'. $$
Hence if $a=a'$ and $b=b'$ (i.e., both directions of ≤ hold), then $a\wedge b=a'\wedge b'$ and $a\vee b=a'\vee b'$. This recovers the substitution axiom IV for $M,J$ when you re-express $M,J$ as equalities to $\wedge,\vee$.
Formula translation back to operations. Now simply replace each atomic $M(s,t,u)$ by $u=s\wedge t$ and $J(s,t,u)$ by $u=s\vee t$; the rest of the connectives/quantifiers stay the same. Because $\wedge,\vee$ were introduced by definition from $M,J$, this translation preserves and reflects derivability.
3) Conclusion (proof/derivation transport)
- Starting with a derivation in the operational theory, either (a) add the definitions $M(a,b,c)\leftrightarrow c=a\wedge b$, $J(a,b,c)\leftrightarrow c=a\vee b$ and read the same derivation, or (b) eliminate $\wedge,\vee$ by the term-graph translation $\llbracket\cdot\rrbracket$ above.
- Starting with a derivation in the relational theory, first derive $\exists !$ witnesses (as above), add $\wedge,\vee$ by definitional extension, replace $M,J$ by equalities to $\wedge,\vee$, and read the same derivation.
In model-theoretic terms, each theory is a definitional extension of the other, hence they prove exactly the same sentences once symbols are translated. Consequently, every derivation in one presentation can be uniformly, step-by-step translated into a derivation in the other.
No comments:
Post a Comment