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