2

MICHAEL MAKKAI

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/~

Q

) =(p/~1 , g(9/~

1

) = p/~2 , h(p/~1) = p[Q/P]/~2 , where ~0 ,

h

~- , ~

2

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 :