FOM: ``Reduction'' of FOL to Propositional logic

[Matt Insall]

I have been convinced for a while that there is a sense in which all of
logic can be ``reduced'' to Propositional Logic.  I am interested in your
views on this topic.  Let me outline the process for any FOL relational
language L with arbitrarily many constant symbols (by ``relational'' I mean
L has no function symbols).  My propositional language P has as many
propositional symbols as there are finite strings of constant and relation
symbols of L. But my propositional language is not finitary.  It has an
infinitary OR operator and an infinitary AND operator.  I map each atomic
formula of the form Rxyz...w to a propositional variable in a one-to-one and
onto way.  I map each logical axiom to a corresponding one in which the
universal quantifiers are interpreted via application of the infinitary
conjunction, and the existential quantifier is mapped to the infinitary
disjunction.  For instance, if a(x) is an atomic formula whose only free
variable is x, then denote by f[a] the image of all substitution instances
of a, where variables are substituted for x in a(x).  Then I map (Ax)a(x) to
AND{f[a]} and I map (Ex)a(x) to OR{f[a]}.  In fact, this is the idea behind
the use of Herbrand semantics in logic programming, is it not?  In any case,
the idea is motivated by the construction of the Lindenbaum-Tarski Algebra
of a given FOL language, as in ``Models and Ultraproducts'' by Bell and
Slomson, page 61, but I am sure I have seen this done, for I believe it is a
large part of the motivation for studies of the theory of complete lattices.
For in fact, the Lindenbaum-Tarski algebra has some completeness properties
that translate into the availability of these infinitary conjunctions and
infinitary disjunctions.  In fact, when ``reducing'' a countable FOL
language to a propositional language, only countably many propositional
variables are needed, etc.  Yet there is a cost:  To me, it seems somewhat
unnatural to use propositional calculus to do things I naturally represent
in FOL, such as theorems that quantify over all members of some domain.
Thus I prefer to work in FOL or some form of SOL or HOL.




Dr. Matt Insall
http://www.umr.edu/~insall