An elegant way of writing FOL(=,e)
in [Logic]
|
Prev: POLYNOMIAL POEM
Next: If - this statement is used to open an exact proof p = np, if this is true or false, do this.
From: zuhair on 4 May 2010 04:01 Logical connectives: Negation ~ Disjunction | Implication > Conjunction juxtapositioning of the formulae. Example: QP stands for: Q and P Biconditional <> Quntifiers Existential quantifier _ _x stands for "there exist x" Unique existential quantifier ! !x stands for "there exist unique x" Universal quantifier no symbol just mention the quantified variable on the left of the formula with space in between x Q(x) is read as for all x Q(x). x, _y stands for "for all x, there exist y". x, _y Q(x,y) is read as: for all x there exist y such that Q(x,y). Primitives: Membership no symbol, just juxtapositioning the variables so xy stands for "x is a member of y" Identity = Functions: same as traditional f(x0,...,xn) and f:A -> B standing for f is a function having A as its domain, and B as its co-domain. Contants are zero-arity function symbols, usually written using upper case letters. Predicates: Q(x0,...,xn) Set builder: same as traditional {:} or {|}. Strings of variables: x0,...,xn examples: used in n-arity functions and predicates, and also in quantification. _x0,...,xn refers to Exist x0,..., Exist xn while x0,...,xn placed before a formula with space between xn and the formula, then this string mean for all x0,...,for all xn while _x0; x1,...,xn refers to Exist x0 for all x1,...,for all xn notice the semi-colon in between x0 and x1. THE FOUR RULES OF ABBREVIATION: RULE 1: Rule of minimal required notation for unique interpret-ability: "A formula has only ONE interpretation, with the minimal amount of symbols to achieve that". RULE 2: Rule of dot notation: A dot notation is to be placed always on the left of a connective. we have different powers of dot notations:- .. is a unit power dot notation : is a double power dot notation :. is a triple power dot notation :: is a quadruple power dot notation ::. is a five unit power dot notation and so on, the power of a dot notation is the number of dots in it. "The less is the power of the dot notation placed on the left of a connective, the earlier this connective is processed". So first connectives to be processed in a formula are those having no dot notation on the left of them, then those having unit power dot notations, then double power, then triple, till the maximal power dot notation in the formula. Examples: P|Q.|Q:>D.S<>K this would be ( (P|Q) | Q ) > (D and (S<>K)) so instead of 8 brackets, we only have three dot notations. Another example: P|Q:.|Q:>D.S<>K this would be (P|Q) | (Q>(D and (S<>K))) so 8 brackets are reduced to 4 dot notations. RULE 3: Rule of Hidden quantifiers: "Quantifiers are hidden if their appearance would be consecutive otherwise; or in case of universal quantification the order of which is totally predictable without their appearance". Example: Exist x For all y ( y e x iff Q ) this is written as _x,y yx<>Q however we see that y is appearing consecutively, so it is better to hide the first y so this can be written as _x yx<>Q Example: zx<>zy>y=x this is: for all x for all y ( for all z (zex <->zey) -> x=y ). Note: hiding the quantifiers is optional. RULE 4: Exhaustive quantification: "All occurrences of a variable are quantified by the same quantifier". So we cannot have a formula like _yx > _yx _cy cx because y is quantified twice. so we need to choose another variable instead of a second y like _yx > _zx _cz cx which is axiom of foundation. according to rule 4 we cannot have the same variable being bound and free, or bound by two different quantifiers; this would obviate the need for quantification brackets. Examples showing the abbreviating power of this methodology: t _x yt <> w _k uw <> u is a wiener ordered pair i _s,r isru > i subset k j _p,q jpqu 0q > j=x > yw is the abbreviation of: for all t Exist x for all y ( y e t <-> for all w ( Exist k for all u ( u e w <-> (u is a wiener ordered pair & for all i (Exist sr (iesereu) -> i subset k)& for all j (Exist pq (jepeqeu & 0eq) -> j=x))) -> yew)). Writing ZF set theory axioms: _____________________________________________ Extensionality: zx<>zy > x=y Foundation: _yx > _zx _cz cx Empty: _x ~yx Pairing: a,b _x yx.<> y=a|y=b Union: a _x yx <> _z yza Power: a _x yx<> zy>za Separation: a _x yx.<> yaQ Replacement: x!yQ(x,y)> a _b zb <>_xaQ(x,z) Infinity: _x 0x yx > z uz.<>uy|u=y > zx _______________________________________________ This syntax is both elegant, abbreviating and easily readable. Zuhair |