SUO: Mapping Closure
All,
I was thinking about this during the fireworks display last evening and
thought I should write it down.
*Entailment closure* is one of the most important concepts in the semantics
of first order logic. However, there is another notion of closure that is
important in moving theories about. I call this *mapping closure*.
====================
Definition: An *adjoint pair* of monotonic functions
(left, right) : (P0, <=0) --> (P1, <=1)
from source preorder (P0, <=0) to target preorder (P1, <=1) consists of
1. a *left adjoint* monotonic function
left : (P0, <=0) --> (P1, <=1)
2. a *right adjoint* monotonic function
left : (P1, <=1) --> (P0, <=0)
which satisfy the adjointness condition
left(p0) <=1 p1 iff p0 <=0 right(p1)
for any two elements p0 \in P0 and p1 \in P1.
Symbolized as: left -| right.
A pair of adjoint monotonic functions defines both a closure and an interior
operator.
Definition: The *closure* operator for an adjoint pair (left, right) is the
composite monotonic function on the source order
closure ^= left o right : (P0, <=0) --> (P0, <=0).
This satisfies the two conditions:
* closure o closure == closure
"closure is idempotent"
* identity <= closure
"closure contains the identity.
The interior operator is dual.
Fact: The *opposite* of the above adjoint pair is also an adjoint pair
(right^op, left^op) : (P1, >=1) --> (P0, >=1)
from the opposite of the target preorder (P1, <=1)^op = (P1, >=1) to the
opposite of the source preorder (P0, <=0)^op = (P0, >=1).
Fact: Left adjoints preserve any joins that exist and right adjoints
preserve any meets that exist.
====================
As a special case, for any function
f : A --> B
from source set A to target set B,
there is an adjoint pair of monotonic functions
(exists(f), subst(f)) : (pow(A), \subset_A) --> (pow(B), \subset_B)
from the power poset of subsets of A to the power poset of subsets of B,
where the left adjoint is the *exist*(ential) operator
exists(f) : (pow(A), \subset_A) --> (pow(B), \subset_B)
maps a subset X \subset A to the subset of B
exists(f)(X) ^= {b \in B | exists a \in B, f(a) = b and a \in X}
= {b \in B | exists a \in X, f(a) = b}.
and the right adjoint is the *subst*(itution) operator
subst(f) : (pow(B), \subset_B) --> (pow(A), \subset_A)
maps a subset Y \subset B to the subset of A
subst(f)(Y) ^= {a \in A | f(a) \in Y}.
Check adjointness:
exists(f)(X) \subset_B Y
iff f(a) \in Y for all a \in X
iff X \subset_A subst(f)(Y)
for any two subsets X \subset A and Y \subset B.
The exist(ential) operator) is usually called the *direct image* operator,
and the subst(itution) operator is usually called the *inverse image*
operator. However, I have used the alternate names on purpose here -- they
manifest the logical dual universal operator, and I am using the
direct/inverse image terminology in another related sense.
The *closure* operator (monotonic function)
closure ^= exist o subst : (pow(A), \subset_A) --> (pow(A), \subset_A)
maps a subset X \subset A to the subset of A
closure(X) = {a \in A | f(a) \in exists(f)(X)}
{a \in A | exists a' \in X, f(a') = f(a)}
\union {[a] | a \in A},
where [a] is the equivalence class for the element a, and the equivalence
relation is the kernel equivalence ~_f induced by the function f:
a ~_f a' when f(a) = f(a').
Logically dual to the exist(ential) operator (monotonic function)
exists(f) : (pow(A), \subset_A) --> (pow(B), \subset_B)
is the *forall* (universal) operator (monotonic function)
forall(f) : (pow(A), \subset_A) --> (pow(B), \subset_B)
which maps a subset X \subset A to the subset of B
forall(f)(X) ^= {b \in B | forall a \in A, if f(a) = b then a \in X}.
Fact: The pair
(subst(f), forall(f)) : (pow(B), \subset_B) --> (pow(A), \subset_A)
is an adjoint pair of monotonic functions from the power poset of subsets of
B to the power poset of subsets of A.
Check adjointness:
subst(f)(Y) \subset_A X
iff {a \in A | f(a) \in Y} \subset_A X
iff Y \subset_B {b \in B | forall a \in A, if f(a) = b then a \in X}
iff Y \subset_B forall(f)(X)
for any two subsets Y \subset B and X \subset A.
Summary symbolization: exists -| subst -| forall.
====================
Consider a language morphism
f : L0 --> L1.
Recall that f maps L0 relation (function, sort) symbols to L1 relation
(function, sort) symbols to relation, preserving arity and signature.
This extends to the (recursively defined) expression function
expr(f) : expr(L0) --> expr(L1)
that maps L0 expressions to L1 expressions, also preserving arity and
signature.
Definition: The theory poset (lattice) over a FOL language L is the
collection of all subsets of expressions ordered by reverse subset
inclusion:
th(L) ^= (pow(expr(L)), \subset)^op = (pow(expr(L)), \supset).
Apply the exists -| subst -| forall adjunctions to the expression function.
Define the *(existential) direct image* operator to be the opposite of the
exist(ential) operator applied to the expression function:
dir(f) ^= exists(expr(f))^op : th(L0) --> th(L1)
and the inverse image operator to be the opposite of the subst(itution)
operator applied to the expression function:
inv(f) ^= subst(expr(f)) : th(L1) --> th(L0).
Fact: The inverse-(existential) direct pair form an adjoint pair of
monotonic functions
(inv(f), dir(f)) : th(L1) --> th(L0)
between lattices of theories. Being left adjoint, the inverse image operator
preserves joins (intersections). Being right adjoint, the (existential)
direct image operator preserves meets (unions).
Fact: The existential direct image operator is part of the colimit operator
on theories:
col(D) = meet(flow(D))
for any diagram of theories, where flow(D) is defined pointwise as the
existential direct image.
Define the *mapping closure* to be the inv(f)-dir(f) interior:
map-clo(L)(T0) = inv(f)(dir(f)(T0)
for any theory T0 \in th(L0). Note: even though it is strictly speaking an
interior operator with the opposite subset ordering (and also the entailment
ordering), we follow the tradition of entailment and call this a closure
operator.
Define the *(universal) direct image* operator to be the opposite of the
forall (universal) operator applied to the expression function:
dir'(f) ^= forall(expr(f))^op : th(L0) --> th(L1).
Fact: The (universal) direct-inverse image pair form an adjoint pair of
monotonic functions
(dir'(f), inv(f)) : th(L0) --> th(L1)
between lattices of theories. Being left adjoint, the (universal) direct
image operator preserves joins (intersections). Being right adjoint, the
inverse image operator preserves meets (unions).
In summary: dir' -| inv -| dir, with dir' and inv preserving joins
(intersections), and inv and dir preserving meets (unions).
Two questions arise:
1. What is the significance of the mapping closure?
2. Which quantificational direct image operator should be used for
moving theories?
====================
My answers to these questions are as follows.
1. I maintain that mapping theories along a language morphism requires a
commitment to mapping closure. In other words, if one is willing to use a
language morphism to map a theory, then one is committing oneself to the
mapping closure of that theory; that is, one is essentially asserting all of
the additional axioms in the difference between the theory and its mapping
closure.
2. The existential direct image operator is seen to be important by its use
in colimits. But what about the universal direct image operator? The fact is
that the two operators are identical on the mapping closure of a theory.
Hence, if we commit ourselves to the mapping closure of a theory, it does
not matter which direct image operator we use, since they are both equal in
this case.
Robert E. Kent
rekent@ontologos.org