FOM: new book announcement, from Walter Felscher

[Stephen G Simpson]

There just appeared with the publishing house of Gordon and Breach my

      Lectures on Mathematical Logic

      Vol.1 : Set Theoretical Logic - The Algebra of Models
              283 pages   ISBN 90 5699 266 X  ,  GBP 40  US$ 58

      Vol.2 : Calculi for Derivations and Deductions
              336 pages   ISBN 90 5699 267 8  ,  GBP 40  US$ 58

      Vol.3 : The Logic of Arithmetic
              312 pages   ISBN 90 5699 268 6  ,  GBP 40  US$ 58


Volume 1 is an introduction to mathematical logic in which all the usual
suspects are presented: semantical consequence and its compactness and
axiomatizability, Loewenheim-Skolem-Tarski theorems, prenex and other
normal forms, characterizations of elementary classes with help of
ultraproducts.  What is less usual here are the methods by which these
results are developed: logic is based exclusively on semantics: truth and
satisfiability of formulas in structures are the basic notions, and there
is no need to mention logical calculi with axioms and rules.  The methods
throughout rely on algebraic notions such as homomorphisms and congruence
relations, and this not just as abbreviations, but in order to gain new
insights.  They are developed in an introductory chapter which, together
with the chapters 5 to 9 on equations, can be viewed as a first course on
universal algebra.  The algorithms generating semantical consequence are
obtained in a uniform manner, first for equations in algebras, next for
propositional formulas and open formulas of predicate logic, and then for
the formulas of quantifier logic.  Here the former argumentation carries
over directly as long as formulas are evaluated in Boolean valued
structures; the reduction of the classical 2-valued case then depends on
the Boolean prime ideal theorem.  It is essential for this approach that
in canonical structures evaluation and substitution are related to each
other; hence a preliminary study of simultaneous substitutions is
required which have a built-in renaming operator to avoid collisions of
variables.



Volume 2 begins by observing that in everyday's argumentations, as
brought forward, say, by a lawyer, statements are transformed
linguistically, connecting them in formal ways irrespective of their
contents.  Understanding the objects of such argumentations as "deductive
situations" or "sequents", the transformations between them can be viewed
to take place with help of "logical rules".  This leads to Gentzen's
calculi of derivations, presented first for positive logic and then for
minimal, intuitionistic and classical logic, depending on the requirements
made on the behaviour of negation.  Identifying interdeducible formulas,
each of these calculi gives rise to a lattice-like ordered structure, and
the description of the generation of filters in these structures leads to
corresponding modus ponens calculi.  These turn out to be semantically
complete because they express the algorithms generating semantical
consequences as obtained in volume 1 .  Attention again has to paid to
substitutions in order to set up syntactic equivalences in preparation
for cut elimination.  The operators transforming derivations from one
type of calculus into an other are studied also with respect to changes
of the lengths of derivations, and operators eliminating defined
predicate and function symbols are described explicitly.  The book ends
with the algorithms producing the results of Gentzen's midsequent theorem
and of Herbrand's theorem for prenex formulas.


Volume 3 begins with decision methods for derivability in fragments of
arithmetic based on order-plus-successor and on order-plus-addition
(Presburger arithmetic).  They make use of quantifier elimination which,
in turn, is also applied to obtain consistency proofs for these fragments.
Stronger fragments of arithmetic, containing also multiplication, are
sufficiently rich to express a primitive recursive encoding of terms,
formulas and deductions, and this leads to G"odel's theorem exhibiting
statements undecidable already in such fragments.  Its central idea,
isolated in Tarski's fixpoint lemma, has a certain analogy with Eubulides'
antinomy of the Liar, and in a non-technical chapter, destined for a
wider class of readers, this analogy is exploited for an informal
discussion of undefinability and incompleteness.  The technical tools, on
the other hand, required to verify the hypotheses on arithmetical
representability, are collected in an autonomous presentation of
recursive functions and relations.  - For the theory PA of full
arithmetic with induction it is shown that its extension PR by symbols
for primitive recursive functions is conservative.  Thus PR permits us to
speak about the encoding of PA itself, and this, essentially, with free
variable formulas.  This makes it possible to verify the Bernays-L"ob
provability conditions which entail G"odels theorem about the
unprovability in PR of the encoded form of statements expressing the
consistency of PA .


Walter Felscher