#### 1.1 Elementary logic --- its scope and purpose

By *elementary logic*, we understand certain aspects of
logic which are regarded as fundamental. We avoid the use of compound
terms, such as *x *+* y*, and stick to the
part of logic concerned with purely logical rules rather than
with rules deriving from mathematical practice, or from some other
specific domain. This restriction allows us to use a fairly simple
syntax, and to make certain parts of the MacLogic program itself
fairly efficient.

We stick to zero-order and first-order logic, traditionally
known as *propositional calculus* and* predicate calculus*
respectively. (We prefer the non-traditional names, to suggest
to the discerning reader that logicians are also interested in
higher-order logics.)

MacLogic is a proof assistant, intended as a vehicle for learning
about proofs. In our view, proof theory is fundamental to logic,
and the "semantic" aspect of logic, concerning Boolean
algebras, valuations, models, etc, is secondary. Proof theory
owes a great deal to Gentzen's pioneering work in the 1930s, especially
as kept alive by the intuitionists and type theorists such as
Girard, Heyting and Martin-Löf. Some so-called "semantic"
techniques are just notational variants of the syntactic notions
we shall encounter.