Abstract:
Part One. An Introduction to the Necessary
Terminology, Notation and Some Basics Involving Galois
Connections. Let (P, <) be a "poset" ie a set P with
a binary relation < of "partial ordering". The
"dual" of a poset is defined by the converse partial
ordering on the same members. A "lattice" is a poset
in which each pair of members has both, a least upper
bound and a greatest lower bound. A "complete"
lattice is a lattice in which any set of members,
finite or infinite, has the lub and the glb bounds.
We usually introduce the notation of "a+b" for the
least upper bound of a and b, ie a+b = lub{a,b}, which
we call the "joint" of a and b, and the notation of
"a.b" for the greatest lower bound, ie a.b = glb{a,b},
which we call the "meet" of a and b. A one-to-one
mapping f is called an "isomorphism" from (P, <) to
(Q, <) iff x1 < x2 is equivalent to fx1 < fx2. The f
is called a "dual" isomorphism from (P, <) to (Q, <)
iff x1 < x2 is equivalent to fx2 < fx1.
G-Connections. The pair (g, h) is called a "Galois
connection" (or a G-connection for short) between
posets (P, <) and (Q, <)) iff the mappings g (from P
to Q) and h (from Q to P) are such that
(G1.1) x1 < x2 implies that gx2 < gx1
(G1.2) y1 < y2 implies that hy2 < hy1
(G2.1) x < hgx (G2.2) y < ghy
(G3.1) ghgx = gx (G3.2) hghy = hy
for any members x, x1, x2 of P and any members y, y1,
y2 of Q.
It is well-known that conditions (G3.1) and (G3.2) of
the above list are redundant. Thus we have the
following useful fact.
THEOREM 1. The pair (g, h) is a G-connection iff g
and h satisfy conditions (G1.1) - (G2.2).
Also known is the following theorem.
THEOREM 2 (or The Schmidt Theorem). The conditions
below are equivalent. (i) g, h) is a G-connection
between (P, <) and (Q, <)
(ii) If g is a mapping from (P, <) to (Q, <) and h is
a mapping from (Q, <) to (P, <) then the fact that x
< hy is equivalent to the fact that y < gx, for any
member x of P and member y of Q.
THEOREM 3. If (g,h) is a G-connection between
lattices (P, +, .) and
(Q, +, .) then (i) g(x1+x2) = gx1.gx2; (ii)
h(y1+y2) = hy1.hy2, for any members x1, x2 of P and
members y1, y2 of Q.
That the interchange of the meets and joints of the
above theorem is not generally valid of any Galois
connection. We can only go as far as the
justification of the following relations: g(x1.x2) >
gx1+gx2 and
h(y1.y2) > hy1+hy2.
Strong G-Connections. None of the inequalities
(G2.1) and (G2.2) can be strengthened to an equality
simply on the basis of the definition of a
G-connection. Yet, practical considerations fully
justify the separation of this rather important
subclass of the class of all G-connections by
demanding that the inequalities be strengthened to
equalities.
A G-connection (g, h) between (P, <) and (Q, <) is
called "strong" iff it is "strong on the left" ie
(SG2.1) hgh = x, for any member x of P, and it is
also "strong on the right" ie (SG2.2) ghy = y, for
any member y of Q.
Trivially, each strong G-connection (or an
SG-connection for short) is a G-connection.
THEOREM 4. If (g, h) is an SG-connection between
lattices (P, +, .) and (Q, +, .) then (i) g(x1.x2)
= gx1+gx2; (ii) h(y1.y2) = hy1+hy2, for any members
x1, x2 of P and members y1, y2 of Q.
THEOREM 5. If (g, h) is a G-connection between (P,
<) and (Q, <) then the conditions below are
equivalent. (i) (g, h) is strong on the left;
(ii) h is onto; (iii) g is one-to-one.
THEOREM 6. If (g, h) is a G-connection between (P,
<) and (Q, <) then the conditions below are
equivalent. (i) (g, h) is strong on the right;
(ii) g is onto; (iii) h is one-to-one.
It may be remarked at this junction that some
connections between posets are only strong on the left
or only strong on the right.
THEOREM 7. (i) If (g, h) is a strong G-connection
between (P, <) and (Q, <) then g is one-to-one and h
is a reverse of g.
(ii) If (h, g) is a strong G-connection between (Q,
<) and (P, <) then h is one-to-one and g is a reverse
of h.
Isotone Connections. One of the features of a
G-connection (g, h) is that it only applies to dual
pairs of posets because its defining conditions (G1.1)
and (G1.2) require of the two mappings g and h to be
each antitone. The replacement of (G1.1) and (G1.2)
by their isotone counterparts opens the door for some
modifications and extensions of this original,
connection-based methodology.
The pair (g, h) is an "isotone" connection (or an
I-connection for short) between posets (P, <) and (Q,
<) iff the mappings g (from P to Q) and h (from Q to
P) are such that
(IG1.1) x1 < x2 implies that gx1 < gx2
(IG1.2) y1 < y2 implies that hy1 < hy2
(G2.1) x < hgx (G2.2) y < ghy
(G3.1) ghgx = gx (G3.2) hghy = hy
for any members x, x1, x2 of P and any members y, y1,
y2 of Q.
Unlike in the case of a G-connection, conditions
(G3.1) and (G3.2) are not deducible from conditions
(IG1.1) - (G2.2).
Strong Isotone Connections. The pair (g, h) is a
"strong isotone" connection (or an SI-connection for
short) between posets (P, <) and (Q, <) iff the
mappings g (from P to Q) and h (from Q to P) are such
that
(IG1.1) x1 < x2 implies that gx1 < gx2
(IG1.2) y1 < y2 implies that hy1 < hy2
(SG2.1) hgx = x (SG2.2) ghy = y
for any members x, x1, x2 of P and any members y, y1,
y2 of Q.
THEOREM 8. The conditions below are equivalent.
(i) The pair (g, h) is an SI-connection between
posets (P, <) and (Q, <)
(ii) If g is a mapping from a poset (P, <) to a poset
(Q, <) then the following conditions are
satisfied:
(ii.1) x < hy is equivalent to gx < y, and
(ii.2) y < gx is equivalent to hy < x.
Clearly, the above Theorem involving SI-connections is
a counterpart of Theorem 2 (or the Schmidt Theorem)
involving G-connections.
This brief description of G-connections and some of
the connections of a similar type already shows that
the Galois method is a general and powerful method
with which certain mathematical objects can be
investigated using the isomorphisms between these
objects. It can also be applied, in particular, to
metamathematical objects, something we are concerned
with in the rest of this paper.
Part Two. Some Metamathematical Galois-Connections.
We now employ the method of Galois connections as well
as of some connections similar in kind to discuss the
relationship between the traditional methodological
orthodoxy (which is based on the idea of proof and
polished up with the help of a closure operator), on
the one hand, and some alternative methodologies
(which are based on other ideas such as, for instance,
consistency or some forms of maximality), on the other
hand. Some results in this direction are reported
below.
The symbols "<", "+" and ".", which we keep on using
in this section, now stand for the relation of
set-inclusion, for the operation of set-union and the
operation of set-intersection, respectively. We
denote by S the set of all sentences of a fixed but
not specified object language, and we use letters X,
Y, Z, ... and A, B, C, ... to denote subset of S and
members of S, respectively. We also use the notation
of the type of "2Z". This last notation stands for
the class of all subsets of S which extend the set Z.
And, clearly, letter O stands for the empty set.
(I) Strongly regular closure operators versus regular
consistency properties. Let CO be the set of all
strongly regular closure operators Cn. This means
that
(i) X < Cn(X)
(ii) X < Y implies that Cn(X) < Cn(Y)
(iii) Cn(Cn(X)) < Cn(X)
(iv) if A is not a member of Cn(X) then there is a
set Z extending X and such that A is not a member of
Cn(Z) and Cn(Z+{B}) = S for any B which is not a
member of Z. In other words, every A-omitting set
can be extended to an A-omitting set which has no
A-omitting proper superset.
And let CP be the set of all regular consistency
properties Cons. This means that
(i) S is not a member of Cons
(ii) the fact that X is a member of Cons .2Y implies
that Y is also a member of Cons
(iii) the fact that X is a member of Cons implies
that there is a member Z of Cons .2X such that Z' = Z
for any member Z' of Cons .2Z. In other words, each
member of Cons is a subset of a inclusion-maximal
member of Cons.
We accept the following two pivotal definitions, one
definition of a consistency property Cons[Cn] in terms
of a closure operator Cn, and the other definition of
a closure operator Cn[Cons] in terms of a consistency
property Cons.
X is a member of Cons[Cn] iff Cn(X) != S.
A is a member of Cn[Cons](X) iff Y+{A} is a member
of Cons for any member Y of Cons .2X.
On the basis of these definitions we obtain the
following theorem.
THEOREM 9. The pair (Cons[Cn], Cn[Cons]) is a
strong Galois connection between the complete lattices
(CO, <) and (CP, <).
(II) Strongly regular closure operators versus
regular Lindenbaum operators. Let LN be the set of
all regular Lindenbaum operators Ln. This means that
(i) Ln(S) = O; (ii) Ln(X) < 2X
(iii) Ln(O) .2X < Ln(X); (iv) X < Y implies that
Ln(Y) < Ln(X)
(v) the fact that X is a member of Ln(O) and Y is a
member of Ln(X) implies that X = Y.
Here we also have two pivotal definitions, one
definition of a Lindenbaum operator Ln[Cn] in terms of
Cn, and the other definition of a closure operator
Cn[Ln] in terms of a Lindenbaum operator Ln.
X is a member of Ln[Cn](Y) iff X is a member of 2Y,
Cn(X) != S and Z = X for any member Z of 2X such that
Cn(Z) != S.
A is a member of Cn[Ln](X) iff Ln(X) < Ln(X+{A}).
THEOREM 10. The pair (Ln[Cn], Cn[Ln]) is a strong
Galois connection between the complete lattices (CO,
<) and (LN, <).
(III) Strongly regular closure operators versus
families of maximal sets. Let MAX stand for the set
of all families of maximal sets, ie
(i) S is not a member of Max
(ii) X = Y for any member X of Max and any member Y
of Max .2X
Our pivotal definitions, ie the definition of Max[Cn]
in terms of Cn and the definition of Cn[Max] in terms
of Max are as follows.
X is a member of Max[Cn] iff Y = X for any member of
Y of 2X such that Cn(Y) != S.
A is a member of Cn[Max](X) iff A is a member of Y
where Y is an arbitrary member of Max .2X.
THEOREM 11. The pair (Max[Cn], Cn[Max]) is a
strong Galois connection between the complete lattices
(CO, <) and (MAX, <).
(IV) Regular Lindenbaum operators versus families of
maximal sets. The pivotal definitions here, ie the
definition of Max[Ln] in terms of Ln and the
definition of Ln[Max] in terms of Max are as follows.
X is a member of Max[Ln] iff X is a member of Ln(O).
X is a member of Ln[Max](Y) iff x is a member of Max
.2Y.
THEOREM 12. The pair (Max[Ln], Ln[Max]) is a
strong isotone connection between the complete
lattices (LN, <) and (MAX, <).