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 + 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.