**MacLogic Help - Syntax**

ATP | Menus | Rules | Syntax | Tactics

MacLogic uses a special font called 'Konstanz', which has, inter alia, the following special symbols for certain LOGICAL CONSTANTS:-

Á | "Shift Option Y" | for implication | |

& | "Shift 7" | for conjunction | |

Î | "Shift Option D" | for Disjunction | |

Ò | "Shift Option L" | for negation | |

Í | "Shift Option S" | for bi-implication | |

‰ | "Shift Option E" | for the Existential quantifier | |

Ë | "Shift Option U" | for the Universal quantifier | |

Ï | "Shift Option F" | for absurdity (Falsehood) | |

"Shift Option N" | for Necessity | ||

‡ | "Shift Option V" | for possibility | |

· | "Shift Option 9" | for strict implication | |

= | "=" | for equality | |

Ê | "Shift Option T" | for Turnstile | |

"Shift Option 2" | for Sequent Arrow |

MacLogic will also allow you to type

… | "Option H" | for implication, |

-> | for implication, | |

\/ | for disjunction, | |

<-> | for bi-implication | |

¬ | "Option L" | for negation, |

- | minus | for negation |

– | "Option minus" | for negation |

— | "Shift option minus" | for negation |

ƒ | "Option F" | for absurdity, |

\F | for absurdity, | |

\S | for strict implication, | |

\A | for the Universal Quantifier, | |

\U | for the Universal Quantifier, | |

Ëxy... | for ËxËy... | |

(x)... | for Ëx... | |

(xy)... | for ËxËy... | |

\E | for the Existential Quantifier, | |

\L | for necessity and | |

\M | for possibility |

but these will be displayed in proofs using the special symbols above.

ALPHABETIC characters are interpreted as follows:

a, ..., z | are INDIVIDUAL letters, standing for "individuals". |

A, ..., Z | are PREDICATE or PROPOSITION letters, standing for "predicates". |

A TERM consists just of an individual letter. (More powerful logics, but not MacLogic, allow compound terms.) These will also be called VARIABLES. We use the Greek letter µ schematically below to indicate a variable.

An ATOMIC FORMULA consists of a predicate or proposition letter, followed by a finite (possibly, and in propositional logic necessarily, zero) number of terms.

WELL-FORMED FORMULAE (i.e. WFFs) are inductively defined as follows:-

- any atomic formula is a wff;
- Ï is a wff;
- if A is a wff, then ÒA is a wff;
- if A and B are wffs, then (AÁB ) is a wff;
- if A and B are wffs, then (A&B ) is a wff;
- if A and B are wffs, then (AÎB ) is a wff;
- if A and B are wffs, then (AÍB ) is a wff;
- (for Predicate Logic only) let A be a wff containing the variable µ, but not containing a quantification of the form (Ëµ) or (‰µ); then (Ëµ)A and (‰µ)A are wffs. The wff A is called the SCOPE of the quantification. We say that a quantification, (‰µ), or (Ëµ), BINDs every occurrence of µ within its scope. These occurrences of variables are called BOUND. (Occurrences of) variables which are not bound are FREE. A term t is said to be FREE FOR a variable µ in A if no occurrence of µ in A lies in the scope of a quantification of the form (Ët) or (‰t). Loosely, one also talks of the SCOPE of a quantifier

Note that rule (h) forbids:

repeated quantification, as in (Ëx)(Ëx)Fxx,

vacuous quantification, as in (Ëx)(‰y)Fx, where 'y' is vacuously quantified.

(if Equality is in use)

- if s and t are terms, (s = t) is a wff;

(if Modal logic is in use)

- if A is a wff, then A is a wff;
- if A is a wff, then ‡A is a wff;
- if A and B are wffs, then (A · B) is a wff.

Definitions of MODAL and COMODAL :

- i. A, Ò‡A, (A · B) and Ï are S4-modal;

ii. if A and B are S4-modal, so are (A&B), (AÎB) and (‰µ)A;

- i. A, ‡A, (A · B) and Ï are S5-modal;

ii. if A and B are S5-modal, so are ÒA, (A&B), (AÎB), (AÁB), (Ëµ)A and (‰µ)A;

- i. ‡A, ÒA, Ò(A·B) and ÒÏ are S4-comodal;

ii. if A and B are S4-comodal, so are (A & B), (A Î B), (Ëµ)A;

- Every S5-modal wff is S5-comodal.

If one is using the modal logic S4, then 'appropriately modal' means S4-modal; similarly in S5.

Parentheses may be omitted in certain cases: one may omit outermost parentheses, and may drop inner parentheses where possible by virtue of the ranking of propositional connectives: 'Ò' ties more closely than '&' or 'Î', which tie more closely than 'Á', which ties more closely than 'Í'. Thus 'P&ÒQÁR' abbreviates ((P&ÒQ)ÁR). The quantifiers rank so that (Ëx)Ax&B abbreviates ((Ëx)Ax)&B, rather than (Ëx)(Ax&B).

If in doubt, put the parentheses in.

Also, 'Á' is right associative, which means that AÁBÁC means the same as AÁ(BÁC); but '&' and 'Î' are left associative, so that A&B&C means the same as (A&B)&C (and similarly for 'Î'). '·' is right associative too. When a formula is displayed by MacLogic, some extra space is put round the main connective to help you see the structure, as in A&B & C.

Square braces '[', ']' may be used sensibly instead of parentheses, as in (Ëx)[Ax&(BxÁCx)]: this helps make the formula's structure more clear. They must occur in matching pairs, and may not be used around quantifiers, as in [Ëx]Ax.

ATP | Menus | Rules | Syntax | Tactics

Created by Max Dyckhoff, September 1999