The syntax of first-order formulae (in MacLogic) allows the use of variables, a...z, as terms. It does NOT allow compound terms such as x+y or f(x,y). There is no syntactic distinction between free and bound variables, nor any division into "constants" and "variables". No parentheses are needed between predicate letters, A...Z, and their arguments.

Free and bound occurrences of variables are defined as usual - see the file "Syntax Help" for formal details. Vacuous quantification and repeated quantification are prohibited.

Standard inference rules, for introduction and elimination of the universal and existential quantifiers, are provided.

When using inference rules and tactics, it is important to
know when two formulae are identical. (For example, *modus ponens*,
the rule of Á-Elimination,
operates on two formulae A Á C
and B, and is acceptable provided
the formulae A and B
are identical, i.e. the "same".) We therefore
need a precisely defined notion of *identity* between formulae.
This is routine for zero-order formulae: but it becomes non-trivial
when bound variables are present.

Two conventions are possible:

- One is that two formulae are identical if (ignoring spaces and superfluous parentheses) exactly the same characters are used in each, in the same order.
- The other is that two formulae are identical if they are
what is called, in the lambda calculus,
*alpha-convertible*, i.e. they differ only in the names used for bound variables.

Thus, according to the first convention, the two formulae (Ëx)(Ëy)Awxy and (Ëy)(Ëz)Awyz are not identical, whereas, according to the second, they are identical. Note that neither is identical, under either convention, to (Ëw)(Ëx)Awwx, since w in the latter has no free occurrence.

Both conventions are encoded in MacLogic: the choice between them is made from the Options menu, by ticking or unticking the Alpha conversion item. (Note that the notion of identity actually includes the possibility of expanding definitions as well - see section 3.3 below.)

This has the effect that if alpha conversion is on, then the problem of deriving, say, (Ëx)(Ëy)Awxy from (Ëy)(Ëz)Awyz is trivial, whereas if it is off, one has to do two Ë-elimination steps followed by two Ë-introduction steps.

The usual restrictions on variables for the quantifier rules are implemented. In Construct mode, the choice of the tactic for ‰-elimination or Ë-introduction requires the use of a new variable, not occurring free in the current problem. MacLogic either chooses a new variable for you, or asks you to choose one from a list, according to whether alpha conversion is on or off. Likewise, the other quantifier tactics require you to enter a term (actually just a variable, since we have no compound terms or constants). If alpha conversion is off, this must be free for the bound variable being replaced, and is rejected if not; but if alpha conversion is on, then any variable is accepted, and the bound variables are renamed to avoid capturing the entered variable.

One feature, in Construct mode, of the quantifier tactics is a little odd: suppose one is trying to solve the problem (Ëx)Ax => (Ëy)Ay with alpha conversion off. One obvious way is to replace it by the problem(Ëx)Ax => Ay and now use the tactic for Ë-elimination, choosing the term y to instantiate the occurrence of x freed by removal of the quantifer: this is transformed to the natural deduction proof

1 | (1) | (Ëx)Ax | Ass. |

1 | (2) | Ay | 1 ËE |

1 | (3) | (Ëy)Ay | 2 ËI |

One might also wish to be able to replace the original problem by Ay(Ëy)Ay and now use the tactic for Ë-introduction. This is not allowed, since the new variable y used to replace the bound occurrence of y on the RHS occurs free in Ay. In fact, it does not occur free in the assumption (Ëx)Ax from which Ay was derived, so the use of y is harmless: nevertheless, the sequent calculus rules forbid use of y as a new variable at this point. This restriction does not however reduce the range of natural deduction proofs which can be constructed.

Equality may be selected from the
**Logic** menu, in which case the tactics and rules for equality
may be used. (Equations are always acceptable as formulae, even
if Equality is not selected in the
Logic menu.) The rules for equality
are accessible (in the Next Line dialog
box) from the =... radio button (there
isn't room for them otherwise!) The tactics for equality appear
as radio buttons in the Tactic choice
dialog box.

Equality (often, but not in MacLogic, called "identity") is an equivalence relation, i.e. is reflexive (everything is equal to itself), symmetric (one thing equals another if the other is equal to the first), and transitive (whatever equals something equal to a third thing is itself equal to the third thing). But equality is in a sense the smallest equivalence relation, so if a and b are equal, then anything true of a is also true of b---a congruence principle incorporated as the rule =E, in counterpoint to the reflexivity incorporated as the rule =I. [The symmetry and transitivity can actually be derived from these two rules, but it is convenient to make them available as if they were primitive rules of the logic.]

Using the rules for equality (in MacLogic's Check
mode) is straightforward. The tactics for equality (in Construct
mode) are straightforward in the case of reflexivity (in fact,
any goal of the form x = x is regarded
as trivial, and you are not required to invoke the tactic for
=I), symmetry, and transitivity. That
for =E requires more care. The tactic
for =E is that if you know an equation
s = t, and the goal is any formula
C, you may replace the current problem
by two sub-problems---the first that of showing A(s),
and the second that of showing C from
the additional knowledge of A(t),
where A(v) is a formula with one
or more occurrences of a free variable v.
(If there are no such occurrences, the tactic reduces to the **Cut**
tactic.) You are required, by means of a dialog, to enter the
formula A(v), and to indicate what
the variable v is to be replaced
by.

For example, suppose we want to prove that = is symmetric, without using the =symm tactic. Our initial problem (we show formulae parenthesised for clarity) then is, after removal of quantifiers and use of the tactic for ÁI:

We now use the tactic for =E, and enter the formula A(v) ˜ (v = x), with v as designated variable. (What you actually type in is v = x in one edit field, and the variable v in the other.) The new sub-problems are first to show A(x) from (x=y), and secondly to show (y=x) from A(y) and (x=y), i.e.:

both of which are trivial.