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

  1. any atomic formula is a wff;
  2. Ï is a wff;
  3. if A is a wff, then ÒA is a wff;
  4. if A and B are wffs, then (AÁB ) is a wff;
  5. if A and B are wffs, then (A&B ) is a wff;
  6. if A and B are wffs, then (AÎB ) is a wff;
  7. if A and B are wffs, then (AÍB ) is a wff;
  8. (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:

(if Equality is in use)

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

(if Modal logic is in use)

  1. if A is a wff, then A is a wff;
  2. if A is a wff, then A is a wff;
  3. if A and B are wffs, then (A · B) is a wff.

Definitions of MODAL and COMODAL :

  1. 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;
  1. 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;
  1. i. A, ÒA, Ò(A·B) and ÒÏ are S4-comodal;
    ii. if A and B are S4-comodal, so are (A & B), (A ΠB), (˵)A;
  1. 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