Monday, March 24, 2008

Varieties are the spice of logic

This is a retrospective look at Dunn's book. I'm trying to figure out what the point of the major theorems of the second chapter were apart from giving the reader some facility in a couple of important algebraic concepts. Read more

The second chapter of Dunn's algebraic logic book introduces several notions from universal algebra. The most important among these are: algebra (set with some operations under which it is closed), homomorphism (structure preserving function), and congruence relation (structure respecting equivalence relation). In the chapter he goes on to prove various theorems including what he describes as two big theorems from algebra. One of these is a theorem which says that every algebra is isomorphic to a subdirect product of prime algebras. I'm not sure how this is important for the development of the book. The other big theorem is about varieties, which are classes of algebras closed under direct products, subalgebras, and homomorphic images. It says that every variety is equationally definable and conversely. The converse is the easy direction. The hard direction takes several lemmas and the introduction of several new concepts. In subsequent chapters Dunn looks at logics whose operations are equationally definable, algebraized if you will. (Algebra-ized or alge-braised? Not sure.)

This sounds like it should be important for the development of the book. Indeed, some of these classes of algebras turn out to be fairly well known ones, like boolean algebras for classical logic. Right after this result further theorems are proved about soundness and completeness of a set of equations Q with respect to a word algebra W (algebra whose elements are "words" and whose operations combine the "words"). In Dunn's phrasing, Q is sound (satisfied by every algebra) in a class K of algebras with the same number of same arity operations as W, if the quotient algebra W/≡Q is free (the elements of the quotient are distinguishable in terms of the operations) in K. If
W/≡Q∈ K, then Q is complete with respect to K. This also sounds good.

Later in the book we are shown what some logics look like in equational form. Let's say, for concreteness, the implicational fragment of intuitionistic logic. We also know what that looks like in Hilbert-style axiom form as well as natural deduction and Gentzen-stye sequent calculus. The correspondence between Hilbert-style axioms, natural deduction, and sequent calculus is fairly well understood. Most proof theory books should go over translations between them. I'm not sure what a good answer is to the relation between the equational form and the axiomatic form. This is troubling me since this seems like it should be fairly clear. I think there is some answer in the Dunn book and I hope to return later this week with an answer. I'll just register the following point. When talking about the equational form, we are talking about also about a class of algebras. We have at our disposal notions like homomorphism and lots of algebraic machinery. There seems to be more structure there than in the sparse desert landscape that is a Hilbert-style axiomatic system. All the logic that we need to tease out the consequences of the equational form is that of equational logic, rules for symmetry, transitivity, substitution, and reflexivity.

Have we switched subjects between the equational characterization and the axiomatic characterization? The latter is naturally in proof theory but the former may be best understood as in semantics. The equational characterization is equivalent to a class of algebras and classes of algebras are good for semantics. This seems like it is on the right track. Dunn says that a logic is algebraizable if one can give an adequate equational characterization of an algebraic semantics. The proper relation is either not clear in Dunn or I am missing something important.

2 comments:

Kenny said...

I think one important, relevant fact about algebras is that the formulas you write down can involve arbitrary functions and operations, but the only relation allowed is identity. In more usual logic we're used to having lots of relations (and in some treatments we even translate away all n-ary functions and operations as just (n+1)-ary relations with existence and uniqueness axioms).

Shawn said...

Kenny,
Good point. Treating n-ary functions as special n+1-ary relations is is certainly the way I'm used to looking at them. Although, there is a certain amount of that in the Dunn book. Dunn defines operational homomorphism as a special case of relational homomorphism.

Another fact that could be relevant is that algebraic semantics for certain logics form varieties. I'm going to have to read that part of the book to figure out what to make of it.