HELENA RASIOWA, 1917 - 1994
by
W. Bartol, E. Orłowska, A. Skowron
Algebraic Logic
The study of the relationship between logic and algebra, originated by the work of George Boole and continued by A.Lindenbaum, A.Tarski, M.H.Stone, R.McKinsey, A.Mostowski and L.Henkin - to mention only a few - was the main research subject of Helena Rasiowa. One of the crucial moments in the development of algebraic study of logic was the introduction of Lindenbaum's and Tarski's method for treating equivalence classes of formulas as elements of an abstract algebraic system. This provided a link between theories based on classical logic and Boolean algebras. An analogous correspondence between intuitionistic logic and pseudo-complemented lattices was established by Stone and Tarski, while the application of algebraic methods to modal logics was originated by McKinsey and Tarski (1944 - 1948). Another important idea leading to the emergence of the field of algebraic logic was the treatment of formulas as algebraic functions in certain algebras, initiated by Ł ukasiewicz and Post with their generalization of truth tables.
Helena Rasiowa became very active in these areas in the early fifties. Her research work on algebraic logic was aimed at finding a precise description for the mathematical structure of formalised logical systems. Her early papers contain several examples of algebras associated with logical systems as well as algebraic proofs of some of their properties. Jointly with Roman Sikorski she presented the first algebraic proof of the Gödel completeness theorem for classical predicate logic ([4]). Next, she algebraically proved analogous theorems for intuitionistic and modal logics ([5]). In the papers [9, 13, 14, 16, 18, 21, 22, 23, 24, 25, 26] she turned to other nonclassical logics, applying with success the algebraic tools she had developed. All these investigations led her to a synthesis of the results hitherto obtained; she developed a general framework for an algebraic presentation of propositional and first order logics. In particular, she established elegant formal techniques for associating classes of algebras with logical systems and for providing their algebraic semantics. In the following we shall briefly outline the basic elements of her method for an algebraization of logics.
Rasiowa's first monograph The Mathematics of Metamathematics
([31]) written jointly with R.Sikorski, contains a comprehensive survey
of algebraic theories of logical calculi. Algebraization is applied to
classical, intuitionistic, modal and positive logics. The book focuses
on metalogical theorems on the predicate calculi of these logics and on
an investigation of elementary theories based on them. The main idea
underlying the concept of associating algebraic systems with logical
calculi is the following: Let ![]()
be a first order language such that ![]()
is its set of individual variables, ![]()
are the binary propositional
connectives of ![]()
, ![]()
is a unary propositional
connective and ![]()
are the
quantifiers of ![]()
Let ![]()
be a complete algebra such that
![]()
are binary operations, ![]()
is a unary operation and ![]()
and ![]()
are infinitary operations the
common domain of which is the class of all nonempty subsets of ![]()
By a realization of the language
![]()
in a nonempty set ![]()
and in the algebra ![]()
we mean any mapping ![]()
which assigns a function ![]()
to each function symbol ![]()
of ![]()
and a function ![]()
to any predicate symbol ![]()
of ![]()
The realization ![]()
is then extended to all the terms
and all the formulas of ![]()
Let ![]()
be a valuation of individual
variables in a set ![]()
Then we define:
{} ![]()
for any
individual variable ![]()
{} ![]()
{} ![]()
{} ![]()
{} ![]()
{} ![]()
{} ![]()
{} ![]()
where ![]()
and ![]()
![]()
![]()
for all ![]()
{} ![]()
where ![]()
is as above.
The algebraic semantics of the classical predicate logic is
determined by the class of realizations of the language ![]()
in Boolean algebras. We say that
a formula is true in a realization ![]()
whenever ![]()
for every valuation ![]()
where 1 is the unit element of
the underlying Boolean algebra. A formula ![]()
is valid in the classical
predicate logic if and only if ![]()
is true in all realizations in
any Boolean algebra. Similarly, the semantics of intuitionistic logic
is given by realizations in Heyting algebras, positive first order
logic is associated with realizations in the class of relatively
pseduocomplemented lattices. Modal logic, also considered in the book,
is semantically determined by the class of realizations in what is
known as topological Boolean algebras, i.e. Boolean algebras endowed
with a unary operation behaving like an interior operator.
In the next monograph An Algebraic Approach to Non-classical
Lo-gics ([49]) Helena Rasiowa develops a general algebraization
theory for propositional logical systems. Within the framework of this
theory she presents algebraizations of a number of non-classical logics
such as: classical and positive implicative logics, logics weaker than
positive implicative logic, minimal logic, positive logic with
semi-negation, constructive logic with strong negation and many-valued
Post logics. The fundamental idea behind algebraization is the
following: Let ![]()
be a propositional logic, where ![]()
is a propositional language that
includes implication as a binary connective and ![]()
is a consequence operation
determined by the axioms and inference rules. As usual, for a set ![]()
of formulas we denote by ![]()
the least set of formulas which
contains the axioms and the set ![]()
and is closed with respect to
the inference rules. In particular, ![]()
is the set of all the theorems
of ![]()
An algebra associated with ![]()
is any algebra of a type similar
to that of the algebra of formulas of ![]()
and endowed with a distinguished
element 1. Elements of such an algebra are interpreted as truth values,
whereas 1 represents the value true. Let ![]()
be the set of propositional
variables of ![]()
By a valuation in an algebra ![]()
associated with ![]()
we mean any mapping ![]()
Every formula ![]()
of the language ![]()
induces a mapping ![]()
defined as follows:
{} ![]()
for any
propositional variable ![]()
,
{} ![]()
for every unary propositional
connective ![]()
of ![]()
{} ![]()
for every binary connective ![]()
of ![]()
A formula ![]()
is said to be true in ![]()
if and only if ![]()
for every ![]()
Any propositional logic ![]()
determines thus a class of ![]()
-algebras, where an ![]()
-algebra is an algebra ![]()
associated with ![]()
such that for every formula ![]()
we have ![]()
for every ![]()
The completeness theorem states
that if ![]()
is consistent, then the set ![]()
is equal to the set of all
formulas which are true in each ![]()
-algebra.
Helena Rasiowa paid very much attention to many-valued Post logics.
She introduced several generalizations of the standard ![]()
-valued Post logics; she
considered the propositional and predicate versions of ![]()
-valued Post logics and used them
in her reasoning on programs. The following section describes some of
these applications in more detail.