the core gular factorization in Boole , the category of Boolean algebras is the standard
surjective/injective factorization.
Before doing so, however, let's see the connection with the Beth theorem. Let L be a
language (in the sense of [C/K]) for propositional logic, that is, a set of atomic propositions. Let
P be a further atom, and L(P) = Lu{ P} . Let T be a theory in the language L(P) , that is,
a set of L{P) -sentences. We write T(P) for T; replacing P by a new atom Q throughout
results in T{Q) . We say that T implicitly defines P over L , if T{P) u T{Q) h P f - ) Q .
Here, h denotes formal deducibility; via completeness, implicit definability means that any
L-structure (interpretation of all atoms in L by true or false) can be completed in at most one
way to a model of T . T explicitly defines P over L if there is an L-sentenee p such that
T( P) h P— p . The theorem says that
if T implicitly defines P over L , then T explicitly defines P over L .
The converse is obvious.
With any theory T in any language L (in propositional logic), we associate
LT (L, T) , the Lindenbaum-Tarski algebra of (L, T) . LT (L, T) is the Boolean algebra
whose elements are the equivalence classes p/~ of L-sentences p under the equivalence
p~\\r «=#• TV- p—y^; the partial order of LT(L, T) is p/~ y/7~ #=^ Th-p-*^ -
Let, with our notation in the Beth theorem, A = LT (L, 0) (empty theory over L ; free
Boolean algebra over the generators in L ) , B = LT (L (P), T) , and
D = LT (Lu{P, £}), T( P) uT(Q) ) . We have obvious Boolean homomorphisms f: A—B ,
B D : f(9/~
) =(p/~1 , g(9/~
) = p/~2 , h(p/~1) = p[Q/P]/~2 , where ~0 ,
~- , ~
are the equivalences used to define A, B and D , respectively, and ^[Q/P] is
obtained by substituting £ for p. We claim that the square
is a pushout. The verification of this claim uses only the general features of the concepts
involved, and it is an easy calculation.
Let's take the equalizer i : C-B of (g, h) , and the coregular factorization of f :
Previous Page Next Page