3.3 Definition expansion

Definitions are a useful way of increasing the expressive power of a language. If one can define a new concept in terms of old ones, then all one's knowledge about the old ones can be applied to the new concept.

In MacLogic, definitions are used rather sparsely. Definitions of two logical symbols are available: the definition of negation in terms of implication and contradiction, and of equivalence in terms of implication and conjunction, detailed below.

One can choose whether or not the definition is applied automatically by MacLogic. One point of view is that if two formulae are "definitionally equal", as are for example ÒA & B and (A Á Ï) & B, then the use of one in a context where the other should be used should be acceptable without comment. The other point of view is that the replacement of a formula by a definitionally equal formula should involve invocation of the rule "Definition".

The two views are reflected by adjustments to the item Delta conversion in the Options menu. If Delta conversion is ticked, then two definitionally equal formulae can be used interchangeably without comment. If Delta conversion is unticked, then expansion or contraction of formulae using definitions must be explicitly invoked. We now describe how to do this just in the case where Delta conversion is unticked. [When it is ticked, there is neither necessity nor possibility of invoking the definition mechanism.]

In Check mode, suppose we have established a formula P, depending on certain assumptions. We may now derive a formula Q, depending on the same assumptions, by invoking the rule "Defn.", accessed via the ... radio button, and quoting as premiss the line number on which P was established, provided that P and Q are definitionally equal. [Note that if P and Q are actually the same formula, this can still be done, but it may look a little odd!]

In Construct mode, suppose we are working on a problem FA, where F is a formula list and A is a formula. If we invoke the tactic for "Definition", accessed via the ... radio button, MacLogic looks to see whether or not any of the formulae in the problem have a principal symbol which is a defined symbol, and thus admit a rather simple expansion. If there is only one such formula, the expansion is done immediately, the move from one line to the next being marked by the comment "Using tactic for Definition". If there are several such formulae, you are asked to choose which one is to be expanded.

Note that there is a restriction here: in Construct mode, you may not (in effect) point at a formula and say that it is to be replaced by a definitionally equal formula: all you can do is expand a definition used at the top level. This avoids the necessity of typing in the new formula.

For example, PÍQ can be expanded to (PÁQ)&(QÁP), since Í is a defined symbol; but (PÍQ)&R cannot be expanded to ((PÁQ)&(QÁP))&R, even though they are definitionally equal.

Note also that if Delta conversion is ticked, you may use the rules for implication in place of the rules for negation: negation is just a special case of implication. Likewise, equivalences A Í B are just a special case of conjunctions, so the rules for & are applicable. But when Delta conversion is not ticked, then a formula of the form A Í B must be expanded explicitly, as described above, before its components can be used.

The definitions currently built into MacLogic are that

ÒA ˜ AÁÏ.

A Í B ˜ (AÁB) & (BÁA).

where A, B are arbitrary formulae. [ ˜ is a symbol traditionally used between a definiendum, on the left, and the definiens, on the right. ]