include $_SERVER["DOCUMENT_ROOT"].'/think/module.php'; section('Syntax'); ?> Now let us formally present the syntax of MPL.
MPL contains the following symbols:
1. Predicate letters : A, B, C, ... Z. If a subscript is added to a predicate letter, the result is a predicate letter, e.g. A1 , B274, etc.2. Constants : a, b, c, ... t. If a subscript is added to a constant, the result is a constant, e.g. a1, b24, etc.
3. Variables : u, v, w, x, y, z. If a subscript is added to a variable, the result is a variable, e.g. x1, y24, etc.
4. Five sentential connectives :
~ (tilde, or the negation sign)
5. Open and close brackets : ( )
& (ampersand, or the conjunction sign)
∨ (the wedge, or the disjunction sign)
→ (the arrow)
↔ (the double-arrow)
An expression of MPL is a string of one or more symbols of MPL.
The syntactic rules, or formation rules, for MPL are as follows :
Rules of formation:Rule #1 tells us that expressions such as "Pa", "Qb", "Gc" are wffs. Rules #2 and #3 are just like rules from SL. We can apply rules #2 and #3 to form new wffs such as "~~Pa", "~((Pa&Sc)↔(~Fb∨Ka))".
- Any predicate letter followed by a constant is a wff.
- If φ is a wff, then ~φ is a wff.
- If φ and ψ are wffs, then (φ&ψ), (φvψ), (φ→ψ), (φ↔ψ) are also wffs.
- If φ is a wff that contains any constant ω, and β is a variable which does not occur in φ, then the resulting expression that is obtained by replacing one or more occurrences of ω with β and then attaching "∃β" or "∀β" to the front, is also a wff.
- Nothing else is a wff.
Rule #4 is a little complicated. It applies only to wffs that include at least one constant. So it applies to expressions such as "Qa", "(~Pa→Qb)", "(Pa&Qa)", but not "∃xFx". The rule says that we can pick a constant in a wff, replace one or more occurrences of that constant by a single variable, and then add either an existential or universal quantifier to the front. Here are some examples:
From "Qa", we can generate wffs such as "∃xQx", "∀yQy".From "(~Pa→Sa)", we get "∃y(~Py→Sy)" or "∃x(~Px→Sx)" or "∃x(~Px→Sa)" or "∃x(~Pa→Sx)", or "∀x(~Px→Sx), or "∀y(~Py→Sa)" etc.
From "(~Qa→Qb)", we get "∃x(~Qx→Qb)", "∀z(~Qa→Qz)" (But not "∃x(~Qx→Qx)"!)
pagefooter(); ?>
- (P&(P&~R)) popupbox('Not a wff of MPL. (It is a wff of SL.)'); ?>
- ∃x(Mx↔~Qx) popupbox('Yes'); ?>
- ~∃x~(Ma↔~Qx) popupbox('Yes'); ?>
- ~(~∀xKx∨∃y~Qy) popupbox('Yes'); ?>
- ∀x∀y(Qx&Py) popupbox('Yes'); ?>
- ∀x(Px&∀y~Ly) popupbox('Yes'); ?>
- ∃x(P→Qa) popupbox('Not a wff.'); ?>
- ∀x∀yFxy popupbox('Not a wff.'); ?>
- ((∀xKx&∀yQy)∨Ma) popupbox('Yes'); ?>
- (∀xKx&((∀yQy)∨Ma)) popupbox('Not a wff.'); ?>
- (∀xKx&∀yQy∨Ma) popupbox('Not a wff.'); ?>
- ~~~∃x~~~Gx popupbox('Yes'); ?>
- (~~~∃x~~~Gx&Hx) popupbox('Not a wff.'); ?>
- ~~∃x(~Gx&Hx) popupbox('Yes'); ?>
- ∀x((Ga∨Bx)↔(Kb&Gx)) popupbox('Yes'); ?>
- ∀x((Gx∨Bx)↔(Kx&Gx)) popupbox('Yes'); ?>
- ∀x((Ga∨Ba)↔(Ka&Ga)) popupbox('Not a wff.'); ?>